diff --git a/Hsmtlib.cabal b/Hsmtlib.cabal --- a/Hsmtlib.cabal +++ b/Hsmtlib.cabal @@ -1,76 +1,37 @@ --- Initial Hsmtlib.cabal generated by cabal init. For further --- documentation, see http://haskell.org/cabal/users-guide/ - --- The name of the package. -name: Hsmtlib - --- 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.2.0.6 - --- A short (one-line) description of the package. -synopsis: Haskell library for easy interaction with SMT-LIB 2 compliant solvers. - --- A longer description of the package. -description: - Hsmtl provides functions to interact with several smt solvers using SMT-LIB 2. - - The current suported solvers are Alt-Ergo, Cvc4, MathSat, Yices, Z3. - Additional solvers can be used if they are SMT-LIB 2 compliant. - - More information and tutorials can be found in - --- URL for the project homepage or repository. -homepage: https://github.com/MfesGA/Hsmtlib - --- The license under which the package is released. -license: BSD3 - --- The file containing the license text. -license-file: LICENSE - --- The package author(s). -author: Nuno Laranjo and Rogerio Pontes - --- An email address to which users can send suggestions, bug reports, and --- patches. -maintainer: numicola@gmail.com and rogeriop062@gmail.com - --- A copyright notice. --- copyright: - -category: SMT - -build-type: Simple - --- Extra files to be distributed with the package, such as examples or a --- README. --- extra-source-files: - --- Constraint on the version of Cabal needed to build this package. -cabal-version: >=1.10 - - -library - -- Modules exported by the library. - exposed-modules: Hsmtlib, Hsmtlib.Solver, Hsmtlib.HighLevel, Hsmtlib.Solvers.Z3, Hsmtlib.Solvers.Yices, Hsmtlib.Solvers.MathSAT, Hsmtlib.Solvers.Cvc4, Hsmtlib.Solvers.Boolector, Hsmtlib.Solvers.Altergo, Hsmtlib.Solvers.Cmd.ScriptCmd, Hsmtlib.Solvers.Cmd.OnlineCmd, Hsmtlib.Solvers.Cmd.BatchCmd, Hsmtlib.Solvers.Cmd.ProcCom.Process, Hsmtlib.Solvers.Cmd.Parser.Visualizers, Hsmtlib.Solvers.Cmd.Parser.Syntax, Hsmtlib.Solvers.Cmd.Parser.Parsers, Hsmtlib.Solvers.Cmd.Parser.CmdResult - - -- Modules included in this library but not exported. - -- other-modules: - - -- LANGUAGE extensions used by modules in this package. - -- other-extensions: - - -- Other library packages from which modules are imported. - build-depends: base >=4.6 && <= 4.7, smtLib >=1.0 && <1.1, containers >=0.5 && <0.6, pretty >=1.1 && <1.2, process >=1.1 && <= 1.2 , transformers >=0.3 && <0.4, parsec >=3.1 && <3.2 - - -- Directories containing source files. - -- hs-source-dirs: - - -- Base language which the package is written in. - default-language: Haskell2010 - +-- Initial Hsmtlib.cabal generated by cabal init. For further +-- documentation, see http://haskell.org/cabal/users-guide/ + +name: Hsmtlib +version: 2.8.8.8 +synopsis: Haskell library for easy interaction with SMT-LIB 2 compliant solvers. +description: + Hsmtl provides functions to interact with several smt solvers using SMT-LIB 2. + + The current suported solvers are Alt-Ergo, Cvc4, MathSat, Yices, Z3. + Additional solvers can be used if they are SMT-LIB 2 compliant. + + More information and tutorials can be found in +homepage: https://github.com/MfesGA/Hsmtlib + +-- The license under which the package is released. +license: BSD3 + +-- The file containing the license text. +license-file: LICENSE + +author: Nuno Laranjo And Rogério Pontes +maintainer: numicola@gmail.com and rogerp062@gmail.com +-- copyright: +category: SMT + +build-type: Simple +-- extra-source-files: +cabal-version: >=1.10 + +library + exposed-modules: Hsmtlib, Hsmtlib.Solver, Hsmtlib.HighLevel, Hsmtlib.Parsers.ParseResponse, Hsmtlib.Parsers.Visualizer, Hsmtlib.Parsers.ParseScript, Hsmtlib.Parsers.Syntax, Hsmtlib.Parsers.AuxParser, Hsmtlib.Solvers.Boolector, Hsmtlib.Solvers.Cvc4, Hsmtlib.Solvers.Altergo, Hsmtlib.Solvers.Z3, Hsmtlib.Solvers.Yices, Hsmtlib.Solvers.MathSAT, Hsmtlib.Solvers.Cmd.BatchCmd, Hsmtlib.Solvers.Cmd.ResultHelpers, Hsmtlib.Solvers.Cmd.CmdResult, Hsmtlib.Solvers.Cmd.OnlineCmd, Hsmtlib.Solvers.Cmd.ScriptCmd, Hsmtlib.Solvers.Cmd.ProcCom.Process + -- other-modules: + -- other-extensions: + build-depends: base >=4.7 && <4.8, containers >=0.5 && <0.6, smtLib >=1.0 && <1.1, transformers >=0.4 && <0.5, parsec >=3.1 && <3.2, pretty >=1.1 && <1.2, process >=1.2 && <1.3 + -- hs-source-dirs: + default-language: Haskell2010 diff --git a/Hsmtlib.hs b/Hsmtlib.hs --- a/Hsmtlib.hs +++ b/Hsmtlib.hs @@ -1,58 +1,61 @@ -{- | - Module : Hsmtlib - Main module which provides the function to initialize a Solver. --} - -module Hsmtlib(startSolver) where - -import Hsmtlib.Solver as Slv -import Hsmtlib.Solvers.Altergo (startAltErgo) -import Hsmtlib.Solvers.Boolector (startBoolector) -import Hsmtlib.Solvers.Cvc4 (startCvc4) -import Hsmtlib.Solvers.MathSAT (startMathSat) -import Hsmtlib.Solvers.Yices (startYices) -import Hsmtlib.Solvers.Z3 (startZ3) -import Hsmtlib.HighLevel -{- | - -The function to initialialyze a solver. -The solver can be initialized with a desired configuration, or a diferent -Path to keep the script in Script Mode, if Nothing is passed then it will use -the default settings. - -There are two 'Mode's of operation for the solvers, Online and Script. - -In online Mode a solver is created and kept running. Commands are sent -via pipe one by one and every time one is sent it also reads the answer of the -solver. - -In script 'Mode' a file is created in a desired file path, if Nothing is passed -then its created in the current directory with the name temp.smt2. -If a file already exists then it's overwriten. - -The functions in this mode (Script) behave in the following manner: -If it's a funcion where something is declared, for example declareFun or assert -then it's only writen to the file. In functions where some feedback is expected -such as checkSat, this are writen to the file, a solver is created and the -file is given to solver, and it waits for the result. The result is the result -of the last function. - --} - - - -startSolver :: Solvers -- ^ Avaliable'Solvers'. - -> Mode -- ^ Avaliable 'Modes', Online, Script, Context. - -> Logic -- ^ The desired SMT Logic. - -> Maybe SolverConfig -- ^ A customized Configuration for the Solver. - -> Maybe String -- ^ A possible alternate path to save the Script. - -> IO Solver -startSolver Z3 mode logic = startZ3 mode $ show logic -startSolver Cvc4 mode logic = startCvc4 mode $ show logic -startSolver Yices mode logic = startYices mode $ show logic -startSolver Mathsat mode logic = startMathSat mode $ show logic -startSolver Altergo mode logic = startAltErgo mode $ show logic -startSolver Boolector mode logic = startBoolector mode $ show logic - - - +{- | + Module : Hsmtlib + Main module which provides the function to initialize a Solver. +-} + +module Hsmtlib(startSolver) where + +import Hsmtlib.Solver as Slv +import Hsmtlib.Solvers.Altergo (startAltErgo) +import Hsmtlib.Solvers.Boolector (startBoolector) +import Hsmtlib.Solvers.Cvc4 (startCvc4) +import Hsmtlib.Solvers.MathSAT (startMathSat) +import Hsmtlib.Solvers.Yices (startYices) +import Hsmtlib.Solvers.Z3 (startZ3) +{-import Hsmtlib.HighLevel +import Hsmtlib.Parsers.AuxParser +import Hsmtlib.Parsers.ParseResponse +import Hsmtlib.Parsers.ParseScript +import Hsmtlib.Parsers.Syntax +import Hsmtlib.Parsers.Visualizer-} + +{- | + +The function to initialialyze a solver. +The solver can be initialized with a desired configuration, or a diferent +Path to keep the script in Script Mode, if Nothing is passed then it will use +the default settings. + +There are two 'Mode's of operation for the solvers, Online and Script. + +In online Mode a solver is created and kept running. Commands are sent +via pipe one by one and every time one is sent it also reads the answer of the +solver. + +In script 'Mode' a file is created in a desired file path, if Nothing is passed +then its created in the current directory with the name temp.smt2. +If a file already exists then it's overwriten. + +The functions in this mode (Script) behave in the following manner: +If it's a funcion where something is declared, for example declareFun or assert +then it's only writen to the file. In functions where some feedback is expected +such as checkSat, this are writen to the file, a solver is created and the +file is given to solver, and it waits for the result. The result is the result +of the last function. + +-} + + + +startSolver :: Solvers -- ^ Avaliable'Solvers'. + -> Mode -- ^ Avaliable 'Modes', Online, Script, Context. + -> Logic -- ^ The desired SMT Logic. + -> Maybe SolverConfig -- ^ A customized Configuration for the Solver. + -> Maybe String -- ^ A possible alternate path to save the Script. + -> IO Solver +startSolver Z3 mode logic = startZ3 mode $ show logic +startSolver Cvc4 mode logic = startCvc4 mode $ show logic +startSolver Yices mode logic = startYices mode $ show logic +startSolver Mathsat mode logic = startMathSat mode $ show logic +startSolver Altergo mode logic = startAltErgo mode $ show logic +startSolver Boolector mode logic = startBoolector mode $ show logic diff --git a/Hsmtlib/HighLevel.hs b/Hsmtlib/HighLevel.hs --- a/Hsmtlib/HighLevel.hs +++ b/Hsmtlib/HighLevel.hs @@ -1,112 +1,125 @@ -{- | - Module: Hsmtlib.HighLevel - This Module provide auxiliar functions that simplify writing expressions - to send to the solver. --} - -module Hsmtlib.HighLevel where - -import Hsmtlib.Solver as Slv -import SMTLib2 - - -{- | - This function hides the application of a function on the SMT syntax - receives the name of the function and the args and gives the corresponding - SMT2Lib syntax. --} -functionArg :: Name -> [Expr] -> Expr -functionArg fun = App (I fun []) Nothing - - -{- | - This function hides the application of a constant function on the - SMT syntax receives the name of the function and gives the corresponding - SMT2Lib syntax, the function must be already declared using declareFun. --} -constant :: String -> Expr -constant x =App (I (N x) []) Nothing [] - -{- | - This function hides the application of distinct on the SMT syntax - receives the solver and a list of the expressions which must be distinct and gives the corresponding SMT2Lib syntax. --} -assertDistinct :: Solver -> [Expr] -> IO GenResult -assertDistinct solver dexp = - assert solver (App (I (N "distinct") []) Nothing dexp) - -{- | - This function hides Integers on the SMT syntax receives a integer - and gives the corresponding SMT2Lib syntax. --} -literal :: Int -> Expr -literal a = Lit $ LitNum (read (show a) :: Integer) - - -{- | - This function allows the user to given a list of expressions make a - assert of them giving the SMTLib2 syntax corespondant (auxiliary function for maping). --} -mapAssert :: Solver -> [Expr] -> IO () -mapAssert _ [] = return () -mapAssert solver (a:as) = assert solver a >> mapAssert solver as - -{- | - This function when giving a solver and a function that gives an Expr and a list of the input type of that function, asserts the map of expressions its particulary useful to say that some set variables are all for example greater than zero. --} -maping :: Solver -> (a -> Expr) -> [a] -> IO () -maping solver expr a = mapAssert solver (map expr a) - -{- | - This function hides the name creation on the SMT syntax receives a string and gives the corresponding SMT2Lib syntax for declaring a function. --} -declFun :: Solver -> String -> [Type] -> Type -> IO GenResult -declFun solver name = declareFun solver (N name) - -defFun :: Solver -> String -> [Binder] -> Type -> Expr -> IO GenResult -defFun solver name = defineFun solver (N name) - - --- | This function binds a name to a type, and returns a Binder. -bind :: String -> Type -> Binder -bind name = Bind (N name) - -{- | - This function hides Constants implemnted as functions without arguments on the SMT syntax receives a String and a type and gives the corresponding SMT2Lib syntax for declaring a constant function. --} -declConst :: Solver -> String -> Type -> IO GenResult -declConst solver name = declareFun solver (N name) [] - -{- | - This function hides Constants implemnted as functions without arguments on the SMT syntax receives a String and a type and gives the corresponding SMT2Lib syntax for declaring a constant function. --} -mapDeclConst :: Solver -> [String] -> Type -> IO () -mapDeclConst _ [] _ = return () -mapDeclConst solver (x:xs) y = - declConst solver x y >> mapDeclConst solver xs y - - -{- | - This function hides the way to access an array (Hammered version) - on the SMT syntax receives a integer and gives the corresponding - SMT2Lib syntax. --} -getPos :: Show a => Solver -> String -> a -> IO GValResult -getPos solver arr pos= let name = arr ++ " " ++ show pos in - getValue solver [App (I (N name ) []) Nothing []] - --- | This function hides the Name Type in the declare type comand -declType :: Solver -> String -> Integer -> IO GenResult -declType sol name = declareType sol (N name) - - -{- | - This function simplifies the command to set the option - to Produce Models. --} -produceModels :: Solver -> IO GenResult -produceModels solver = setOption solver (OptProduceModels True) - --- | This function simplifies the command to set the option to Interactive Mode. -interactiveMode :: Solver -> IO GenResult -interactiveMode solver = setOption solver (OptInteractiveMode True) +{- | + Module: Hsmtlib.HighLevel + This Module provide auxiliar functions that simplify writing expressions + to send to the solver. +-} + +module Hsmtlib.HighLevel where + +import Hsmtlib.Solver as Slv +import SMTLib2 + + +{- | function that hides the creatinf of the quantifier forall-} +forall :: [Binder] -> Expr -> Expr +forall = Quant Forall + +{- | function that hides the creatinf of the quantifier exists-} +exists :: [Binder] -> Expr -> Expr +exists = Quant Exists + +{- | + This function hides the application of a function on the SMT syntax + receives the name of the function and the args and gives the corresponding + SMT2Lib syntax. +-} +fun :: String -> [Expr] -> Expr +fun name = App (I (N name) []) Nothing + + +{- | + This function hides the application of a constant function on the + SMT syntax receives the name of the function and gives the corresponding + SMT2Lib syntax, the function must be already declared using declareFun. +-} +ct :: String -> Expr +ct x = App (I (N x) []) Nothing [] + +{- | + This function hides the application of distinct on the SMT syntax + receives the solver and a list of the expressions which must be distinct and gives the corresponding SMT2Lib syntax. +-} +assertDistinct :: Solver -> [Expr] -> IO Result +assertDistinct solver dexp = + assert solver (App (I (N "distinct") []) Nothing dexp) + +{- | + This function hides Integers on the SMT syntax receives a integer + and gives the corresponding SMT2Lib syntax. +-} +lit :: Int -> Expr +lit a = Lit $ LitNum (read (show a) :: Integer) + + +{- | + This function allows the user to given a list of expressions make a + assert of them giving the SMTLib2 syntax corespondant (auxiliary function for maping). +-} +mapAssert :: Solver -> [Expr] -> IO () +mapAssert _ [] = return () +mapAssert solver (a:as) = assert solver a >> mapAssert solver as + +{- | + This function when giving a solver and a function that gives an Expr and a list of the input type of that function, asserts the map of expressions its particulary useful to say that some set variables are all for example greater than zero. +-} +maping :: Solver -> (a -> Expr) -> [a] -> IO () +maping solver expr a = mapAssert solver (map expr a) + +{- | + This function hides the name creation on the SMT syntax receives a string and gives the corresponding SMT2Lib syntax for declaring a function. +-} +declFun :: Solver -> String -> [Type] -> Type -> IO Result +declFun solver name = declareFun solver (N name) + +defFun :: Solver -> String -> [Binder] -> Type -> Expr -> IO Result +defFun solver name = defineFun solver (N name) + + +-- | This function binds a name to a type, and returns a Binder. +bind :: String -> Type -> Binder +bind name = Bind (N name) + +{- | + This function hides Constants implemnted as functions without arguments on the SMT syntax receives a String and a type and gives the corresponding SMT2Lib syntax for declaring a constant function. +-} +declConst :: Solver -> String -> Type -> IO Result +declConst solver name = declareFun solver (N name) [] + +{- | + This function hides Constants implemnted as functions without arguments on the SMT syntax receives a String and a type and gives the corresponding SMT2Lib syntax for declaring a constant function. +-} +mapDeclConst :: Solver -> [String] -> Type -> IO () +mapDeclConst _ [] _ = return () +mapDeclConst solver (x:xs) y = + declConst solver x y >> mapDeclConst solver xs y + + +{- | + This function hides the way to access an array (Hammered version) + on the SMT syntax receives a integer and gives the corresponding + SMT2Lib syntax. +-} +getPos :: Show a => Solver -> String -> a -> IO Result +getPos solver arr pos= let name = arr ++ " " ++ show pos in + getValue solver [App (I (N name ) []) Nothing []] + +-- | This function hides the Name Type in the declare type comand +declType :: Solver -> String -> Integer -> IO Result +declType sol name = declareType sol (N name) + + +{- | + This function simplifies the command to set the option + to Produce Models. +-} +produceModels :: Solver -> IO Result +produceModels solver = setOption solver (OptProduceModels True) + + +produceProofs :: Solver -> IO Result +produceProofs solver = setOption solver (OptProduceProofs True) + +-- | This function simplifies the command to set the option to Interactive Mode. +interactiveMode :: Solver -> IO Result +interactiveMode solver = setOption solver (OptInteractiveMode True) + diff --git a/Hsmtlib/Parsers/AuxParser.hs b/Hsmtlib/Parsers/AuxParser.hs new file mode 100644 --- /dev/null +++ b/Hsmtlib/Parsers/AuxParser.hs @@ -0,0 +1,116 @@ +module Hsmtlib.Parsers.AuxParser 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 + + +(<:>) :: Applicative f => f a -> f [a] -> f [a] +(<:>) a b = (:) <$> a <*> b + +(<++>) :: Applicative f => f [a] -> f [a] -> f [a] +(<++>) a b = (++) <$> a <*> b + + +-- 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" diff --git a/Hsmtlib/Parsers/ParseResponse.hs b/Hsmtlib/Parsers/ParseResponse.hs new file mode 100644 --- /dev/null +++ b/Hsmtlib/Parsers/ParseResponse.hs @@ -0,0 +1,321 @@ +module Hsmtlib.Parsers.ParseResponse where + +import Control.Applicative as Ctr hiding ((<|>)) +import Control.Monad +import Data.Functor.Identity +import Hsmtlib.Parsers.AuxParser +import Hsmtlib.Parsers.ParseScript +import Hsmtlib.Parsers.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 parseCmdGetAssertion + <|> 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 # + # # + ######################################################################### +-} + + +parseCmdGetAssertion :: ParsecT String u Identity CmdResponse +parseCmdGetAssertion = liftM CmdGetAssertionResponse parseGetAssertionResponse + + + +-- parse Get Assertion Response +parseGetAssertionResponse :: ParsecT String u Identity [Term] +parseGetAssertionResponse = 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 CmdGetUnsatCoreResoponse 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 # + # # + ######################################################################### +-} + diff --git a/Hsmtlib/Parsers/ParseScript.hs b/Hsmtlib/Parsers/ParseScript.hs new file mode 100644 --- /dev/null +++ b/Hsmtlib/Parsers/ParseScript.hs @@ -0,0 +1,840 @@ +module Hsmtlib.Parsers.ParseScript where + +import Control.Applicative as Ctr hiding ((<|>)) +import Control.Monad +import Data.Functor.Identity +import Hsmtlib.Parsers.AuxParser +import Hsmtlib.Parsers.Syntax +import Text.Parsec.Prim as Prim +import Text.ParserCombinators.Parsec as Pc + +teste :: IO () +teste = getLine >>= readFile >>= pt.parse parseSource "" + + +{- +run :: Source -> IO () +run source = do + solver <- startSolver Z3 Online Nothing Nothing + pint $ toSMTLib2 solver source +-} + +pt :: Either ParseError Source -> IO () +pt (Left err) = print err +pt (Right x) = pt' x + +pt' :: Source -> IO() +pt' = foldr (\ x -> (>>) (print x >> putStr "\n")) (return ()) + + +{- + ############################################´m############################# + # # + # 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 # + # # + ######################################################################### +-} + + +-- parseBool + +parseBool :: ParsecT String u Identity Bool +parseBool = (true *> return True) <|> (false *> return False) + + +parseOption :: ParsecT String u Identity Option +parseOption = parsePrintSuccess + <|> parseExpandDefinitions + <|> parseInteractiveMode + <|> parseProduceProofs + <|> parseProduceUnsatCores + <|> parseProduceModels + <|> parseProduceAssignments + <|> parseRegularOutputChannel + <|> parseDiagnosticOutputChannel + <|> parseRandomSeed + <|> parseVerbosity + <|> 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 + + + + +{- + ######################################################################### + # # + # 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 + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + diff --git a/Hsmtlib/Parsers/Syntax.hs b/Hsmtlib/Parsers/Syntax.hs new file mode 100644 --- /dev/null +++ b/Hsmtlib/Parsers/Syntax.hs @@ -0,0 +1,235 @@ +module Hsmtlib.Parsers.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 + | CmdGetAssertionResponse GetAssertion + | CmdGetAssignmentResponse GetAssignmentResponse + | CmdGetProofResponse GetProofResponse + | CmdGetUnsatCoreResoponse GetUnsatCoreResponse + | CmdGetValueResponse GetValueResponse + | CmdGetOptionResponse GetOptionResponse + deriving (Show, Eq) + + +-- Command Responses + + + +type GetAssertion = [Term] + +-- 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 + diff --git a/Hsmtlib/Parsers/Visualizer.hs b/Hsmtlib/Parsers/Visualizer.hs new file mode 100644 --- /dev/null +++ b/Hsmtlib/Parsers/Visualizer.hs @@ -0,0 +1,180 @@ +module Hsmtlib.Parsers.Visualizer where + +import Hsmtlib.Parsers.Syntax as S +import Data.List + + + + +spaces' :: Int -> Int -> String +spaces' n limit | n == limit = "" + | otherwise = " " ++ spaces' (n+1) limit + +spaces :: Int -> String +spaces = spaces' 0 + +branch' :: Int -> String +branch' nsp = "\n" ++ spaces nsp++"|\n" ++ spaces nsp ++ "|- " + +branchAr' :: Int -> String +branchAr' nsp = "\n" ++ spaces nsp ++"\n" ++ spaces (nsp+1) ++ "[" + +fbranch :: Int -> String -> String -> String +fbranch nsp mark fin = mark ++ branch' nsp ++ fin + +branch :: String -> (Int -> a -> String) -> Int -> a -> String +branch mark f nsp arg = mark ++ branch' nsp ++ f (nsp+3) arg + + +nLines :: String -> Int +nLines = length.lines + +mLines :: String ->Int -> String +mLines _ 0 = "" +mLines sps n = sps ++ "|\n" ++ mLines sps (n-1) + +showValuationPair :: Int -> ValuationPair-> String +showValuationPair nsp (ValuationPair t1 t2) = tup "ValP" nsp t1 t2 showTerm showTerm + +showSpecConstant :: SpecConstant -> String +showSpecConstant (SpecConstantNumeral int) = "Num " ++ show int +showSpecConstant (SpecConstantDecimal st) = "Dec " ++ st +showSpecConstant (SpecConstantHexadecimal st) = "Hex " ++ st +showSpecConstant (SpecConstantBinary it) = "Bin " ++ show it +showSpecConstant (SpecConstantString st) = "Str " ++ st + + +aTup :: String + -> Int + -> [a] + -> (Int -> a -> String) + -> String +aTup mark nsp arg f = + mark ++ " -[ " ++ hd ++ arr ++ endSpace++"]" + where + hd =f (nsp+8) (head arg) + bd = drop 1 arg + arr = backSpace ++ intercalate backSpace (fmap (f (nsp+8)) bd) + backSpace = "\n" ++ spaces (nsp+6) ++ ", " + endSpace = "\n" ++ spaces (nsp+6) + +dTup :: String + -> Int + -> String + -> a + -> (Int -> a -> String) + -> String +dTup mark nsp st arg f = + bMark ++ st ++ sndStr + where bMark = mark ++ branch' nsp + sndStr = branch' nsp ++ f (nsp+3) arg + +tup :: String + -> Int + -> a + -> b + -> (Int -> a -> String) + -> (Int -> b -> String) + -> String +tup mark nsp arg1 arg2 f1 f2 = + bMark ++ bf1 ++ bf2 + where bMark = mark ++ branch' nsp + bf1 = f1 (nsp+3) arg1 ++ "\n" ++ spaces nsp ++"|- " + bf2 = f2 (nsp+3) arg2 + + +tupArray :: String + -> Int + -> a + -> [b] + -> (Int -> a -> String) + -> (Int -> b -> String) + -> String +tupArray mark nsp arg1 arg2 f1 f2 = + mark ++ fstf ++ sndf + where fstf = "\n" ++spaces nsp ++ "|- " ++ f1 (nsp+3) arg1 + sndf ="\n" ++ spaces nsp ++ "|-[ " ++ hd ++ strs ++ endSpace + hd = f2 (nsp+5) (head arg2) ++ backSpace + bd = drop 1 arg2 + strs = intercalate backSpace (fmap (f2 (nsp+5)) bd) + backSpace = "\n" ++ spaces (nsp+2) ++ ", " + endSpace = "\n" ++ spaces (nsp+2) ++ "]" + +showQualIdentifier :: Int -> QualIdentifier -> String +showQualIdentifier nsp (QIdentifier qid) = branch "QI" showIdentifier nsp qid +showQualIdentifier nsp (QIdentifierAs iden srt) = + tup "QIAS" nsp iden srt showIdentifier showSort + + + +showSort :: Int -> Sort -> String +showSort nsp (SortId iden) = branch "SID" showIdentifier nsp iden +showSort nsp (SortIdentifiers iden sorts) = + tupArray "SIden" nsp iden sorts showIdentifier showSort + + + +showIdentifier :: Int -> Identifier -> String +showIdentifier _ (ISymbol st) = "IS " ++ st +showIdentifier nsp (I_Symbol str1 str2) = + "I_S" ++ fstr ++ sstr + where brc = "\n" ++ spaces nsp ++ "|\n" ++ spaces nsp + fstr = brc ++ "|- " ++ str1 + sstr = brc ++ "|- [ " ++hd ++ strs ++ end + hd = show ( head str2) ++ "\n" + bd = drop 1 str2 + strs = intercalate "\n" (fmap (\x ->((spaces (nsp + 3) ++ ", ")) ++ show x) bd) + end = "\n" ++ spaces (nsp+3) ++ "]" + + + + +showTerm ::Int -> Term -> String +showTerm nsp (TermSpecConstant sc) = + fbranch nsp "TSC" $ showSpecConstant sc +showTerm nsp (TermQualIdentifier qi) = + branch "TQI" showQualIdentifier nsp qi +showTerm nsp (TermQualIdentifierT qi ts) = + tupArray "TQIT" nsp qi ts showQualIdentifier showTerm +showTerm nsp (TermLet vb t) = + tupArray "TLt" nsp t vb showTerm showVarBinding +showTerm nsp (TermForall sv t) = + tupArray "TFA" nsp t sv showTerm showSortedVar +showTerm nsp (TermExists sv t) = + tupArray "TE" nsp t sv showTerm showSortedVar +showTerm nsp (TermAnnot t attrs) = + tupArray "TAN" nsp t attrs showTerm showAttribute + + + + + +showVarBinding :: Int -> VarBinding -> String +showVarBinding nsp (VB stg term) = dTup "VB" nsp stg term showTerm + +showSortedVar :: Int -> SortedVar -> String +showSortedVar nsp (SV stg st) = dTup "SV" nsp stg st showSort + +showAttribute :: Int -> Attribute -> String +showAttribute nsp (Attribute st) = fbranch nsp "Attribute" st +showAttribute nsp (AttributeVal stg av) = + dTup "AttrVal" nsp stg av showAttrValue + +showAttrValue :: Int -> AttrValue -> String +showAttrValue nsp (AttrValueConstant sc) = + fbranch nsp "AVC" $ showSpecConstant sc +showAttrValue nsp (AttrValueSymbol st) = + fbranch nsp "AVS" st +showAttrValue nsp (AttrValueSexpr sxpr) = + aTup "AVSP" nsp sxpr showSexpr + + +showSexpr :: Int -> Sexpr -> String +showSexpr nsp (SexprSpecConstant sc) = + fbranch nsp "SSC" $ showSpecConstant sc +showSexpr nsp (SexprSymbol st) = + fbranch nsp "SSymb" st +showSexpr nsp (SexprKeyword st) = + fbranch nsp "SK" st +showSexpr nsp (SexprSxp sexprs) = + aTup "SSxp" nsp sexprs showSexpr diff --git a/Hsmtlib/Solver.hs b/Hsmtlib/Solver.hs --- a/Hsmtlib/Solver.hs +++ b/Hsmtlib/Solver.hs @@ -1,130 +1,138 @@ -{- | -Module : Hsmtlib.Solver - This module has most types,data and functions that a user might need to - utilize the library. --} -module Hsmtlib.Solver where - -import Data.Map -import SMTLib2 - - - --- | Logics that can be passed to the start of the solver -data Logic = AUFLIA - | AUFLIRA - | AUFNIRA - | LRA - | QF_ABV - | QF_AUFBV - | QF_AUFLIA - | QF_AX - | QF_BV - | QF_IDL - | QF_LIA - | QF_LRA - | QF_NIA - | QF_NRA - | QF_RDL - | QF_UF - | QF_UFBV - | QF_UFIDL - | QF_UFLIA - | QF_UFLRA - | QF_UFNRA - | UFLRA - | UFNIA - deriving(Show) - - --- | Solvers that are currently supported. -data Solvers = Z3 | Cvc4 | Yices | Mathsat | Altergo | Boolector - - -{- | - Response from most commands that do not demand a feedback from the solver, - e.g: setLogic,push,pop... --} -data GenResult = Success -- ^ The command was successfully sent to the solver. - | Unsupported -- ^ The solver does not support the command. - | Error String -- ^ Some error occurred in the solver. - -- | Some error occurred parsing the response from the solver. - | GUError String - deriving (Show,Eq) - - - --- | Response from the command checkSat. -data SatResult = Sat -- ^ The solver has found a model. - | Unsat -- ^ The solver has established there is no model. - | Unknown -- ^ The search for a model was inconclusive. - -- Some error occurred parsing the response from the solver. - | SUError String - deriving (Show) - - - --- | Response from the command getValue -data GValResult = Res String Value -- ^ Name of the variable or function and result. - | VArrays Arrays -- ^ The result of arrays - | Results [GValResult] -- ^ Multiple results from multiple requestes. - | GVUError String -- ^ Some error occurred parsing the response from the solver. - deriving (Show) - - -{- | - When the value of an array or several values from diferent arrays are - requested with getValue then the value returned is a Map where the value - ís the name of the array, and the value is also a map. This inner map has - as value the position of the array and returned value. - Only integers are supported as values of arrays. --} -type Arrays = Map String (Map String Integer) - - --- | The type returned by getValue on constants or functions. -data Value = VInt Integer - | VRatio Rational - | VBool Bool - | VHex String - deriving (Show) - - - --- | Avaliable modes to use a solver. -data Mode = Online | Script | Batch - - -{- | - Alternative configuration of a solver which can be passed in the function - startSolver in 'Main' --} -data SolverConfig = Config - { path :: String - , args :: [String] - } - - --- | Solver data type that has all the functions. -data Solver = Solver - { setLogic :: Name -> IO GenResult - , setOption :: Option -> IO GenResult - , setInfo :: Attr -> IO GenResult - , declareType :: Name -> Integer -> IO GenResult - , defineType :: Name -> [Name] -> Type -> IO GenResult - , declareFun :: Name -> [Type] -> Type -> IO GenResult - , defineFun :: Name -> [Binder] -> Type -> Expr -> IO GenResult - , push :: Integer -> IO GenResult - , pop :: Integer -> IO GenResult - , assert :: Expr -> IO GenResult - , checkSat :: IO SatResult - , getAssertions :: IO String - , getValue :: [Expr] -> IO GValResult - , getProof :: IO String - , getUnsatCore :: IO String - , getInfo :: InfoFlag -> IO String - , getOption :: Name -> IO String - , exit :: IO String - } - | BSolver + + +{- | +Module : Hsmtlib.Solver + This module has most types,data and functions that a user might need to + utilize the library. +-} +module Hsmtlib.Solver where + +import Data.Map +import SMTLib2 +import Hsmtlib.Parsers.Syntax hiding(Option, Command) + + +-- | Logics that can be passed to the start of the solver +data Logic = AUFLIA + | AUFLIRA + | AUFNIRA + | LRA + | QF_ABV + | QF_AUFBV + | QF_AUFLIA + | QF_AX + | QF_BV + | QF_IDL + | QF_LIA + | QF_LRA + | QF_NIA + | QF_NRA + | QF_RDL + | QF_UF + | QF_UFBV + | QF_UFIDL + | QF_UFLIA + | QF_UFLRA + | QF_UFNRA + | UFLRA + | UFNIA + deriving(Show) + + +-- | Solvers that are currently supported. +data Solvers = Z3 | Cvc4 | Yices | Mathsat | Altergo | Boolector + + + + + +{-| Each response correspondes to it's respective command, + for example CGI correspondes to the command Get Info. + The Command CGR is the result for the command that dont return anything by default, for + example push or pop. What is returned by this command is if it was succefull or not. + +-} +data Result = CGR GenResponse + | CGI GetInfoResponse + | CCS CheckSatResponse + | CGAssert GetAssertion + | CGP GetProofResponse + | CGUC GetUnsatCoreResponse + | CGV [GValResult] + | CGAssig GetAssignmentResponse + | CGO GetOptionResponse + | ComError String -- ^ Error comunicating with the smt or Parsing + deriving (Show, Eq) + +-- | Name of the variable or function and result +data GValResult = Res String Value + -- | The result of arrays + | VArrays Arrays + -- | Multiple results from multiple requestes. + | Results [GValResult] + {-| + In case it can't turn the result + to one of the results above, + it return the syntax tree + -} + | Synt GetValueResponse + deriving (Show, Eq) + + +{- | + When the value of an array or several values from diferent arrays are + requested with getValue then the value returned is a Map where the value + ís the name of the array, and the value is also a map. This inner map has + as value the position of the array and returned value. + Only integers are supported as values of arrays. +-} +type Arrays = Map String (Map String Integer) + + + +-- | The type returned by getValue on constants or functions. +data Value = VInt Integer + | VRatio Rational + | VBool Bool + | VHex String + deriving (Show, Eq) + + + +-- | Avaliable modes to use a solver. +data Mode = Online | Script | Batch + + +{- | + Alternative configuration of a solver which can be passed in the function + startSolver in 'Main' +-} +data SolverConfig = Config + { path :: String + , args :: [String] + } + + +-- | Solver data type that has all the functions. +data Solver = Solver + { setLogic :: Name -> IO Result + , setOption :: Option -> IO Result + , setInfo :: Attr -> IO Result + , declareType :: Name -> Integer -> IO Result + , defineType :: Name -> [Name] -> Type -> IO Result + , declareFun :: Name -> [Type] -> Type -> IO Result + , defineFun :: Name -> [Binder] -> Type -> Expr -> IO Result + , push :: Integer -> IO Result + , pop :: Integer -> IO Result + , assert :: Expr -> IO Result + , checkSat :: IO Result + , getAssertions :: IO Result + , getValue :: [Expr] -> IO Result + , getProof :: IO Result + , getUnsatCore :: IO Result + , getInfo :: InfoFlag -> IO Result + , getOption :: Name -> IO Result + , exit :: IO Result + } + | BSolver { executeBatch :: [Command] -> IO String } diff --git a/Hsmtlib/Solvers/Altergo.hs b/Hsmtlib/Solvers/Altergo.hs --- a/Hsmtlib/Solvers/Altergo.hs +++ b/Hsmtlib/Solvers/Altergo.hs @@ -1,178 +1,223 @@ -{- | -Module : Hsmtlib.Solvers.Altergo - Module wich has the standard configuration for all altergo Modes and - provides the initilizing function. --} -module Hsmtlib.Solvers.Altergo(startAltErgo) where - -import Hsmtlib.Solver as Slv -import Hsmtlib.Solvers.Cmd.BatchCmd as B (executeBatch) -import Hsmtlib.Solvers.Cmd.OnlineCmd -import Hsmtlib.Solvers.Cmd.ProcCom.Process -import Hsmtlib.Solvers.Cmd.ScriptCmd -import SMTLib2 -import System.IO (Handle, - IOMode (WriteMode), - openFile) - - --- All the configurations are the same but have diferent names so if anything --- changes it's easy to alter its configuration. - - -altErgoConfigOnline :: SolverConfig -altErgoConfigOnline = - Config { path = "altergo" - , args = ["-v"] - } - -altErgoConfigScript :: SolverConfig -altErgoConfigScript = - Config { path = "altergo" - , args = ["-v"] - } - -altErgoConfigBatch :: SolverConfig -altErgoConfigBatch = - Config { path = "altergo" - , args = ["-v"] - } - - - -{- | - Function that initialyzes a altergo Solver. - It Receives a Mode, an SMT Logic, it can receive a diferent configuration - for the solver and an anternative path to create the script in Script Mode. - - In Online Mode if a FilePath is passed then it's ignored. --} -startAltErgo :: Mode - -> String - -> Maybe SolverConfig - -> Maybe FilePath - -> IO Solver - -startAltErgo Slv.Batch logic sConf _ = startAltErgoBatch logic sConf -startAltErgo Slv.Online logic sConf _ = startAltErgoOnline logic sConf -startAltErgo Slv.Script logic sConf scriptFilePath = - startAltErgoScript logic sConf scriptFilePath - --- Start altergo Online. - -startAltErgoOnline :: String -> Maybe SolverConfig -> IO Solver -startAltErgoOnline logic Nothing = - startAltErgoOnline' logic altErgoConfigOnline -startAltErgoOnline logic (Just conf) = startAltErgoOnline' logic conf - -startAltErgoOnline' :: String -> SolverConfig -> IO Solver -startAltErgoOnline' logic conf = do - -- Starts a Z4 Process. - process <- beginProcess (path conf) (args conf) - --Set Option to print success after accepting a Command. - onlineSetOption process (OptPrintSuccess True) - -- Sets the SMT Logic. - onlineSetLogic process (N logic) - -- Initialize the solver Functions and return them. - return $ onlineSolver process - ---Start altergo Script. - -startAltErgoScript :: String -> Maybe SolverConfig -> Maybe FilePath -> IO Solver -startAltErgoScript logic Nothing Nothing = - startAltErgoScript' logic altErgoConfigScript "temp.smt2" -startAltErgoScript logic (Just conf) Nothing = - startAltErgoScript' logic conf "temp.smt2" -startAltErgoScript logic Nothing (Just scriptFilePath) = - startAltErgoScript' logic altErgoConfigScript scriptFilePath -startAltErgoScript logic (Just conf) (Just scriptFilePath) = - startAltErgoScript' logic conf scriptFilePath - -{- - In this function a file is created where the commands are kept. - - Every function in the ScriptCmd Module needs a ScriptConf data which has: - - - sHandle: The handle of the script file - - sCmdPath: The Path to initilyze the solver - - sArgs: The options of the solver - - sFilePath: The file path of the script so it can be passed to the solver - when started. --} -startAltErgoScript' :: String -> SolverConfig -> FilePath -> IO Solver -startAltErgoScript' logic conf scriptFilePath = do - scriptHandle <- openFile scriptFilePath WriteMode - let srcmd = newScriptArgs conf scriptHandle scriptFilePath - scriptSetOption srcmd (OptPrintSuccess True) - scriptSetLogic srcmd (N logic) - return $ scriptSolver srcmd - ---Function which creates the ScriptConf for the script functions. -newScriptArgs :: SolverConfig -> Handle -> FilePath -> ScriptConf -newScriptArgs solverConfig nHandle scriptFilePath = - ScriptConf { sHandle = nHandle - , sCmdPath = path solverConfig - , sArgs = args solverConfig - , sFilePath = scriptFilePath - } - --- start Alt-Ergo Batch -startAltErgoBatch :: String -> Maybe SolverConfig -> IO Solver -startAltErgoBatch logic Nothing = startAltErgoBatch' logic altErgoConfigBatch -startAltErgoBatch logic (Just conf) = startAltErgoBatch' logic conf - -startAltErgoBatch' :: String -> SolverConfig -> IO Solver -startAltErgoBatch' logic config = return $ batchSolver logic config - - --- Creates the functions for online mode with the process already running. --- Each function will send the command to the solver and wait for the response. -onlineSolver :: Process -> Solver -onlineSolver process = - Solver { setLogic = onlineSetLogic process - , setOption = onlineSetOption process - , setInfo = onlineSetInfo process - , declareType = onlineDeclareType process - , defineType = onlineDefineType process - , declareFun = onlineDeclareFun process - , defineFun = onlineDefineFun process - , push = onlinePush process - , pop = onlinePop process - , assert = onlineAssert process - , checkSat = onlineCheckSat process - , getAssertions = onlineGetAssertions process - , getValue = onlineGetValue process - , getProof = onlineGetProof process - , getUnsatCore = onlineGetUnsatCore process - , getInfo = onlineGetInfo process - , getOption = onlineGetOption process - , exit = onlineExit process - } - --- Creates the funtion for the script mode. --- The configuration of the file is passed. -scriptSolver :: ScriptConf -> Solver -scriptSolver srcmd = - Solver { setLogic = scriptSetLogic srcmd - , setOption = scriptSetOption srcmd - , setInfo = scriptSetInfo srcmd - , declareType = scriptDeclareType srcmd - , defineType = scriptDefineType srcmd - , declareFun = scriptDeclareFun srcmd - , defineFun = scriptDefineFun srcmd - , push = scriptPush srcmd - , pop = scriptPop srcmd - , assert = scriptAssert srcmd - , checkSat = scriptCheckSat srcmd - , getAssertions = scriptGetAssertions srcmd - , getValue = scriptGetValue srcmd - , getProof = scriptGetProof srcmd - , getUnsatCore = scriptGetUnsatCore srcmd - , getInfo = scriptGetInfo srcmd - , getOption = scriptGetOption srcmd - , exit = scriptExit srcmd - } - -batchSolver :: String -> SolverConfig -> Solver -batchSolver logic config = - BSolver { Slv.executeBatch = B.executeBatch (path config) (args config) logic} +{- | +Module : Hsmtlib.Solvers.Altergo + Module wich has the standard configuration for all altergo Modes and + provides the initilizing function. +-} +module Hsmtlib.Solvers.Altergo(startAltErgo) where + +import Hsmtlib.Solver as Slv +import Hsmtlib.Solvers.Cmd.BatchCmd as B (executeBatch) +import Hsmtlib.Solvers.Cmd.OnlineCmd +import Hsmtlib.Solvers.Cmd.ProcCom.Process +import Hsmtlib.Solvers.Cmd.ScriptCmd +import SMTLib2 +import System.IO (Handle, + IOMode (WriteMode), + openFile) +import Control.Applicative as Ctr hiding ((<|>)) +import Control.Monad +import Data.Functor.Identity +import Hsmtlib.Parsers.AuxParser +import Hsmtlib.Parsers.ParseScript +import Hsmtlib.Parsers.Syntax as CmdRsp +import Text.Parsec.Prim as Prim +import Text.ParserCombinators.Parsec as Pc + + +-- All the configurations are the same but have diferent names so if anything +-- changes it's easy to alter its configuration. + + +altErgoConfigOnline :: SolverConfig +altErgoConfigOnline = + Config { path = "altergo" + , args = ["-v"] + } + +altErgoConfigScript :: SolverConfig +altErgoConfigScript = + Config { path = "altergo" + , args = ["-v"] + } + +altErgoConfigBatch :: SolverConfig +altErgoConfigBatch = + Config { path = "altergo" + , args = ["-v"] + } + + + +{- | + Function that initialyzes a altergo Solver. + It Receives a Mode, an SMT Logic, it can receive a diferent configuration + for the solver and an anternative path to create the script in Script Mode. + + In Online Mode if a FilePath is passed then it's ignored. +-} +startAltErgo :: Mode + -> String + -> Maybe SolverConfig + -> Maybe FilePath + -> IO Solver + +startAltErgo Slv.Batch logic sConf _ = startAltErgoBatch logic sConf +startAltErgo Slv.Online logic sConf _ = startAltErgoOnline logic sConf +startAltErgo Slv.Script logic sConf scriptFilePath = + startAltErgoScript logic sConf scriptFilePath + +-- Start altergo Online. + +startAltErgoOnline :: String -> Maybe SolverConfig -> IO Solver +startAltErgoOnline logic Nothing = + startAltErgoOnline' logic altErgoConfigOnline +startAltErgoOnline logic (Just conf) = startAltErgoOnline' logic conf + +startAltErgoOnline' :: String -> SolverConfig -> IO Solver +startAltErgoOnline' logic conf = do + -- Starts a Z4 Process. + process <- beginProcess (path conf) (args conf) + --Set Option to print success after accepting a Command. + _ <- onlineSetOption Altergo process (OptPrintSuccess True) + -- Sets the SMT Logic. + _ <- onlineSetLogic Altergo process (N logic) + -- Initialize the solver Functions and return them. + return $ onlineSolver process + +--Start altergo Script. + +startAltErgoScript :: String -> Maybe SolverConfig -> Maybe FilePath -> IO Solver +startAltErgoScript logic Nothing Nothing = + startAltErgoScript' logic altErgoConfigScript "temp.smt2" +startAltErgoScript logic (Just conf) Nothing = + startAltErgoScript' logic conf "temp.smt2" +startAltErgoScript logic Nothing (Just scriptFilePath) = + startAltErgoScript' logic altErgoConfigScript scriptFilePath +startAltErgoScript logic (Just conf) (Just scriptFilePath) = + startAltErgoScript' logic conf scriptFilePath + +{- + In this function a file is created where the commands are kept. + + Every function in the ScriptCmd Module needs a ScriptConf data which has: + + - sHandle: The handle of the script file + - sCmdPath: The Path to initilyze the solver + - sArgs: The options of the solver + - sFilePath: The file path of the script so it can be passed to the solver + when started. +-} +startAltErgoScript' :: String -> SolverConfig -> FilePath -> IO Solver +startAltErgoScript' logic conf scriptFilePath = do + scriptHandle <- openFile scriptFilePath WriteMode + let srcmd = newScriptArgs conf scriptHandle scriptFilePath + _ <- scriptSetOption srcmd (OptPrintSuccess True) + _ <- scriptSetLogic srcmd (N logic) + return $ scriptSolver srcmd + +--Function which creates the ScriptConf for the script functions. +newScriptArgs :: SolverConfig -> Handle -> FilePath -> ScriptConf +newScriptArgs solverConfig nHandle scriptFilePath = + ScriptConf { sHandle = nHandle + , sCmdPath = path solverConfig + , sArgs = args solverConfig + , sFilePath = scriptFilePath + } + +-- start Alt-Ergo Batch +startAltErgoBatch :: String -> Maybe SolverConfig -> IO Solver +startAltErgoBatch logic Nothing = startAltErgoBatch' logic altErgoConfigBatch +startAltErgoBatch logic (Just conf) = startAltErgoBatch' logic conf + +startAltErgoBatch' :: String -> SolverConfig -> IO Solver +startAltErgoBatch' logic config = return $ batchSolver logic config + +-- parsing the results of altergo's checksat in online mode (not compliant) + +parseCheckSatResponseAlt :: ParsecT String u Identity CheckSatResponse +parseCheckSatResponseAlt = + (string "sat" >> return Sat) <|> + (string "unsat" >> return Unsat) <|> + (string "unknown (sat)" >> return Unknown) + +parseCmdCheckSatResponseAlt :: ParsecT String u Identity CmdResponse +parseCmdCheckSatResponseAlt = liftM CmdCheckSatResponse parseCheckSatResponseAlt + +onlineCheckSatAlt ::Solvers -> Process -> IO Result +onlineCheckSatAlt solver proc = + onlineCheckSatResponseAlt proc CmdCheckSat solver + + +onlineCheckSatResponseAlt :: Process -> SMTLib2.Command -> Solvers -> IO Result +onlineCheckSatResponseAlt proc cmd solver = + liftA checkSatResponseAlt (onlineFun proc cmd solver) + +checkSatResponseAlt :: String -> Result +checkSatResponseAlt stg = + case result of + Left err -> ComError $ stg ++ " | " ++ show err + Right cmdRep -> CCS cmdRep + where result = parse parseCheckSatResponseAlt "" stg + +-- parsing the results of altergo's checksat in script mode (not compliant) + +scriptCheckSatResponseAlt :: ScriptConf -> SMTLib2.Command -> IO Result +scriptCheckSatResponseAlt conf cmd = + liftA checkSatResponseAlt (scriptFunExec conf cmd) + +scriptCheckSatAlt :: ScriptConf -> IO Result +scriptCheckSatAlt sConf = scriptCheckSatResponseAlt sConf CmdCheckSat + + + +-- Creates the functions for online mode with the process already running. +-- Each function will send the command to the solver and wait for the response. +onlineSolver :: Process -> Solver +onlineSolver process = + Solver { setLogic = onlineSetLogic Altergo process + , setOption = onlineSetOption Altergo process + , setInfo = onlineSetInfo Altergo process + , declareType = onlineDeclareType Altergo process + , defineType = onlineDefineType Altergo process + , declareFun = onlineDeclareFun Altergo process + , defineFun = onlineDefineFun Altergo process + , push = onlinePush Altergo process + , pop = onlinePop Altergo process + , assert = onlineAssert Altergo process + , checkSat = onlineCheckSatAlt Altergo process + , getAssertions = onlineGetAssertions Altergo process + , getValue = onlineGetValue Altergo process + , getProof = onlineGetProof Altergo process + , getUnsatCore = onlineGetUnsatCore Altergo process + , getInfo = onlineGetInfo Altergo process + , getOption = onlineGetOption Altergo process + , exit = onlineExit process + } + +-- Creates the funtion for the script mode. +-- The configuration of the file is passed. +scriptSolver :: ScriptConf -> Solver +scriptSolver srcmd = + Solver { setLogic = scriptSetLogic srcmd + , setOption = scriptSetOption srcmd + , setInfo = scriptSetInfo srcmd + , declareType = scriptDeclareType srcmd + , defineType = scriptDefineType srcmd + , declareFun = scriptDeclareFun srcmd + , defineFun = scriptDefineFun srcmd + , push = scriptPush srcmd + , pop = scriptPop srcmd + , assert = scriptAssert srcmd + , checkSat = scriptCheckSatAlt srcmd + , getAssertions = scriptGetAssertions srcmd + , getValue = scriptGetValue srcmd + , getProof = scriptGetProof srcmd + , getUnsatCore = scriptGetUnsatCore srcmd + , getInfo = scriptGetInfo srcmd + , getOption = scriptGetOption srcmd + , exit = scriptExit srcmd + } + +batchSolver :: String -> SolverConfig -> Solver +batchSolver logic config = + BSolver { Slv.executeBatch = B.executeBatch (path config) (args config) logic} diff --git a/Hsmtlib/Solvers/Boolector.hs b/Hsmtlib/Solvers/Boolector.hs --- a/Hsmtlib/Solvers/Boolector.hs +++ b/Hsmtlib/Solvers/Boolector.hs @@ -1,176 +1,176 @@ -{- | -Module : Hsmtlib.Solvers.Boolector - Module wich has the standard configuration for all boolector Modes and - provides the initilizing function. --} -module Hsmtlib.Solvers.Boolector(startBoolector) where - -import Hsmtlib.Solver as Slv -import Hsmtlib.Solvers.Cmd.BatchCmd as B (executeBatch) -import Hsmtlib.Solvers.Cmd.OnlineCmd -import Hsmtlib.Solvers.Cmd.ProcCom.Process -import Hsmtlib.Solvers.Cmd.ScriptCmd -import SMTLib2 -import System.IO (Handle, - IOMode (WriteMode), - openFile) - --- All the configurations are the same but have diferent names so if anything --- changes it's easy to alter its configuration. - - -boolectorConfigOnline :: SolverConfig -boolectorConfigOnline = - Config { path = "boolector" - , args = ["--smt2", "-d2", "-o STDOUT"] - } - -boolectorConfigScript :: SolverConfig -boolectorConfigScript = - Config { path = "boolector" - , args = ["--smt2", "-d2", "-o STDOUT"] - } - -boolectorConfigBatch :: SolverConfig -boolectorConfigBatch = - Config { path = "boolector" - , args = ["--smt2", "-d2", "-o STDOUT"] - } - - -{- | - Function that initialyzes a boolector Solver. - It Receives a Mode, an SMT Logic, it can receive a diferent configuration - for the solver and an anternative path to create the script in Script Mode. - - In Online Mode if a FilePath is passed then it's ignored. --} -startBoolector :: Mode - -> String - -> Maybe SolverConfig - -> Maybe FilePath - -> IO Solver - -startBoolector Slv.Batch logic sConf _ = startBoolectorBatch logic sConf -startBoolector Slv.Online logic sConf _ = startBoolectorOnline logic sConf -startBoolector Slv.Script logic sConf scriptFilePath = - startBoolectorScript logic sConf scriptFilePath - --- Start boolector Online. - -startBoolectorOnline :: String -> Maybe SolverConfig -> IO Solver -startBoolectorOnline logic Nothing = startBoolectorOnline' logic boolectorConfigOnline -startBoolectorOnline logic (Just conf) = startBoolectorOnline' logic conf - -startBoolectorOnline' :: String -> SolverConfig -> IO Solver -startBoolectorOnline' logic conf = do - -- Starts a Z4 Process. - process <- beginProcess (path conf) (args conf) - --Set Option to print success after accepting a Command. - --onlineSetOption process (OptPrintSuccess True) - -- Sets the SMT Logic. - onlineSetLogic process (N logic) - -- Initialize the solver Functions and return them. - return $ onlineSolver process - ---Start boolector Script. - -startBoolectorScript :: String -> Maybe SolverConfig -> Maybe FilePath -> IO Solver -startBoolectorScript logic Nothing Nothing = - startBoolectorScript' logic boolectorConfigScript "temp.smt2" -startBoolectorScript logic (Just conf) Nothing = - startBoolectorScript' logic conf "temp.smt2" -startBoolectorScript logic Nothing (Just scriptFilePath) = - startBoolectorScript' logic boolectorConfigScript scriptFilePath -startBoolectorScript logic (Just conf) (Just scriptFilePath) = - startBoolectorScript' logic conf scriptFilePath - -{- - In this function a file is created where the commands are kept. - - Every function in the ScriptCmd Module needs a ScriptConf data which has: - - - sHandle: The handle of the script file - - sCmdPath: The Path to initilyze the solver - - sArgs: The options of the solver - - sFilePath: The file path of the script so it can be passed to the solver - when started. --} -startBoolectorScript' :: String -> SolverConfig -> FilePath -> IO Solver -startBoolectorScript' logic conf scriptFilePath = do - scriptHandle <- openFile scriptFilePath WriteMode - let srcmd = newScriptArgs conf scriptHandle scriptFilePath - scriptSetOption srcmd (OptPrintSuccess True) - scriptSetLogic srcmd (N logic) - return $ scriptSolver srcmd - ---Function which creates the ScriptConf for the script functions. -newScriptArgs :: SolverConfig -> Handle -> FilePath -> ScriptConf -newScriptArgs solverConfig nHandle scriptFilePath = - ScriptConf { sHandle = nHandle - , sCmdPath = path solverConfig - , sArgs = args solverConfig - , sFilePath = scriptFilePath - } - --- Start Booleactor batch -startBoolectorBatch :: String -> Maybe SolverConfig -> IO Solver -startBoolectorBatch logic Nothing = - startBoolectorBatch' logic boolectorConfigBatch -startBoolectorBatch logic (Just conf) = startBoolectorBatch' logic conf - -startBoolectorBatch' :: String -> SolverConfig -> IO Solver -startBoolectorBatch' logic conf = return $ batchSolver logic conf - - --- Creates the functions for online mode with the process already running. --- Each function will send the command to the solver and wait for the response. -onlineSolver :: Process -> Solver -onlineSolver process = - Solver { setLogic = onlineSetLogic process - , setOption = onlineSetOption process - , setInfo = onlineSetInfo process - , declareType = onlineDeclareType process - , defineType = onlineDefineType process - , declareFun = onlineDeclareFun process - , defineFun = onlineDefineFun process - , push = onlinePush process - , pop = onlinePop process - , assert = onlineAssert process - , checkSat = onlineCheckSat process - , getAssertions = onlineGetAssertions process - , getValue = onlineGetValue process - , getProof = onlineGetProof process - , getUnsatCore = onlineGetUnsatCore process - , getInfo = onlineGetInfo process - , getOption = onlineGetOption process - , exit = onlineExit process - } - --- Creates the funtion for the script mode. --- The configuration of the file is passed. -scriptSolver :: ScriptConf -> Solver -scriptSolver srcmd = - Solver { setLogic = scriptSetLogic srcmd - , setOption = scriptSetOption srcmd - , setInfo = scriptSetInfo srcmd - , declareType = scriptDeclareType srcmd - , defineType = scriptDefineType srcmd - , declareFun = scriptDeclareFun srcmd - , defineFun = scriptDefineFun srcmd - , push = scriptPush srcmd - , pop = scriptPop srcmd - , assert = scriptAssert srcmd - , checkSat = scriptCheckSat srcmd - , getAssertions = scriptGetAssertions srcmd - , getValue = scriptGetValue srcmd - , getProof = scriptGetProof srcmd - , getUnsatCore = scriptGetUnsatCore srcmd - , getInfo = scriptGetInfo srcmd - , getOption = scriptGetOption srcmd - , exit = scriptExit srcmd - } - -batchSolver :: String -> SolverConfig -> Solver -batchSolver logic config = - BSolver { Slv.executeBatch = B.executeBatch (path config) (args config) logic} +{- | +Module : Hsmtlib.Solvers.Boolector + Module wich has the standard configuration for all boolector Modes and + provides the initilizing function. +-} +module Hsmtlib.Solvers.Boolector(startBoolector) where + +import Hsmtlib.Solver as Slv +import Hsmtlib.Solvers.Cmd.BatchCmd as B (executeBatch) +import Hsmtlib.Solvers.Cmd.OnlineCmd +import Hsmtlib.Solvers.Cmd.ProcCom.Process +import Hsmtlib.Solvers.Cmd.ScriptCmd +import SMTLib2 +import System.IO (Handle, + IOMode (WriteMode), + openFile) + +-- All the configurations are the same but have diferent names so if anything +-- changes it's easy to alter its configuration. + + +boolectorConfigOnline :: SolverConfig +boolectorConfigOnline = + Config { path = "boolector" + , args = ["--smt2", "-d2", "-o STDOUT"] + } + +boolectorConfigScript :: SolverConfig +boolectorConfigScript = + Config { path = "boolector" + , args = ["--smt2", "-d2", "-o STDOUT"] + } + +boolectorConfigBatch :: SolverConfig +boolectorConfigBatch = + Config { path = "boolector" + , args = ["--smt2", "-d2", "-o STDOUT"] + } + + +{- | + Function that initialyzes a boolector Solver. + It Receives a Mode, an SMT Logic, it can receive a diferent configuration + for the solver and an anternative path to create the script in Script Mode. + + In Online Mode if a FilePath is passed then it's ignored. +-} +startBoolector :: Mode + -> String + -> Maybe SolverConfig + -> Maybe FilePath + -> IO Solver + +startBoolector Slv.Batch logic sConf _ = startBoolectorBatch logic sConf +startBoolector Slv.Online logic sConf _ = startBoolectorOnline logic sConf +startBoolector Slv.Script logic sConf scriptFilePath = + startBoolectorScript logic sConf scriptFilePath + +-- Start boolector Online. + +startBoolectorOnline :: String -> Maybe SolverConfig -> IO Solver +startBoolectorOnline logic Nothing = startBoolectorOnline' logic boolectorConfigOnline +startBoolectorOnline logic (Just conf) = startBoolectorOnline' logic conf + +startBoolectorOnline' :: String -> SolverConfig -> IO Solver +startBoolectorOnline' logic conf = do + -- Starts a Z4 Process. + process <- beginProcess (path conf) (args conf) + --Set Option to print success after accepting a Command. + --onlineSetOption process (OptPrintSuccess True) + -- Sets the SMT Logic. + _ <- onlineSetLogic Boolector process (N (show logic)) + -- Initialize the solver Functions and return them. + return $ onlineSolver process + +--Start boolector Script. + +startBoolectorScript :: String -> Maybe SolverConfig -> Maybe FilePath -> IO Solver +startBoolectorScript logic Nothing Nothing = + startBoolectorScript' logic boolectorConfigScript "temp.smt2" +startBoolectorScript logic (Just conf) Nothing = + startBoolectorScript' logic conf "temp.smt2" +startBoolectorScript logic Nothing (Just scriptFilePath) = + startBoolectorScript' logic boolectorConfigScript scriptFilePath +startBoolectorScript logic (Just conf) (Just scriptFilePath) = + startBoolectorScript' logic conf scriptFilePath + +{- + In this function a file is created where the commands are kept. + + Every function in the ScriptCmd Module needs a ScriptConf data which has: + + - sHandle: The handle of the script file + - sCmdPath: The Path to initilyze the solver + - sArgs: The options of the solver + - sFilePath: The file path of the script so it can be passed to the solver + when started. +-} +startBoolectorScript' :: String -> SolverConfig -> FilePath -> IO Solver +startBoolectorScript' logic conf scriptFilePath = do + scriptHandle <- openFile scriptFilePath WriteMode + let srcmd = newScriptArgs conf scriptHandle scriptFilePath + _ <- scriptSetOption srcmd (OptPrintSuccess True) + _ <- scriptSetLogic srcmd (N logic) + return $ scriptSolver srcmd + +--Function which creates the ScriptConf for the script functions. +newScriptArgs :: SolverConfig -> Handle -> FilePath -> ScriptConf +newScriptArgs solverConfig nHandle scriptFilePath = + ScriptConf { sHandle = nHandle + , sCmdPath = path solverConfig + , sArgs = args solverConfig + , sFilePath = scriptFilePath + } + +-- Start Booleactor batch +startBoolectorBatch :: String -> Maybe SolverConfig -> IO Solver +startBoolectorBatch logic Nothing = + startBoolectorBatch' logic boolectorConfigBatch +startBoolectorBatch logic (Just conf) = startBoolectorBatch' logic conf + +startBoolectorBatch' :: String -> SolverConfig -> IO Solver +startBoolectorBatch' logic conf = return $ batchSolver logic conf + + +-- Creates the functions for online mode with the process already running. +-- Each function will send the command to the solver and wait for the response. +onlineSolver :: Process -> Solver +onlineSolver process = + Solver { setLogic = onlineSetLogic Boolector process + , setOption = onlineSetOption Boolector process + , setInfo = onlineSetInfo Boolector process + , declareType = onlineDeclareType Boolector process + , defineType = onlineDefineType Boolector process + , declareFun = onlineDeclareFun Boolector process + , defineFun = onlineDefineFun Boolector process + , push = onlinePush Boolector process + , pop = onlinePop Boolector process + , assert = onlineAssert Boolector process + , checkSat = onlineCheckSat Boolector process + , getAssertions = onlineGetAssertions Boolector process + , getValue = onlineGetValue Boolector process + , getProof = onlineGetProof Boolector process + , getUnsatCore = onlineGetUnsatCore Boolector process + , getInfo = onlineGetInfo Boolector process + , getOption = onlineGetOption Boolector process + , exit = onlineExit process + } + +-- Creates the funtion for the script mode. +-- The configuration of the file is passed. +scriptSolver :: ScriptConf -> Solver +scriptSolver srcmd = + Solver { setLogic = scriptSetLogic srcmd + , setOption = scriptSetOption srcmd + , setInfo = scriptSetInfo srcmd + , declareType = scriptDeclareType srcmd + , defineType = scriptDefineType srcmd + , declareFun = scriptDeclareFun srcmd + , defineFun = scriptDefineFun srcmd + , push = scriptPush srcmd + , pop = scriptPop srcmd + , assert = scriptAssert srcmd + , checkSat = scriptCheckSat srcmd + , getAssertions = scriptGetAssertions srcmd + , getValue = scriptGetValue srcmd + , getProof = scriptGetProof srcmd + , getUnsatCore = scriptGetUnsatCore srcmd + , getInfo = scriptGetInfo srcmd + , getOption = scriptGetOption srcmd + , exit = scriptExit srcmd + } + +batchSolver :: String -> SolverConfig -> Solver +batchSolver logic config = + BSolver { Slv.executeBatch = B.executeBatch (path config) (args config) logic} diff --git a/Hsmtlib/Solvers/Cmd/BatchCmd.hs b/Hsmtlib/Solvers/Cmd/BatchCmd.hs --- a/Hsmtlib/Solvers/Cmd/BatchCmd.hs +++ b/Hsmtlib/Solvers/Cmd/BatchCmd.hs @@ -1,19 +1,19 @@ -module Hsmtlib.Solvers.Cmd.BatchCmd(executeBatch) where - -import Data.List (intercalate) -import Hsmtlib.Solvers.Cmd.ProcCom.Process (Args, CmdPath, - sendContext) -import SMTLib2 (Command (CmdSetLogic), - Name (N), pp) -import Text.PrettyPrint (Doc, render) - - -setLogic :: String -> Command -setLogic logic = CmdSetLogic (N logic) - - -executeBatch :: CmdPath -> Args -> String -> [Command]-> IO String -executeBatch cmd args logic script = - sendContext cmd args result - where fScript = setLogic logic : script - result = intercalate "\n" $ fmap (render.(pp :: Command -> Doc)) fScript +module Hsmtlib.Solvers.Cmd.BatchCmd(executeBatch) where + +import Data.List (intercalate) +import Hsmtlib.Solvers.Cmd.ProcCom.Process (Args, CmdPath, + sendContext) +import SMTLib2 (Command (CmdSetLogic), + Name (N), pp) +import Text.PrettyPrint (Doc, render) + + +setLogic :: String -> Command +setLogic logic = CmdSetLogic (N logic) + + +executeBatch :: CmdPath -> Args -> String -> [Command]-> IO String +executeBatch cmd args logic script = + sendContext cmd args result + where fScript = setLogic logic : script + result = intercalate "\n" $ fmap (render.(pp :: Command -> Doc)) fScript diff --git a/Hsmtlib/Solvers/Cmd/CmdResult.hs b/Hsmtlib/Solvers/Cmd/CmdResult.hs new file mode 100644 --- /dev/null +++ b/Hsmtlib/Solvers/Cmd/CmdResult.hs @@ -0,0 +1,237 @@ +module Hsmtlib.Solvers.Cmd.CmdResult where + +import Control.Applicative ((<|>)) +import Control.Monad +--import Data.List (intercalate) +import Data.Map as M +import Data.Maybe (isJust) +import Hsmtlib.Parsers.ParseResponse +import Hsmtlib.Parsers.Syntax as S +import Hsmtlib.Solver as Solv +import Hsmtlib.Solvers.Cmd.ResultHelpers +import Prelude as P +import Text.ParserCombinators.Parsec.Prim (parse) + + + +{- + ######################################################################### + # # + # Gen Response # + # # + ######################################################################### +-} + + + +genResponse :: String -> Result +genResponse stg = + case result of + Left err -> ComError $ stg ++ " | " ++ show err + Right cmdRep -> CGR cmdRep + where result = parse parseGenResponse "" stg + + + + +{- + ######################################################################### + # # + # Check Sat Response # + # # + ######################################################################### +-} + +checkSatResponse :: String -> Result +checkSatResponse stg = + case result of + Left err -> ComError $ stg ++ " | " ++ show err + Right cmdRep -> CCS cmdRep + where result = parse parseCheckSatResponse "" stg + + + + +{- + ######################################################################### + # # + # get Value Respose # + # # + ######################################################################### +-} + + + +{- +getValueResponse :: String -> GValResult +getValueResponse stg = GVUError $ stg ++ "\n" ++ tree + where result = parse parseGetValueResponse "" stg + tree = getVR' result + + +getVR' :: Show a => Either a [ValuationPair] -> String +getVR' result = + case result of + Left err -> show err + Right vals -> intercalate "\n" (fmap (showValuationPair 0) vals) + +-} + +getValueResponse :: String -> Result +getValueResponse stg = case result of + Left err -> ComError $ stg ++ " | " ++ show err + Right vals -> getValResponse vals + where result = parse parseGetValueResponse "" stg + + + +getValResponse::[ValuationPair] -> Result +getValResponse vp = CGV $ arrays ++ [errors] + -- gets the results in a Maybe GValResult. + where res = getValResponses vp + --Produes UErrors from the results that gave Nothing. + errors = Synt $ valErrors' vp res + cRes = P.filter isJust res -- Removes the Nothings. + -- Joins all arrays in one and + --removes the Just from all results. + arrays = joinArrays cRes + + + +valErrors' :: [ValuationPair] -> [Maybe GValResult] -> [ValuationPair] +valErrors' [] [] = [] +valErrors' [] (_:_) = [] +valErrors' (_:_) [] = [] +valErrors' (x:xs) (Nothing:gs) = + x : valErrors' xs gs +valErrors' (_:xs) (_:gs) = valErrors' xs gs + + + +joinArrays :: [Maybe GValResult] -> [GValResult] +joinArrays = joinArrays' $ VArrays empty + + +joinArrays' :: GValResult -> [Maybe GValResult] -> [GValResult] +-- if there was no array in the result then don't put an empty one. +joinArrays' (VArrays n) [] | M.null n = [] + | otherwise = [VArrays n] +joinArrays' res (x:xs) = case nVal of + (VArrays _) -> joinArrays' nVal xs + _ -> nVal : joinArrays' res xs + where nVal = checkGVal res x +joinArrays' _ _ = [] + +checkGVal :: GValResult -> Maybe GValResult -> GValResult +checkGVal (VArrays oarr) (Just(VArrays arr)) = + VArrays $ unionWith union oarr arr +checkGVal _ (Just x) = x +checkGVal _ _ = VArrays empty + + +getValResponses :: [ValuationPair] -> [Maybe GValResult] +getValResponses = fmap getGValResult + +getGValResult :: ValuationPair -> Maybe GValResult +getGValResult vp = getVar vp + <|> getArray vp + <|> getFun vp + <|> getBitVec vp + + +{- + ######################################################################### + # # + # get Info Response # + # # + ######################################################################### +-} + +getInfoResponse :: String -> Result +getInfoResponse stg = case result of + Left err -> ComError $ stg ++ " | " ++ show err + Right vals -> CGI vals + where result = parse parseGetInfoResponse "" stg + + +{- + ######################################################################### + # # + # get Assertion response # + # # + ######################################################################### +-} + + +getAssertionResponse :: String -> Result +getAssertionResponse stg = case result of + Left err -> ComError $ stg ++ " | " ++ show err + Right vals -> CGAssert vals + where result = parse parseGetAssertionResponse "" stg + + + +{- + ######################################################################### + # # + # get Proof response # + # # + ######################################################################### +-} + + +getProofResponse :: String -> Result +getProofResponse stg = case result of + Left err -> ComError $ stg ++ " | " ++ show err + Right vals -> CGP vals + where result = parse parseGetProofResponse "" stg + + + +{- + ######################################################################### + # # + # get Unsat Core Response # + # # + ######################################################################### +-} + + +getUnsatCoreResponse :: String -> Result +getUnsatCoreResponse stg = case result of + Left err -> ComError $ stg ++ " | " ++ show err + Right vals -> CGUC vals + where result = parse parseGetUnsatCoreResp "" stg + + + +{- + ######################################################################### + # # + # get Assignment # + # # + ######################################################################### +-} + + +getAssignmentResponse :: String -> Result +getAssignmentResponse stg = case result of + Left err -> ComError $ stg ++ " | " ++ show err + Right vals -> CGAssig vals + where result = parse parseGetAssignmentResp "" stg + + +{- + ######################################################################### + # # + # get Option # + # # + ######################################################################### +-} + + +getOptionResponse :: String -> Result +getOptionResponse stg = case result of + Left err -> ComError $ stg ++ " | " ++ show err + Right vals -> CGO vals + where result = parse parseGetOptionResponse "" stg diff --git a/Hsmtlib/Solvers/Cmd/OnlineCmd.hs b/Hsmtlib/Solvers/Cmd/OnlineCmd.hs --- a/Hsmtlib/Solvers/Cmd/OnlineCmd.hs +++ b/Hsmtlib/Solvers/Cmd/OnlineCmd.hs @@ -1,88 +1,142 @@ -{- | -Module : OnlineCmd - -Module with the functions used in online Mode. --} - -module Hsmtlib.Solvers.Cmd.OnlineCmd where - -import Hsmtlib.Solver -import Hsmtlib.Solvers.Cmd.ProcCom.Process -import SMTLib2 -import Text.PrettyPrint -import Hsmtlib.Solvers.Cmd.Parser.CmdResult -import Control.Applicative(liftA) - ---Uses the function send from Cmd.Solver to send the command. -onlineFun :: Process -> Command -> IO String -onlineFun proc cmd = send proc (render (pp cmd) ++ "\n") - -onlineGenResponse :: Process -> Command -> IO GenResult -onlineGenResponse proc cmd = liftA genResponse (onlineFun proc cmd) - -onlineCheckSatResponse :: Process -> Command -> IO SatResult -onlineCheckSatResponse proc cmd = liftA checkSatResponse (onlineFun proc cmd) - -onlineGetValueResponse :: Process -> Command -> IO GValResult -onlineGetValueResponse proc cmd = liftA getValueResponse (onlineFun proc cmd) - - ---SMT Commands. - -onlineSetLogic :: Process -> Name -> IO GenResult -onlineSetLogic proc name = onlineGenResponse proc (CmdSetLogic name) - -onlineSetOption :: Process -> Option -> IO GenResult -onlineSetOption proc option = onlineGenResponse proc (CmdSetOption option) - -onlineSetInfo :: Process -> Attr -> IO GenResult -onlineSetInfo proc attr = onlineGenResponse proc (CmdSetInfo attr) - -onlineDeclareType :: Process -> Name -> Integer -> IO GenResult -onlineDeclareType proc name number = - onlineGenResponse proc (CmdDeclareType name number) - -onlineDefineType :: Process -> Name -> [Name] -> Type -> IO GenResult -onlineDefineType proc name names t = - onlineGenResponse proc (CmdDefineType name names t) - -onlineDeclareFun :: Process -> Name -> [Type] -> Type -> IO GenResult -onlineDeclareFun proc name lt t = - onlineGenResponse proc (CmdDeclareFun name lt t) - -onlineDefineFun :: Process -> Name -> [Binder] -> Type -> Expr -> IO GenResult -onlineDefineFun proc name binders t expression = - onlineGenResponse proc (CmdDefineFun name binders t expression) - -onlinePush :: Process -> Integer -> IO GenResult -onlinePush proc number = onlineGenResponse proc (CmdPush number) - -onlinePop :: Process -> Integer -> IO GenResult -onlinePop proc number = onlineGenResponse proc (CmdPop number) - -onlineAssert :: Process -> Expr -> IO GenResult -onlineAssert proc expression = onlineGenResponse proc (CmdAssert expression) - -onlineCheckSat :: Process -> IO SatResult -onlineCheckSat proc = onlineCheckSatResponse proc CmdCheckSat - -onlineGetAssertions :: Process -> IO String -onlineGetAssertions proc = onlineFun proc CmdGetAssertions - -onlineGetValue :: Process -> [Expr] -> IO GValResult -onlineGetValue proc exprs = onlineGetValueResponse proc (CmdGetValue exprs) - -onlineGetProof :: Process -> IO String -onlineGetProof proc = onlineFun proc CmdGetProof - -onlineGetUnsatCore :: Process -> IO String -onlineGetUnsatCore proc = onlineFun proc CmdGetUnsatCore - -onlineGetInfo :: Process -> InfoFlag -> IO String -onlineGetInfo proc info = onlineFun proc ( CmdGetInfo info ) - -onlineGetOption :: Process -> Name -> IO String -onlineGetOption proc name = onlineFun proc ( CmdGetOption name ) - -onlineExit :: Process -> IO String -onlineExit proc = onlineFun proc CmdExit +{- | +Module : OnlineCmd + +Module with the functions used in online Mode. +-} + +module Hsmtlib.Solvers.Cmd.OnlineCmd where +import Control.Applicative (liftA) +import Hsmtlib.Solver +import Hsmtlib.Solvers.Cmd.CmdResult +import Hsmtlib.Solvers.Cmd.ProcCom.Process +import SMTLib2 +import Text.PrettyPrint + + + +--Uses the function send from Cmd.Solver to send the command. +onlineFun :: Process -> Command -> Solvers -> IO String +onlineFun proc cmd Cvc4 = sendCvc4 proc (render (pp cmd) ++ "\n") +onlineFun proc cmd _ = send proc (render (pp cmd) ++ "\n") + + + +onExit :: Process -> IO String +onExit proc = endProcess proc >> return "success" + +onlineGenResponse :: Process -> Command -> Solvers -> IO Result +onlineGenResponse proc cmd solver = + liftA genResponse (onlineFun proc cmd solver) + +onlineCheckSatResponse :: Process -> Command -> Solvers -> IO Result +onlineCheckSatResponse proc cmd solver = + liftA checkSatResponse (onlineFun proc cmd solver) + +onlineGetValueResponse :: Process -> Command -> Solvers -> IO Result +onlineGetValueResponse proc cmd solver = + liftA getValueResponse (onlineFun proc cmd solver) + + +onlineGetInfoResponse :: Process -> Command -> Solvers -> IO Result +onlineGetInfoResponse proc cmd solver = + liftA getInfoResponse (onlineFun proc cmd solver) + + +onlineGetAssertionResponse :: Process -> Command -> Solvers -> IO Result +onlineGetAssertionResponse proc cmd solver = + liftA getAssertionResponse (onlineFun proc cmd solver) + +onlineGetProofResponse :: Process -> Command -> Solvers -> IO Result +onlineGetProofResponse proc cmd solver = + liftA getProofResponse (onlineFun proc cmd solver) + + +onlineGetUnsatCoreResponse :: Process -> Command -> Solvers -> IO Result +onlineGetUnsatCoreResponse proc cmd solver = + liftA getUnsatCoreResponse (onlineFun proc cmd solver) + + +onlineGetAssignmentResponse :: Process -> Command -> Solvers -> IO Result +onlineGetAssignmentResponse proc cmd solver = + liftA getAssignmentResponse (onlineFun proc cmd solver) + + +onlineGetOptionResponse :: Process -> Command -> Solvers -> IO Result +onlineGetOptionResponse proc cmd solver = + liftA getOptionResponse (onlineFun proc cmd solver) + +onlineExitResponse :: Process -> IO Result +onlineExitResponse proc = liftA genResponse (onExit proc) + +--SMT Commands. + +onlineSetLogic ::Solvers -> Process -> Name -> IO Result +onlineSetLogic solver proc name = + onlineGenResponse proc (CmdSetLogic name) solver + +onlineSetOption ::Solvers -> Process -> Option -> IO Result +onlineSetOption solver proc option = + onlineGenResponse proc (CmdSetOption option) solver + +onlineSetInfo ::Solvers -> Process -> Attr -> IO Result +onlineSetInfo solver proc attr = + onlineGenResponse proc (CmdSetInfo attr) solver + +onlineDeclareType ::Solvers -> Process -> Name -> Integer -> IO Result +onlineDeclareType solver proc name number = + onlineGenResponse proc (CmdDeclareType name number) solver + +onlineDefineType ::Solvers -> Process -> Name -> [Name] -> Type -> IO Result +onlineDefineType solver proc name names t = + onlineGenResponse proc (CmdDefineType name names t) solver + +onlineDeclareFun ::Solvers -> Process -> Name -> [Type] -> Type -> IO Result +onlineDeclareFun solver proc name lt t = + onlineGenResponse proc (CmdDeclareFun name lt t) solver + +onlineDefineFun ::Solvers -> Process -> Name -> [Binder] -> Type -> Expr -> IO Result +onlineDefineFun solver proc name binders t expression = + onlineGenResponse proc (CmdDefineFun name binders t expression) solver + +onlinePush ::Solvers -> Process -> Integer -> IO Result +onlinePush solver proc number = + onlineGenResponse proc (CmdPush number) solver + +onlinePop ::Solvers -> Process -> Integer -> IO Result +onlinePop solver proc number = + onlineGenResponse proc (CmdPop number) solver + +onlineAssert ::Solvers -> Process -> Expr -> IO Result +onlineAssert solver proc expression = + onlineGenResponse proc (CmdAssert expression) solver + +onlineCheckSat ::Solvers -> Process -> IO Result +onlineCheckSat solver proc = + onlineCheckSatResponse proc CmdCheckSat solver + +onlineGetAssertions ::Solvers -> Process -> IO Result +onlineGetAssertions solver proc = + onlineGetAssertionResponse proc CmdGetAssertions solver + +onlineGetValue ::Solvers -> Process -> [Expr] -> IO Result +onlineGetValue solver proc exprs = + onlineGetValueResponse proc (CmdGetValue exprs) solver + +onlineGetProof ::Solvers -> Process -> IO Result +onlineGetProof solver proc = + onlineGetProofResponse proc CmdGetProof solver + +onlineGetUnsatCore ::Solvers -> Process -> IO Result +onlineGetUnsatCore solver proc = + onlineGetUnsatCoreResponse proc CmdGetUnsatCore solver + +onlineGetInfo ::Solvers -> Process -> InfoFlag -> IO Result +onlineGetInfo solver proc info = + onlineGetInfoResponse proc (CmdGetInfo info) solver + +onlineGetOption ::Solvers -> Process -> Name -> IO Result +onlineGetOption solver proc name = + onlineGetOptionResponse proc (CmdGetOption name) solver + +onlineExit :: Process -> IO Result +onlineExit proc = onlineExitResponse proc diff --git a/Hsmtlib/Solvers/Cmd/Parser/CmdResult.hs b/Hsmtlib/Solvers/Cmd/Parser/CmdResult.hs deleted file mode 100644 --- a/Hsmtlib/Solvers/Cmd/Parser/CmdResult.hs +++ /dev/null @@ -1,388 +0,0 @@ -module Hsmtlib.Solvers.Cmd.Parser.CmdResult where - -import Control.Applicative ((<|>),(<$>)) -import Control.Monad -import Data.List (intercalate) -import Data.Map as M -import Data.Maybe (isJust) -import Hsmtlib.Solver as Solv -import Hsmtlib.Solvers.Cmd.Parser.Parsers hiding (numeral, symbol) -import Hsmtlib.Solvers.Cmd.Parser.Syntax as S -import Hsmtlib.Solvers.Cmd.Parser.Visualizers -import Prelude as P -import Text.ParserCombinators.Parsec.Prim (parse) - -genResponse :: String -> GenResult -genResponse stg = - case result of - Left err -> Solv.GUError $ show err - Right cmdRep -> case cmdRep of - CmdGenResponse S.Success -> Solv.Success - CmdGenResponse S.Unsupported -> Solv.Unsupported - CmdGenResponse (S.Error err) -> Solv.Error err - where result = parse parseCmdGenResponse "" stg - - -checkSatResponse :: String -> SatResult -checkSatResponse stg = - case result of - Left err -> Solv.SUError $ show err - Right cmdRep -> case cmdRep of - S.Sat -> Solv.Sat - S.Unsat -> Solv.Unsat - S.Unknown -> Solv.Unknown - where result = parse parseCheckSatResponse "" stg - - -{- -getValueResponse :: String -> GValResult -getValueResponse stg = GVUError $ stg ++ "\n" ++ tree - where result = parse parseGetValueResponse "" stg - tree = getVR' result - - -getVR' :: Show a => Either a [ValuationPair] -> String -getVR' result = - case result of - Left err -> show err - Right vals -> intercalate "\n" (fmap (showValuationPair 0) vals) - --} -getValueResponse :: String -> GValResult -getValueResponse stg = case result of - Left err -> GVUError $ stg ++ "|"++show err - Right vals -> getVR' $ getValResponse vals - where result = parse parseGetValueResponse "" stg - - -getVR' :: [GValResult] -> GValResult -getVR' xs | length xs == 1 = head xs - | otherwise = Results xs - -getValResponse::[ValuationPair] -> [GValResult] -getValResponse vp = arrays ++ errors - -- gets the results in a Maybe GValResult. - where res = getValResponses vp - --Produes UErrors from the results that gave Nothing. - errors = valErrors' vp res - cRes = P.filter isJust res -- Removes the Nothings. - -- Joins all arrays in one and - --removes the Just from all results. - arrays = joinArrays cRes - - - -valErrors' :: [ValuationPair] -> [Maybe GValResult] -> [GValResult] -valErrors' [] [] = [] -valErrors' (x:xs) (Nothing:gs) = - GVUError (showValuationPair 0 x) : valErrors' xs gs -valErrors' (_:xs) (_:gs) = valErrors' xs gs - - - -joinArrays :: [Maybe GValResult] -> [GValResult] -joinArrays = joinArrays' $ VArrays empty - - -joinArrays' :: GValResult -> [Maybe GValResult] -> [GValResult] --- if there was no array in the result then don't put an empty one. -joinArrays' (VArrays n) [] | M.null n = [] - | otherwise = [VArrays n] -joinArrays' res (x:xs) = case nVal of - (VArrays _) -> joinArrays' nVal xs - _ -> nVal : joinArrays' res xs - where nVal = checkGVal res x - -checkGVal :: GValResult -> Maybe GValResult -> GValResult -checkGVal (VArrays oarr) (Just(VArrays arr)) = - VArrays $ unionWith union oarr arr -checkGVal _ (Just x) = x - - -getValResponses :: [ValuationPair] -> [Maybe GValResult] -getValResponses = fmap getGValResult - -getGValResult :: ValuationPair -> Maybe GValResult -getGValResult vp = getVar vp - <|> getArray vp - <|> getFun vp - <|> getBitVec vp - -{- | Retrives the value of a BitVector. - Works with: - - Z3. --} -getBitVec :: ValuationPair -> Maybe GValResult -getBitVec vp = getBitVec' name vhex - where name = getVarName vp - vhex = getHexVal vp - - --- auxiliar function to getBitVec -getBitVec' :: Maybe String -> Maybe String -> Maybe GValResult -getBitVec' (Just name) (Just vhex) = Just $ Res name $ VHex vhex -getBitVec' _ _ = Nothing - -{- | Retrives the value of a function. - Works with: - - Z3. --} -getFun :: ValuationPair -> Maybe GValResult -getFun vp = getFun' name value - where name = getFunName vp - value = getFunResult vp - --- auxiliar function to getFun -getFun' :: Maybe String -> Maybe Value -> Maybe GValResult -getFun' (Just name) (Just res) = Just $ Res name res -getFun' _ _ = Nothing - - -{- | Retrives the value of a variable. - Works with: - - Z3. --} -getVar :: ValuationPair -> Maybe GValResult -getVar vp = getVar' name value - where name = getVarName vp - value = getVarValue vp - --- auxiliar function to getVar -getVar' :: Maybe String -> Maybe Integer -> Maybe GValResult -getVar' Nothing _ = Nothing -getVar' _ Nothing = Nothing -getVar' (Just name) (Just value) = Just $ Res name $ VInt value - - - - -{- | Retrives the value of an array. - Works with: - - Z3. --} -getArray :: ValuationPair -> Maybe GValResult -getArray vp = - case isArr of - Nothing -> Nothing - Just _ -> case res of - Just arr -> Just $ VArrays arr - Nothing -> Nothing - - where name = arrayName vp - posInt = arrayIntPos vp - posVar = arrayVarPos vp - val = arrayVal vp - isArr = isArray vp - res = getArray' name posInt posVar val - - --- Auxiliar function to getArray. -getArray' :: Maybe String - -> Maybe Integer - -> Maybe String - -> Maybe Integer - -> Maybe Arrays -getArray' (Just name) (Just pos) Nothing (Just val) = - Just $ singleton name $ singleton (show pos) val -getArray' (Just name) Nothing (Just pos) (Just val) = - Just $ singleton name $ singleton pos val -getArray' _ _ _ _ = Nothing - - - - --- Auxiliar functions to get values from constructed ast. - - - - - -isArray :: ValuationPair -> Maybe Bool -isArray = isArray' - <=< symbol - <=< qIdentifier - <=< fstTermQualIdentierT - <=< fstTerm - - -{- | Verifies if the string correspond to a certain notation that indicates - that is an Array. - For example Z3 would have the keyword select therefor it's an array. - If it isn't an array then returns nothing - --} -isArray' :: String -> Maybe Bool -isArray' "select" = Just True -isArray' _ = Nothing - - --- Auxliar functions to work with arrays. -{- | Retrives the name of the array. - Works with: - - Z3. --} - -arrayName :: ValuationPair -> Maybe String -arrayName = symbol - <=< qIdentifier - <=< termQualIdentifier - <=< fstValArray - <=< sndTermQualIdentierT - <=< fstTerm - where fstValArray x = Just $ head x - -{-| Retrives the position of the array if it is an Integer. - Works with: - - Z3. --} -arrayIntPos :: ValuationPair -> Maybe Integer -arrayIntPos = numeral - <=< getTermSpecConstant - <=< sndValArray - <=< sndTermQualIdentierT - <=< fstTerm - where sndValArray x = Just $ x !! 1 - -{-| Retrives the position of the array if it is a String. - Works with: - - Z3. --} -arrayVarPos :: ValuationPair -> Maybe String -arrayVarPos = symbol - <=< qIdentifier - <=< termQualIdentifier - <=< sndValArray - <=< sndTermQualIdentierT - <=< fstTerm - where sndValArray x = Just $ x !! 1 - - -{-| Retrives the value of an array. - Works with: - - Z3. --} -arrayVal :: ValuationPair -> Maybe Integer -arrayVal = numeral <=< getTermSpecConstant <=< sndTerm - - - -{- | Retrive the name of a variable. - Works with: - - Z3. - --} - -getVarName :: ValuationPair -> Maybe String -getVarName = symbol <=< qIdentifier <=< termQualIdentifier <=< fstTerm - - -{- | Retrive the variable of a variable. - Works with: - - Z3. - --} -getVarValue :: ValuationPair -> Maybe Integer -getVarValue = numeral <=< getTermSpecConstant <=< sndTerm - - - -{- | Retrives the name of a function. - Works with: - - Z3 --} -getFunName :: ValuationPair -> Maybe String -getFunName = symbol <=< qIdentifier <=< fstTermQualIdentierT <=< fstTerm - - - -{- | Retrives the result of a function if it is a Integer. - Works with: - - Z3. --} - - -getFunResult :: ValuationPair -> Maybe Value -getFunResult vp = getFunResultBool vp <|> getFunResultInt vp - -getFunResultBool :: ValuationPair -> Maybe Value -getFunResultBool = VBool <#> toBool <=< getFunResultBool' - - -getFunResultInt :: ValuationPair -> Maybe Value -getFunResultInt = VInt <#> getFunResultInt' - - - -(<#>):: Functor m => (b -> c) -> (a -> m b) -> a -> m c -(<#>) f m = \x -> f <$> m x - -toBool :: String -> Maybe Bool -toBool "true" = Just True -toBool "false" = Just False -toBool _ = Nothing - -getFunResultInt' :: ValuationPair -> Maybe Integer -getFunResultInt' = numeral <=< getTermSpecConstant <=< sndTerm - - -getFunResultBool' :: ValuationPair -> Maybe String -getFunResultBool' = symbol <=< qIdentifier <=< termQualIdentifier <=< sndTerm - - -{- | Retrives the result of a bitvector. - Works with: - - Z3 --} -getHexVal :: ValuationPair -> Maybe String -getHexVal = hex <=< getTermSpecConstant <=< fstTerm - - --- Auxiliar functions to get specific value from ast. - - --- | Returns the first term of a valuation pair. -fstTerm :: ValuationPair -> Maybe Term -fstTerm (ValuationPair a _) = Just a - - --- | Returns the second term of a valuation pair. -sndTerm :: ValuationPair -> Maybe Term -sndTerm (ValuationPair _ b) = Just b - - --- | Returns the list of terms from TermQualIdeintifierT -sndTermQualIdentierT :: Term -> Maybe [Term] -sndTermQualIdentierT (TermQualIdentifierT _ ts) = Just ts -sndTermQualIdentierT _ = Nothing - -fstTermQualIdentierT :: Term -> Maybe QualIdentifier -fstTermQualIdentierT (TermQualIdentifierT qi _) = Just qi -fstTermQualIdentierT _ = Nothing - - -termQualIdentifier :: Term -> Maybe QualIdentifier -termQualIdentifier (TermQualIdentifier a) = Just a -termQualIdentifier _ = Nothing - - -getTermSpecConstant :: Term -> Maybe SpecConstant -getTermSpecConstant (TermSpecConstant spc) = Just spc -getTermSpecConstant _ = Nothing - - -qIdentifier :: QualIdentifier -> Maybe Identifier -qIdentifier (QIdentifier a) = Just a -qIdentifier _ = Nothing - -symbol :: Identifier -> Maybe String -symbol (ISymbol s) = Just s -symbol _ = Nothing - - -numeral :: SpecConstant -> Maybe Integer -numeral (SpecConstantNumeral n) = Just n -numeral _ = Nothing - -hex :: SpecConstant -> Maybe String -hex (SpecConstantHexadecimal shex) = Just shex -hex _ = Nothing diff --git a/Hsmtlib/Solvers/Cmd/Parser/Parsers.hs b/Hsmtlib/Solvers/Cmd/Parser/Parsers.hs deleted file mode 100644 --- a/Hsmtlib/Solvers/Cmd/Parser/Parsers.hs +++ /dev/null @@ -1,538 +0,0 @@ - module Hsmtlib.Solvers.Cmd.Parser.Parsers where - -import Control.Applicative as Ctr hiding ((<|>)) -import Control.Monad -import Data.Functor.Identity -import Hsmtlib.Solvers.Cmd.Parser.Syntax as CmdRsp -import Text.Parsec.Prim as Prim -import Text.ParserCombinators.Parsec as Pc - - - -(<:>) :: Applicative f => f a -> f [a] -> f [a] -(<:>) a b = (:) <$> a <*> b - -(<++>) :: Applicative f => f [a] -> f [a] -> f [a] -(<++>) a b = (++) <$> a <*> b - - ---Auxiliar parsers -aspO :: ParsecT String u Identity Char -aspO = char '(' - -aspC :: ParsecT String u Identity Char -aspC = char ')' - -aspUS :: ParsecT String u Identity Char -aspUS = char '_' - -numeral :: ParsecT String u Identity String -numeral = many1 digit - -decimal :: ParsecT String u Identity String -decimal = numeral <++> dot <++> zeros <++> numeral - -zeros :: ParsecT String u Identity String -zeros = Pc.many $ char '0' - -dot :: ParsecT String u Identity String -dot = string "." - -hexadecimal :: ParsecT String u Identity String -hexadecimal = string "#x" *> many1 hexDigit - -binary :: ParsecT String u Identity String -binary = string "#b" *> many1 bin - -bin :: ParsecT String u Identity Char -bin = char '0' <|> char '1' - - -str :: ParsecT String u Identity String -str = string "\"" <++> Pc.many (alphaNum <|> char ' ') <++> string "\"" - - -symbol :: ParsecT String u Identity String -symbol = simpleSymbol <|> quotedSymbol - -quotedSymbol :: ParsecT String u Identity String -quotedSymbol = char '|' <:> Pc.many alphaNum <++> string "|" - -simpleSymbol :: ParsecT String u Identity String -simpleSymbol = (letter <|> spcSymb) <:> sq - where sq = Pc.many (alphaNum <|> spcSymb) - -spcSymb :: ParsecT String u Identity Char -spcSymb = oneOf "+-/*=%?!.$_~^&<>" - - -keyword :: ParsecT String u Identity String -keyword = char ':' <:> Pc.many (alphaNum<|> spcSymb) - - -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" - -bValue :: ParsecT String u Identity Bool -bValue = (string "true" >> return True) <|> - (string "false" >> return False) - - --- Parse spec_constant -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 - - - -parseSpecConstant :: ParsecT String u Identity SpecConstant -parseSpecConstant = Pc.try parseDecimal - <|> parseNumeral - <|> parseHexadecimal - <|> parseBinary - <|> parseString - - - --- parse S-expressions, for the parsing to work newlines must be removed - -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 - -parseSexprS :: ParsecT String u Identity Sexpr -parseSexprS = do - aspO - spaces - res <- sepBy parseSexpr' spaces - aspC - spaces - return $ SexprSxp res - - -parseSexpr' :: ParsecT String u Identity Sexpr -parseSexpr' = parseSexprConstant - <|> parseSexprSymbol - <|> parseSexprKeyword - <|> parseSexprS - -parseSexpr :: ParsecT String u Identity [Sexpr] -parseSexpr = sepBy parseSexpr' spaces - - - - --- Parse identifier -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 - spaces - aspUS - spaces - symb <- symbol - spaces - num <- many1 (numeral <|> string " ") - spaces - aspC - return $ I_Symbol symb num - - --- Parse Sorts -parseSort :: ParsecT String u Identity [Sort] -parseSort = sepBy parseSort' spaces - -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 - spaces - identifier <- parseIdentifier - spaces - sorts <- sepBy1 parseSort' spaces - spaces - aspC - return $ SortIdentifiers identifier sorts - - - - ---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 - spaces - expr <- parseSexpr - aspC - return $ AttrValueSexpr expr - --- Parse Attribute -parseAttribute :: ParsecT String u Identity Attribute -parseAttribute = do - key <- keyword - spaces - attr <- optionMaybe parseAttributeValue - case attr of - Nothing -> return $ Attribute key - Just val -> return $ AttributeVal key val - - - - --- Parse terms - --- -- 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 - spaces - string "as" - spaces - ident <- parseIdentifier - spaces - sort <- parseSort' - spaces - aspC - return $ QIdentifierAs ident sort - - --- -- Parse Var Binding -parseVarBinding :: ParsecT String u Identity VarBinding -parseVarBinding = do - aspO - spaces - symb <- symbol - spaces - term <- parseTerm - spaces - aspC - return $ VB symb term - - - - --- -- Parse Sorted Var -parseSortedVar :: ParsecT String u Identity SortedVar -parseSortedVar = do - aspO - spaces - symb <- symbol - spaces - sort <- parseSort' - spaces - aspC - return $ SV symb sort - - --- 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 - spaces - iden <- parseQualIdentifier - spaces - terms <- sepBy1 parseTerm spaces - aspC - return $ TermQualIdentifierT iden terms - -parseTermLet :: ParsecT String u Identity Term -parseTermLet = do - aspO - spaces - string "let" - spaces - aspO - spaces - vb <- sepBy1 parseVarBinding spaces - aspC - spaces - term <- parseTerm - spaces - aspC - return $ TermLet vb term - -parseTermFA :: ParsecT String u Identity Term -parseTermFA = do - aspO - spaces - string "forall" - spaces - aspO - sv <- sepBy1 parseSortedVar spaces - aspC - spaces - term <- parseTerm - spaces - aspC - return $ TermForall sv term - - -parseTermEX :: ParsecT String u Identity Term -parseTermEX = do - aspO - spaces - string "exists" - spaces - aspO - sv <- sepBy1 parseSortedVar spaces - aspC - spaces - term <- parseTerm - spaces - aspC - return $ TermExists sv term - -parseTermAnnot :: ParsecT String u Identity Term -parseTermAnnot = do - aspO - spaces - char '!' - spaces - term <- parseTerm - spaces - attr <- sepBy1 parseAttribute spaces - aspC - return $ TermAnnot term attr - - - - ---Parser for CmdGenResponse - -parseCmdGenResponse :: ParsecT String u Identity CmdResponse -parseCmdGenResponse = - (string "unsupported" >> return (CmdGenResponse Unsupported)) - <|> (string "success" >> return (CmdGenResponse Success)) - <|> parseCmdGenRepError - -parseCmdGenRepError :: ParsecT String u Identity CmdResponse -parseCmdGenRepError = do - aspO - string "error" - space - char '"' - cont <- Pc.many (alphaNum<|> char ':'<|> char ' ') - char '"' - aspC - return $ CmdGenResponse $ CmdRsp.Error cont - --- Parsers for CmdGetInfoResponse - -parseCmdGetInfoResponse :: ParsecT String u Identity CmdResponse -parseCmdGetInfoResponse = liftM CmdGetInfoResponse parseGetInfoResponse - - -parseGetInfoResponse :: ParsecT String u Identity [InfoResponse] -parseGetInfoResponse = do - aspO - spaces - infoResp <- sepBy1 parseInfoResponse spaces - 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" *> space *> liftM ResponseName str - - -parseResponseErrorBehavior :: ParsecT String u Identity InfoResponse -parseResponseErrorBehavior = string "error-behavior" *> space *> - 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" *> space *> - liftM ResponseAuthors str - -parseResponseVersion :: ParsecT String u Identity InfoResponse -parseResponseVersion = string "version" *> space *> - liftM ResponseVersion str - - -parseResponseReasonUnknown :: ParsecT String u Identity InfoResponse -parseResponseReasonUnknown = string "reason" *> space *> - liftM ResponseReasonUnknown parseReasonUnknown - -parseResponseAttribute :: ParsecT String u Identity InfoResponse -parseResponseAttribute = liftM ResponseAttribute parseAttribute - - --- Parser for check sat response -parseCheckSatResponse :: ParsecT String u Identity CheckSatResponse -parseCheckSatResponse = - (string "sat" >> return Sat) <|> - (string "unsat" >> return Unsat) <|> - (string "unknown" >> return Unknown) - --- parse Get Assertion Response -parseGetAssertionResponse :: ParsecT String u Identity [Term] -parseGetAssertionResponse = do - aspO - spaces - terms <- sepBy1 parseTerm spaces - aspC - return terms - --- parse Get Proof response -parseGetProofResponse :: ParsecT String u Identity Sexpr -parseGetProofResponse = parseSexpr' - - --- parse Get unsat core response -parseGetUnsatCoreResp :: ParsecT String u Identity [String] -parseGetUnsatCoreResp = do - aspO - spaces - symb <- sepBy1 symbol spaces - aspC - return symb - - --- parse Get Value response -parseGetValueResponse :: ParsecT String u Identity [ValuationPair] -parseGetValueResponse = aspO *> sepBy1 parseValuationPair spaces <* aspC - -parseValuationPair :: ParsecT String u Identity ValuationPair -parseValuationPair = do - aspO - spaces - term1 <- parseTerm - spaces - term2 <- parseTerm - spaces - aspC - return $ ValuationPair term1 term2 - - --- parse t valuation pair -parseTValuationPair :: ParsecT String u Identity TValuationPair -parseTValuationPair = do - aspO - spaces - symb <- symbol - spaces - bval <- bValue - spaces - aspC - return $ TValuationPair symb bval - - - --- parse get Assignent Response -parseGetAssignmentResp :: ParsecT String u Identity [TValuationPair] -parseGetAssignmentResp = do - aspO - spaces - pairs <- sepBy1 parseTValuationPair spaces - aspC - return pairs - - --- parse Get Option Response -parseGetOptionResponse :: ParsecT String u Identity AttrValue -parseGetOptionResponse = parseAttributeValue - - - -parseReasonUnknown :: ParsecT String u Identity ReasonUnknown -parseReasonUnknown = - (string "memout" >> return Memout) <|> - (string "incomplete" >> return Incomplete) - - ---Parser for CmdResponse -{-- -resultParser :: ParsecT String u Identity CmdResponse -resultParser = parseCmdGenResponse - <|> parseCmdGetInfoResponse - ---} - -main :: IO a -main = forever $ do putStrLn "Enter a string: " - input <- getLine - parseTest parseGetValueResponse input - --parseIdentifier - --parseTest parseTerm input diff --git a/Hsmtlib/Solvers/Cmd/Parser/Syntax.hs b/Hsmtlib/Solvers/Cmd/Parser/Syntax.hs deleted file mode 100644 --- a/Hsmtlib/Solvers/Cmd/Parser/Syntax.hs +++ /dev/null @@ -1,153 +0,0 @@ -module Hsmtlib.Solvers.Cmd.Parser.Syntax where - - --- S-expressions - -data SpecConstant = SpecConstantNumeral Integer - | SpecConstantDecimal String - | SpecConstantHexadecimal String - | SpecConstantBinary String - | SpecConstantString String - deriving (Show) - - - -data Sexpr = SexprSpecConstant SpecConstant - | SexprSymbol String - | SexprKeyword String - | SexprSxp [Sexpr] - deriving (Show) - - --- Identifiers - -data Identifier = ISymbol String - | I_Symbol String [String] deriving (Show) - - - --- Sorts - -data Sort = SortId Identifier | SortIdentifiers Identifier [Sort] - deriving (Show) - - - --- Attributes - -data AttrValue = AttrValueConstant SpecConstant - | AttrValueSymbol String - | AttrValueSexpr [Sexpr] - deriving (Show) - - - -data Attribute = Attribute String - | AttributeVal String AttrValue - deriving (Show) - --- Terms - -data QualIdentifier = QIdentifier Identifier - | QIdentifierAs Identifier Sort - deriving (Show) - - - -data VarBinding = VB String Term deriving (Show) - - - -data SortedVar = SV String Sort deriving (Show) - - - -data Term = TermSpecConstant SpecConstant - | TermQualIdentifier QualIdentifier - | TermQualIdentifierT QualIdentifier [Term] - | TermLet [VarBinding] Term - | TermForall [SortedVar] Term - | TermExists [SortedVar] Term - | TermAnnot Term [Attribute] - deriving (Show) - --- Command Responses - --- Gen Response - - - -data GenResponse = Unsupported | Success | Error String deriving (Show) - - --- Error behavior - -data ErrorBehavior = ImmediateExit | ContinuedExecution deriving (Show) - - --- Reason unknown - -data ReasonUnknown = Memout | Incomplete deriving (Show) - --- Status - -data CheckSatResponse = Sat | Unsat | Unknown deriving (Show) - --- Info Response - -type GetInfoResponse = [InfoResponse] - -data InfoResponse = ResponseErrorBehavior ErrorBehavior - | ResponseName String - | ResponseAuthors String - | ResponseVersion String - | ResponseReasonUnknown ReasonUnknown - | ResponseAttribute Attribute - deriving (Show) - --- 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) - - -type GetValueResponse = [ValuationPair] - - --- get Assignment Response - -data TValuationPair = TValuationPair String Bool deriving (Show) - -type GetAssignmentResponse = [TValuationPair] - - --- Get Option Response - -type GetOptionResponse = AttrValue - --- CmdResponse - -data CmdResponse = CmdGenResponse GenResponse - | CmdGetInfoResponse GetInfoResponse - | CmdCheckSatResponse CheckSatResponse - | CmdGetAssertionResponse GetAssignmentResponse - | CmdGetProofResponse GetProofResponse - | CmdGetUnsatCoreResoponse GetUnsatCoreResponse - | CmdGetValueResponse GetValueResponse - | CmdGetAssigmnentResponse TValuationPair - | CmdGetOptionResponse GetOptionResponse - deriving (Show) diff --git a/Hsmtlib/Solvers/Cmd/Parser/Visualizers.hs b/Hsmtlib/Solvers/Cmd/Parser/Visualizers.hs deleted file mode 100644 --- a/Hsmtlib/Solvers/Cmd/Parser/Visualizers.hs +++ /dev/null @@ -1,180 +0,0 @@ -module Hsmtlib.Solvers.Cmd.Parser.Visualizers where - -import Hsmtlib.Solvers.Cmd.Parser.Syntax as S -import Data.List - - - - -spaces' :: Int -> Int -> String -spaces' n limit | n == limit = "" - | otherwise = " " ++ spaces' (n+1) limit - -spaces :: Int -> String -spaces = spaces' 0 - -branch' :: Int -> String -branch' nsp = "\n" ++ spaces nsp++"|\n" ++ spaces nsp ++ "|- " - -branchAr' :: Int -> String -branchAr' nsp = "\n" ++ spaces nsp ++"\n" ++ spaces (nsp+1) ++ "[" - -fbranch :: Int -> String -> String -> String -fbranch nsp mark fin = mark ++ branch' nsp ++ fin - -branch :: String -> (Int -> a -> String) -> Int -> a -> String -branch mark f nsp arg = mark ++ branch' nsp ++ f (nsp+3) arg - - -nLines :: String -> Int -nLines = length.lines - -mLines :: String ->Int -> String -mLines _ 0 = "" -mLines sps n = sps ++ "|\n" ++ mLines sps (n-1) - -showValuationPair :: Int -> ValuationPair-> String -showValuationPair nsp (ValuationPair t1 t2) = tup "ValP" nsp t1 t2 showTerm showTerm - -showSpecConstant :: SpecConstant -> String -showSpecConstant (SpecConstantNumeral int) = "Num " ++ show int -showSpecConstant (SpecConstantDecimal st) = "Dec " ++ st -showSpecConstant (SpecConstantHexadecimal st) = "Hex " ++ st -showSpecConstant (SpecConstantBinary it) = "Bin " ++ show it -showSpecConstant (SpecConstantString st) = "Str " ++ st - - -aTup :: String - -> Int - -> [a] - -> (Int -> a -> String) - -> String -aTup mark nsp arg f = - mark ++ " -[ " ++ hd ++ arr ++ endSpace++"]" - where - hd =f (nsp+8) (head arg) - bd = drop 1 arg - arr = backSpace ++ intercalate backSpace (fmap (f (nsp+8)) bd) - backSpace = "\n" ++ spaces (nsp+6) ++ ", " - endSpace = "\n" ++ spaces (nsp+6) - -dTup :: String - -> Int - -> String - -> a - -> (Int -> a -> String) - -> String -dTup mark nsp st arg f = - bMark ++ st ++ sndStr - where bMark = mark ++ branch' nsp - sndStr = branch' nsp ++ f (nsp+3) arg - -tup :: String - -> Int - -> a - -> b - -> (Int -> a -> String) - -> (Int -> b -> String) - -> String -tup mark nsp arg1 arg2 f1 f2 = - bMark ++ bf1 ++ bf2 - where bMark = mark ++ branch' nsp - bf1 = f1 (nsp+3) arg1 ++ "\n" ++ spaces nsp ++"|- " - bf2 = f2 (nsp+3) arg2 - - -tupArray :: String - -> Int - -> a - -> [b] - -> (Int -> a -> String) - -> (Int -> b -> String) - -> String -tupArray mark nsp arg1 arg2 f1 f2 = - mark ++ fstf ++ sndf - where fstf = "\n" ++spaces nsp ++ "|- " ++ f1 (nsp+3) arg1 - sndf ="\n" ++ spaces nsp ++ "|-[ " ++ hd ++ strs ++ endSpace - hd = f2 (nsp+5) (head arg2) ++ backSpace - bd = drop 1 arg2 - strs = intercalate backSpace (fmap (f2 (nsp+5)) bd) - backSpace = "\n" ++ spaces (nsp+2) ++ ", " - endSpace = "\n" ++ spaces (nsp+2) ++ "]" - -showQualIdentifier :: Int -> QualIdentifier -> String -showQualIdentifier nsp (QIdentifier qid) = branch "QI" showIdentifier nsp qid -showQualIdentifier nsp (QIdentifierAs iden srt) = - tup "QIAS" nsp iden srt showIdentifier showSort - - - -showSort :: Int -> Sort -> String -showSort nsp (SortId iden) = branch "SID" showIdentifier nsp iden -showSort nsp (SortIdentifiers iden sorts) = - tupArray "SIden" nsp iden sorts showIdentifier showSort - - - -showIdentifier :: Int -> Identifier -> String -showIdentifier _ (ISymbol st) = "IS " ++ st -showIdentifier nsp (I_Symbol str1 str2) = - "I_S" ++ fstr ++ sstr - where brc = "\n" ++ spaces nsp ++ "|\n" ++ spaces nsp - fstr = brc ++ "|- " ++ str1 - sstr = brc ++ "|- [ " ++hd ++ strs ++ end - hd = head str2 ++ "\n" - bd = drop 1 str2 - strs = intercalate "\n" (fmap ((spaces (nsp + 3) ++ ", ") ++) bd) - end = "\n" ++ spaces (nsp+3) ++ "]" - - - - -showTerm ::Int -> Term -> String -showTerm nsp (TermSpecConstant sc) = - fbranch nsp "TSC" $ showSpecConstant sc -showTerm nsp (TermQualIdentifier qi) = - branch "TQI" showQualIdentifier nsp qi -showTerm nsp (TermQualIdentifierT qi ts) = - tupArray "TQIT" nsp qi ts showQualIdentifier showTerm -showTerm nsp (TermLet vb t) = - tupArray "TLt" nsp t vb showTerm showVarBinding -showTerm nsp (TermForall sv t) = - tupArray "TFA" nsp t sv showTerm showSortedVar -showTerm nsp (TermExists sv t) = - tupArray "TE" nsp t sv showTerm showSortedVar -showTerm nsp (TermAnnot t attrs) = - tupArray "TAN" nsp t attrs showTerm showAttribute - - - - - -showVarBinding :: Int -> VarBinding -> String -showVarBinding nsp (VB stg term) = dTup "VB" nsp stg term showTerm - -showSortedVar :: Int -> SortedVar -> String -showSortedVar nsp (SV stg st) = dTup "SV" nsp stg st showSort - -showAttribute :: Int -> Attribute -> String -showAttribute nsp (Attribute st) = fbranch nsp "Attribute" st -showAttribute nsp (AttributeVal stg av) = - dTup "AttrVal" nsp stg av showAttrValue - -showAttrValue :: Int -> AttrValue -> String -showAttrValue nsp (AttrValueConstant sc) = - fbranch nsp "AVC" $ showSpecConstant sc -showAttrValue nsp (AttrValueSymbol st) = - fbranch nsp "AVS" st -showAttrValue nsp (AttrValueSexpr sxpr) = - aTup "AVSP" nsp sxpr showSexpr - - -showSexpr :: Int -> Sexpr -> String -showSexpr nsp (SexprSpecConstant sc) = - fbranch nsp "SSC" $ showSpecConstant sc -showSexpr nsp (SexprSymbol st) = - fbranch nsp "SSymb" st -showSexpr nsp (SexprKeyword st) = - fbranch nsp "SK" st -showSexpr nsp (SexprSxp sexprs) = - aTup "SSxp" nsp sexprs showSexpr diff --git a/Hsmtlib/Solvers/Cmd/ProcCom/Process.hs b/Hsmtlib/Solvers/Cmd/ProcCom/Process.hs --- a/Hsmtlib/Solvers/Cmd/ProcCom/Process.hs +++ b/Hsmtlib/Solvers/Cmd/ProcCom/Process.hs @@ -1,156 +1,246 @@ -{- | -Module : Process - - The following module contains method that facilitate the comunication with - the SMTSolvers. --} -module Hsmtlib.Solvers.Cmd.ProcCom.Process - ( beginProcess - , send - , endProcess - , sendContext - , sendScript - , Process - , CmdPath - , Args - ) where - -import Control.Exception -import GHC.IO.Handle -import System.Exit -import System.Process - - --- | Path to the process -type CmdPath = String - --- | Argumants passed to process -type Args = [String] - --- |Type returned by CreateProcess -type Process = - ( Maybe Handle -- process std_in pipe - , Maybe Handle -- process std_out pipe - , Maybe Handle -- process std_err pipe - , ProcessHandle -- process pid - ) - --- | Context is just a string wich will be sent to std_in -type Context = String - - --- Functions used in Online Mode - - -{- | - Generates a CreateProcess - with just the command, - the arguments - and creates the pipes to comunicate - -} -newProcess :: CmdPath -> Args -> CreateProcess -newProcess p a = CreateProcess - { cmdspec = RawCommand p a - , cwd = Nothing - , env = Nothing - , std_in = CreatePipe - , std_out = CreatePipe - , std_err = CreatePipe - , close_fds = False - , create_group = False - } - --- | Creates a Process ready to be executed. -beginProcess :: CmdPath -> Args -> IO Process -beginProcess cmd path = createProcess (newProcess cmd path) - - --- | trys to run the function. -tryIO ::(a -> IO b ) -> a -> IO ( Either IOException b ) -tryIO f arg = try $ f arg - - -{-| - Sends the desired input to the process std_in and then reads from std out. - Working smt with this method: - - z3 - - mathSat - - cvc4 --} -send :: Process -> String -> IO String -send (Just hIn, Just hOut,_,_) cmd = do - let put_str = flip hPutStr cmd - resPut <-tryIO put_str hIn -- trys to write to std in - case resPut of - --If there was an excepion writing then return the error - Left exception -> return $ "send1: " ++ show exception - Right _ -> do -- if it was successeful - resFlush <- tryIO hFlush hIn -- trys to flush std in - case resFlush of - --if there was an exception flushing then return the error - Left exception -> return $ "send2: " ++ show exception - --if it was succeful then start reading from the std out - Right _ -> readResponse (-1) "" hOut - - -{-| - Receive a inital time to wait for the process to write to the handle, - a String wich will be added the text read from the handle and the handle. - If it was able to read a line from the handle then call the function again - but with time equals to 10. - Working smt with this methid: - - z3 - - mathSat - - cvc4 --} -readResponse :: Int -> String -> Handle -> IO String -readResponse time str procHandle = do - -- if the process dosent write to std out this function will block. - let hWait = flip hWaitForInput time - readOut <- tryIO hWait procHandle -- trys to wait for some output in std out. - case readOut of - -- if the wait gave an exception returns the error. - Left exception -> return $ "readResponse1:" ++ show exception - Right False -> return str -- returns the lines read until now. - Right True -> do - -- if there is something to read then trys to read a line. - res_get <- tryIO hGetLine procHandle - case res_get of - -- if there was an exception then return it. - Left exception -> return $ "readResponse2:" ++ show exception - -- if some text was read then trys to read the pipe again. - Right text -> readResponse 10 (str++text) procHandle - - - --- | Sends the signal to terminate to the running process. -endProcess :: Process -> IO ExitCode -endProcess (_,_,_,processHandle) = do - terminateProcess processHandle - waitForProcess processHandle - - - --- Function used in ContextMode - -{-| - It's the same function as readProcess. - - -} -sendContext :: CmdPath -> Args -> Context -> IO String -sendContext = readProcess - - - -{-| -Calls readProcess and pass as arguments the arguments given plus the name of -the file with the context. -An empty String is passed to the std_in. - -It's the same function as readProcess. -readProcess: - --} -sendScript :: CmdPath -> Args -> FilePath -> IO String -sendScript cmdPath args script_name = - readProcess cmdPath (args ++ [script_name]) "" + {- | +Module : Process + + The following module contains method that facilitate the comunication with + the SMTSolvers. +-} +module Hsmtlib.Solvers.Cmd.ProcCom.Process + ( beginProcess + , send + , endProcess + , sendContext + , sendScript + , sendCvc4 + , Process + , CmdPath + , Args + ) where + +import Control.Exception +import GHC.IO.Handle +import System.Exit +import System.Process +-- | Path to the process +type CmdPath = String + +-- | Argumants passed to process +type Args = [String] + +-- |Type returned by CreateProcess +type Process = + ( Maybe Handle -- process std_in pipe + , Maybe Handle -- process std_out pipe + , Maybe Handle -- process std_err pipe + , ProcessHandle -- process pid + ) + +-- | Context is just a string wich will be sent to std_in +type Context = String + + +-- Functions used in Online Mode + + +{- | + Generates a CreateProcess + with just the command, + the arguments + and creates the pipes to comunicate + -} + +newProcess :: CmdPath -> Args -> CreateProcess +newProcess p a = CreateProcess + { cmdspec = RawCommand p a + , cwd = Nothing + , env = Nothing + , std_in = CreatePipe + , std_out = CreatePipe + , std_err = CreatePipe + , close_fds = False + , create_group = False + --, delegate_ctlc= True + } + +-- | Creates a Process ready to be executed. +beginProcess :: CmdPath -> Args -> IO Process +beginProcess cmd path = createProcess (newProcess cmd path) +{-- + +beginProcess :: CmdPath -> Args -> IO Process +beginProcess cmdPath args = runInteractiveProcess cmdPath args Nothing Nothing +--} +-- | trys to run the function. +tryIO ::(a -> IO b ) -> a -> IO ( Either IOException b ) +tryIO f arg = try $ f arg + + +{- + ######################################################################### + # # + # Functions to send command and read from cvc4 # + # # + ######################################################################### +-} + + + +{-| + Sends the desired input to the process std_in and then reads from std out. + Working smt with this method: + -Cvc4 +-} +sendCvc4 :: Process -> String -> IO String +sendCvc4 (Just hIn, Just hOut, _, _) cmd = do + let put_str = flip hPutStr cmd + resPut <-tryIO put_str hIn -- trys to write to std in + case resPut of + --If there was an excepion writing then return the error + Left exception -> return $ "send1: " ++ show exception + Right _ -> do -- if it was successeful + resFlush <- tryIO hFlush hIn -- trys to flush std in + case resFlush of + --if there was an exception flushing then return the error + Left exception -> return $ "send2: " ++ show exception + --if it was succeful then start reading from the std out + Right _ -> do + -- the first line in the buffer is the command written + -- so we throw it away. + res<- hGetLine hOut + let b = reverse $ drop 1 $reverse cmd -- drop new line in linux + case res == b of + True -> readResponseCvc4 (-1) "" hOut -- linux + False -> readResponseCvc4 (10) res hOut -- windows + + +{-| + Receive a inital time to wait for the process to write to the handle, + a String wich will be added the text read from the handle and the handle. + If it was able to read a line from the handle then call the function again + but with time equals to 10. + Working smt with this methid: + -Cvc4 +-} +readResponseCvc4 :: Int -> String -> Handle -> IO String +readResponseCvc4 time str procHandle = do + -- if the process dosent write to std out this function will block. + let hWait = flip hWaitForInput time + readOut <- tryIO hWait procHandle -- trys to wait for some output in std out. + case readOut of + -- if the wait gave an exception returns the error. + Left exception -> return $ "readResponse1:" ++ show exception + Right False -> return str -- returns the lines read until now. + Right True -> do + -- if there is something to read then trys to read a line. + res_get <- tryIO hGetLine procHandle + case res_get of + -- if there was an exception then return it. + Left exception -> return $ "readResponse2:" ++ show exception + -- if some text was read then trys to read the pipe again. + Right text -> readResponse 10 (str++text) procHandle + + + + + + +{- + ######################################################################### + # # + # Functions to send command and read from most solvers # + # # + ######################################################################### +-} + + + +{-| + Sends the desired input to the process std_in and then reads from std out. + Working smt with this method: + - z3 + - mathSat +-} +send :: Process -> String -> IO String +send (Just hIn, Just hOut, _, _) cmd = do + let put_str = flip hPutStr cmd + resPut <-tryIO put_str hIn -- trys to write to std in + case resPut of + --If there was an excepion writing then return the error + Left exception -> return $ "send1: " ++ show exception + Right _ -> do -- if it was successeful + resFlush <- tryIO hFlush hIn -- trys to flush std in + case resFlush of + --if there was an exception flushing then return the error + Left exception -> return $ "send2: " ++ show exception + --if it was succeful then start reading from the std out + Right _ -> readResponse (-1) "" hOut + +{-| + Receive a inital time to wait for the process to write to the handle, + a String wich will be added the text read from the handle and the handle. + If it was able to read a line from the handle then call the function again + but with time equals to 10. + Working smt with this methid: + - z3 + - mathSat +-} +readResponse :: Int -> String -> Handle -> IO String +readResponse time str procHandle = do + -- if the process dosent write to std out this function will block. + let hWait = flip hWaitForInput time + readOut <- tryIO hWait procHandle -- trys to wait for some output in std out. + case readOut of + -- if the wait gave an exception returns the error. + Left exception -> return $ "readResponse1:" ++ show exception + Right False -> return str -- returns the lines read until now. + Right True -> do + -- if there is something to read then trys to read a line. + res_get <- tryIO hGetLine procHandle + case res_get of + -- if there was an exception then return it. + Left exception -> return $ "readResponse2:" ++ show exception + -- if some text was read then trys to read the pipe again. + Right text -> readResponse 10 (str++text) procHandle + + + + + + +-- | Sends the signal to terminate to the running process. +endProcess :: Process -> IO ExitCode +endProcess (_,_,_,processHandle) = do + terminateProcess processHandle + waitForProcess processHandle + + + +-- Function used in ContextMode + +{-| + It's the same function as readProcess. + + -} +sendContext :: CmdPath -> Args -> Context -> IO String +sendContext = readProcess + + + +{-| +Calls readProcess and pass as arguments the arguments given plus the name of +the file with the context. +An empty String is passed to the std_in. + +It's the same function as readProcess. +readProcess: + +-} + +tryIOError:: IO a -> IO (Either IOError a) +tryIOError = try + +sendScript :: CmdPath -> Args -> FilePath -> IO String +sendScript cmdPath args script_name = do + res <- tryIOError$ readProcess cmdPath (args ++ [script_name]) "" + case res of + Left err -> return (show err) + Right val -> return val diff --git a/Hsmtlib/Solvers/Cmd/ResultHelpers.hs b/Hsmtlib/Solvers/Cmd/ResultHelpers.hs new file mode 100644 --- /dev/null +++ b/Hsmtlib/Solvers/Cmd/ResultHelpers.hs @@ -0,0 +1,295 @@ +module Hsmtlib.Solvers.Cmd.ResultHelpers where + +import Control.Applicative ((<$>), (<|>)) +import Control.Monad +import Hsmtlib.Parsers.Syntax as S +import Hsmtlib.Solver as Solv +import Data.Map as M + + +{- | Retrives the value of a BitVector. + Works with: + - Z3. +-} +getBitVec :: ValuationPair -> Maybe GValResult +getBitVec vp = getBitVec' name vhex + where name = getVarName vp + vhex = getHexVal vp + + +-- auxiliar function to getBitVec +getBitVec' :: Maybe String -> Maybe String -> Maybe GValResult +getBitVec' (Just name) (Just vhex) = Just $ Res name $ VHex vhex +getBitVec' _ _ = Nothing + +{- | Retrives the value of a function. + Works with: + - Z3. +-} +getFun :: ValuationPair -> Maybe GValResult +getFun vp = getFun' name value + where name = getFunName vp + value = getFunResult vp + +-- auxiliar function to getFun +getFun' :: Maybe String -> Maybe Value -> Maybe GValResult +getFun' (Just name) (Just res) = Just $ Res name res +getFun' _ _ = Nothing + + +{- | Retrives the value of a variable. + Works with: + - Z3. +-} +getVar :: ValuationPair -> Maybe GValResult +getVar vp = getVar' name value + where name = getVarName vp + value = getVarValue vp + +-- auxiliar function to getVar +getVar' :: Maybe String -> Maybe Integer -> Maybe GValResult +getVar' Nothing _ = Nothing +getVar' _ Nothing = Nothing +getVar' (Just name) (Just value) = Just $ Res name $ VInt value + + + + +{- | Retrives the value of an array. + Works with: + - Z3. +-} +getArray :: ValuationPair -> Maybe GValResult +getArray vp = + case isArr of + Nothing -> Nothing + Just _ -> case res of + Just arr -> Just $ VArrays arr + Nothing -> Nothing + + where name = arrayName vp + posInt = arrayIntPos vp + posVar = arrayVarPos vp + val = arrayVal vp + isArr = isArray vp + res = getArray' name posInt posVar val + + +-- Auxiliar function to getArray. +getArray' :: Maybe String + -> Maybe Integer + -> Maybe String + -> Maybe Integer + -> Maybe Arrays +getArray' (Just name) (Just pos) Nothing (Just val) = + Just $ singleton name $ singleton (show pos) val +getArray' (Just name) Nothing (Just pos) (Just val) = + Just $ singleton name $ singleton pos val +getArray' _ _ _ _ = Nothing + + + + +-- Auxiliar functions to get values from constructed ast. + + + + + +isArray :: ValuationPair -> Maybe Bool +isArray = isArray' + <=< symbol + <=< qIdentifier + <=< fstTermQualIdentierT + <=< fstTerm + + +{- | Verifies if the string correspond to a certain notation that indicates + that is an Array. + For example Z3 would have the keyword select therefor it's an array. + If it isn't an array then returns nothing + +-} +isArray' :: String -> Maybe Bool +isArray' "select" = Just True +isArray' _ = Nothing + + +-- Auxliar functions to work with arrays. +{- | Retrives the name of the array. + Works with: + - Z3. +-} + +arrayName :: ValuationPair -> Maybe String +arrayName = symbol + <=< qIdentifier + <=< termQualIdentifier + <=< fstValArray + <=< sndTermQualIdentierT + <=< fstTerm + where fstValArray x = Just $ head x + +{-| Retrives the position of the array if it is an Integer. + Works with: + - Z3. +-} +arrayIntPos :: ValuationPair -> Maybe Integer +arrayIntPos = numeral + <=< getTermSpecConstant + <=< sndValArray + <=< sndTermQualIdentierT + <=< fstTerm + where sndValArray x = Just $ x !! 1 + +{-| Retrives the position of the array if it is a String. + Works with: + - Z3. +-} +arrayVarPos :: ValuationPair -> Maybe String +arrayVarPos = symbol + <=< qIdentifier + <=< termQualIdentifier + <=< sndValArray + <=< sndTermQualIdentierT + <=< fstTerm + where sndValArray x = Just $ x !! 1 + + +{-| Retrives the value of an array. + Works with: + - Z3. +-} +arrayVal :: ValuationPair -> Maybe Integer +arrayVal = numeral <=< getTermSpecConstant <=< sndTerm + + + +{- | Retrive the name of a variable. + Works with: + - Z3. + +-} + +getVarName :: ValuationPair -> Maybe String +getVarName = symbol <=< qIdentifier <=< termQualIdentifier <=< fstTerm + + +{- | Retrive the variable of a variable. + Works with: + - Z3. + +-} +getVarValue :: ValuationPair -> Maybe Integer +getVarValue = numeral <=< getTermSpecConstant <=< sndTerm + + + +{- | Retrives the name of a function. + Works with: + - Z3 +-} +getFunName :: ValuationPair -> Maybe String +getFunName = symbol <=< qIdentifier <=< fstTermQualIdentierT <=< fstTerm + + + +{- | Retrives the result of a function if it is a Integer. + Works with: + - Z3. +-} + + +getFunResult :: ValuationPair -> Maybe Value +getFunResult vp = getFunResultBool vp <|> getFunResultInt vp + +getFunResultBool :: ValuationPair -> Maybe Value +getFunResultBool = VBool <#> toBool <=< getFunResultBool' + + +getFunResultInt :: ValuationPair -> Maybe Value +getFunResultInt = VInt <#> getFunResultInt' + + +{- + ######################################################################### + # # + # Auxiliar functions to acess Syntax # + # # + ######################################################################### +-} + + +(<#>):: Functor m => (b -> c) -> (a -> m b) -> a -> m c +(f <#> m) x = f <$> m x + +toBool :: String -> Maybe Bool +toBool "true" = Just True +toBool "false" = Just False +toBool _ = Nothing + +getFunResultInt' :: ValuationPair -> Maybe Integer +getFunResultInt' = numeral <=< getTermSpecConstant <=< sndTerm + + +getFunResultBool' :: ValuationPair -> Maybe String +getFunResultBool' = symbol <=< qIdentifier <=< termQualIdentifier <=< sndTerm + + +{- | Retrives the result of a bitvector. + Works with: + - Z3 +-} +getHexVal :: ValuationPair -> Maybe String +getHexVal = hex <=< getTermSpecConstant <=< fstTerm + + +-- Auxiliar functions to get specific value from ast. + + +-- | Returns the first term of a valuation pair. +fstTerm :: ValuationPair -> Maybe Term +fstTerm (ValuationPair a _) = Just a + + +-- | Returns the second term of a valuation pair. +sndTerm :: ValuationPair -> Maybe Term +sndTerm (ValuationPair _ b) = Just b + + +-- | Returns the list of terms from TermQualIdeintifierT +sndTermQualIdentierT :: Term -> Maybe [Term] +sndTermQualIdentierT (TermQualIdentifierT _ ts) = Just ts +sndTermQualIdentierT _ = Nothing + +fstTermQualIdentierT :: Term -> Maybe QualIdentifier +fstTermQualIdentierT (TermQualIdentifierT qi _) = Just qi +fstTermQualIdentierT _ = Nothing + + +termQualIdentifier :: Term -> Maybe QualIdentifier +termQualIdentifier (TermQualIdentifier a) = Just a +termQualIdentifier _ = Nothing + + +getTermSpecConstant :: Term -> Maybe SpecConstant +getTermSpecConstant (TermSpecConstant spc) = Just spc +getTermSpecConstant _ = Nothing + + +qIdentifier :: QualIdentifier -> Maybe Identifier +qIdentifier (QIdentifier a) = Just a +qIdentifier _ = Nothing + +symbol :: Identifier -> Maybe String +symbol (ISymbol s) = Just s +symbol _ = Nothing + + +numeral :: SpecConstant -> Maybe Integer +numeral (SpecConstantNumeral n) = Just n +numeral _ = Nothing + +hex :: SpecConstant -> Maybe String +hex (SpecConstantHexadecimal shex) = Just shex +hex _ = Nothing diff --git a/Hsmtlib/Solvers/Cmd/ScriptCmd.hs b/Hsmtlib/Solvers/Cmd/ScriptCmd.hs --- a/Hsmtlib/Solvers/Cmd/ScriptCmd.hs +++ b/Hsmtlib/Solvers/Cmd/ScriptCmd.hs @@ -1,129 +1,167 @@ -{- | -Module : ScriptCmd - -Module with the functions used in script Mode. --} -module Hsmtlib.Solvers.Cmd.ScriptCmd where - -import Control.Applicative (liftA) -import Hsmtlib.Solver -import Hsmtlib.Solvers.Cmd.Parser.CmdResult -import Hsmtlib.Solvers.Cmd.ProcCom.Process -import SMTLib2 -import System.IO (Handle, hClose, hFlush, - hPutStr) -import Text.PrettyPrint - --- Data that hass the arguments for the script -data ScriptConf = ScriptConf - { sHandle :: Handle -- Handle of the script file. - , sCmdPath :: CmdPath -- Path of the solver. - , sArgs :: Args -- Args of the solver. - , sFilePath :: FilePath -- File path of the script. - } - ---Writes to the script the command given. -writeToScript :: ScriptConf -> Command -> IO () -writeToScript sConf cmd = do - let scmd = render (pp cmd) ++ "\n" - hPutStr (sHandle sConf) scmd - hFlush (sHandle sConf) - - ---Function that only writes to the script a command and returns an empty string -scriptFun :: ScriptConf -> Command -> IO String -scriptFun sConf cmd = writeToScript sConf cmd >> return "" - ---Function that writes to the script a comaand, executes the solver and reads ---the response. -scriptFunExec :: ScriptConf -> Command -> IO String -scriptFunExec sConf cmd = do - writeToScript sConf cmd - res <- sendScript (sCmdPath sConf) (sArgs sConf) (sFilePath sConf) - return $ last $ lines res - - - -scriptGenResponse :: ScriptConf -> Command -> IO GenResult -scriptGenResponse sConf cmd = writeToScript sConf cmd >> return Success - - -scriptCheckSatResponse :: ScriptConf -> Command -> IO SatResult -scriptCheckSatResponse conf cmd = - liftA checkSatResponse (scriptFunExec conf cmd) - -scriptGetValueResponse :: ScriptConf -> Command -> IO GValResult -scriptGetValueResponse conf cmd = - liftA getValueResponse (scriptFunExec conf cmd) - - ---SMT Commands. - --- scriptCheckSat, scriptGetAssertins, scriptGetValue, scriptGetValue, --- scriptGetProof, scriptGetUnsatCore, scriptGetInfo, scriptGetOption, --- script Exit. ---All above functions use ScriptFunExc the rest use scriptFun. - - -scriptSetLogic :: ScriptConf -> Name -> IO GenResult -scriptSetLogic sConf name = scriptGenResponse sConf (CmdSetLogic name ) - -scriptSetOption :: ScriptConf -> Option -> IO GenResult -scriptSetOption sConf option = scriptGenResponse sConf (CmdSetOption option) - -scriptSetInfo :: ScriptConf -> Attr -> IO GenResult -scriptSetInfo sConf attr = scriptGenResponse sConf (CmdSetInfo attr) - -scriptDeclareType :: ScriptConf -> Name -> Integer -> IO GenResult -scriptDeclareType sConf name number = - scriptGenResponse sConf (CmdDeclareType name number) - -scriptDefineType :: ScriptConf -> Name -> [Name] -> Type -> IO GenResult -scriptDefineType sConf name names t = - scriptGenResponse sConf (CmdDefineType name names t) - -scriptDeclareFun :: ScriptConf -> Name -> [Type] -> Type -> IO GenResult -scriptDeclareFun sConf name lt t = - scriptGenResponse sConf (CmdDeclareFun name lt t) - -scriptDefineFun :: ScriptConf -> Name -> [Binder] -> Type -> Expr -> IO GenResult -scriptDefineFun sConf name binders t expression = - scriptGenResponse sConf (CmdDefineFun name binders t expression) - -scriptPush :: ScriptConf -> Integer -> IO GenResult -scriptPush sConf number = scriptGenResponse sConf (CmdPush number) - -scriptPop :: ScriptConf -> Integer -> IO GenResult -scriptPop sConf number = - scriptGenResponse sConf (CmdPop number) - -scriptAssert :: ScriptConf -> Expr -> IO GenResult -scriptAssert sConf expression = - scriptGenResponse sConf (CmdAssert expression) - -scriptCheckSat :: ScriptConf -> IO SatResult -scriptCheckSat sConf = scriptCheckSatResponse sConf CmdCheckSat - -scriptGetAssertions :: ScriptConf -> IO String -scriptGetAssertions sConf = scriptFunExec sConf CmdGetAssertions - -scriptGetValue :: ScriptConf -> [Expr] -> IO GValResult -scriptGetValue sConf exprs = scriptGetValueResponse sConf (CmdGetValue exprs) - -scriptGetProof :: ScriptConf -> IO String -scriptGetProof sConf = scriptFunExec sConf CmdGetProof - -scriptGetUnsatCore :: ScriptConf -> IO String -scriptGetUnsatCore sConf = scriptFunExec sConf CmdGetUnsatCore - -scriptGetInfo :: ScriptConf-> InfoFlag -> IO String -scriptGetInfo sConf info = scriptFunExec sConf ( CmdGetInfo info ) - -scriptGetOption :: ScriptConf -> Name -> IO String -scriptGetOption sConf name = scriptFunExec sConf ( CmdGetOption name ) - -scriptExit :: ScriptConf -> IO String -scriptExit sConf = do - result <- scriptFunExec sConf CmdExit --Write to the script and execute - hClose (sHandle sConf) -- close the handle of the script - return result +{- | +Module : ScriptCmd + +Module with the functions used in script Mode. +-} +module Hsmtlib.Solvers.Cmd.ScriptCmd where + +import Control.Applicative (liftA) +import Hsmtlib.Parsers.Syntax (GenResponse (Success)) +import Hsmtlib.Solver +import Hsmtlib.Solvers.Cmd.CmdResult +import Hsmtlib.Solvers.Cmd.ProcCom.Process +import SMTLib2 +import System.IO (Handle, hClose, hFlush, + hPutStr) +import Text.PrettyPrint + +-- Data that hass the arguments for the script +data ScriptConf = ScriptConf + { sHandle :: Handle -- Handle of the script file. + , sCmdPath :: CmdPath -- Path of the solver. + , sArgs :: Args -- Args of the solver. + , sFilePath :: FilePath -- File path of the script. + } + + + + + +--Writes to the script the command given. +writeToScript :: ScriptConf -> Command -> IO () +writeToScript sConf cmd = do + let scmd = render (pp cmd) ++ "\n" + hPutStr (sHandle sConf) scmd + hFlush (sHandle sConf) + + +--Function that only writes to the script a command and returns an empty string +scriptFun :: ScriptConf -> Command -> IO String +scriptFun sConf cmd = writeToScript sConf cmd >> return "" + +--Function that writes to the script a comaand, executes the solver and reads +--the response. +scriptFunExec :: ScriptConf -> Command -> IO String +scriptFunExec sConf cmd = do + writeToScript sConf cmd + res <- sendScript (sCmdPath sConf) (sArgs sConf) (sFilePath sConf) + return $ last $lines res + + + +scriptGenResponse :: ScriptConf -> Command -> IO Result +scriptGenResponse sConf cmd = writeToScript sConf cmd >> return (CGR Success) + + +scriptCheckSatResponse :: ScriptConf -> Command -> IO Result +scriptCheckSatResponse conf cmd = + liftA checkSatResponse (scriptFunExec conf cmd) + + +scriptGetValueResponse :: ScriptConf -> Command -> IO Result +scriptGetValueResponse conf cmd = + liftA getValueResponse (scriptFunExec conf cmd) + + +scriptGetInfoResponse :: ScriptConf -> Command -> IO Result +scriptGetInfoResponse conf cmd = + liftA getInfoResponse (scriptFunExec conf cmd) + + +scriptGetAssertionResponse :: ScriptConf -> Command -> IO Result +scriptGetAssertionResponse conf cmd = + liftA getAssertionResponse (scriptFunExec conf cmd) + +scriptGetProofResponse :: ScriptConf -> Command -> IO Result +scriptGetProofResponse conf cmd = + liftA getProofResponse (scriptFunExec conf cmd) + + +scriptGetUnsatCoreResponse :: ScriptConf -> Command -> IO Result +scriptGetUnsatCoreResponse conf cmd = + liftA getUnsatCoreResponse (scriptFunExec conf cmd) + + +scriptGetAssignmentResponse :: ScriptConf -> Command -> IO Result +scriptGetAssignmentResponse conf cmd = + liftA getAssignmentResponse (scriptFunExec conf cmd) + + +scriptGetOptionResponse :: ScriptConf -> Command -> IO Result +scriptGetOptionResponse conf cmd = + liftA getOptionResponse (scriptFunExec conf cmd) + + + + + +--SMT Commands. + +-- scriptCheckSat, scriptGetAssertins, scriptGetValue, scriptGetValue, +-- scriptGetProof, scriptGetUnsatCore, scriptGetInfo, scriptGetOption, +-- script Exit. +--All above functions use ScriptFunExc the rest use scriptFun. + + +scriptSetLogic :: ScriptConf -> Name -> IO Result +scriptSetLogic sConf name = scriptGenResponse sConf (CmdSetLogic name ) + +scriptSetOption :: ScriptConf -> Option -> IO Result +scriptSetOption sConf option = scriptGenResponse sConf (CmdSetOption option) + +scriptSetInfo :: ScriptConf -> Attr -> IO Result +scriptSetInfo sConf attr = scriptGenResponse sConf (CmdSetInfo attr) + +scriptDeclareType :: ScriptConf -> Name -> Integer -> IO Result +scriptDeclareType sConf name number = + scriptGenResponse sConf (CmdDeclareType name number) + +scriptDefineType :: ScriptConf -> Name -> [Name] -> Type -> IO Result +scriptDefineType sConf name names t = + scriptGenResponse sConf (CmdDefineType name names t) + +scriptDeclareFun :: ScriptConf -> Name -> [Type] -> Type -> IO Result +scriptDeclareFun sConf name lt t = + scriptGenResponse sConf (CmdDeclareFun name lt t) + +scriptDefineFun :: ScriptConf -> Name -> [Binder] -> Type -> Expr -> IO Result +scriptDefineFun sConf name binders t expression = + scriptGenResponse sConf (CmdDefineFun name binders t expression) + +scriptPush :: ScriptConf -> Integer -> IO Result +scriptPush sConf number = scriptGenResponse sConf (CmdPush number) + +scriptPop :: ScriptConf -> Integer -> IO Result +scriptPop sConf number = + scriptGenResponse sConf (CmdPop number) + +scriptAssert :: ScriptConf -> Expr -> IO Result +scriptAssert sConf expression = + scriptGenResponse sConf (CmdAssert expression) + +scriptCheckSat :: ScriptConf -> IO Result +scriptCheckSat sConf = scriptCheckSatResponse sConf CmdCheckSat + +scriptGetAssertions :: ScriptConf -> IO Result +scriptGetAssertions sConf = scriptGetAssertionResponse sConf CmdGetAssertions + +scriptGetValue :: ScriptConf -> [Expr] -> IO Result +scriptGetValue sConf exprs = scriptGetValueResponse sConf (CmdGetValue exprs) + +scriptGetProof :: ScriptConf -> IO Result +scriptGetProof sConf = scriptGetProofResponse sConf CmdGetProof + +scriptGetUnsatCore :: ScriptConf -> IO Result +scriptGetUnsatCore sConf = scriptGetUnsatCoreResponse sConf CmdGetUnsatCore + +scriptGetInfo :: ScriptConf-> InfoFlag -> IO Result +scriptGetInfo sConf info = scriptGetInfoResponse sConf (CmdGetInfo info) + +scriptGetOption :: ScriptConf -> Name -> IO Result +scriptGetOption sConf name = scriptGetOptionResponse sConf (CmdGetOption name) + +scriptExit :: ScriptConf -> IO Result +scriptExit sConf = do + _ <- scriptFun sConf CmdExit --Write to the script and execute + hClose (sHandle sConf) -- close the handle of the script + return (CGR Success) diff --git a/Hsmtlib/Solvers/Cvc4.hs b/Hsmtlib/Solvers/Cvc4.hs --- a/Hsmtlib/Solvers/Cvc4.hs +++ b/Hsmtlib/Solvers/Cvc4.hs @@ -1,185 +1,185 @@ -{- | -Module : Hsmtlib.Solvers.Cvc4 - Module wich has the standard configuration for all Cvc4 Modes and - provides the initilizing function. --} -module Hsmtlib.Solvers.Cvc4(startCvc4) where - - -import Hsmtlib.Solver as Slv -import Hsmtlib.Solvers.Cmd.BatchCmd as B (executeBatch) -import Hsmtlib.Solvers.Cmd.OnlineCmd -import Hsmtlib.Solvers.Cmd.ProcCom.Process -import Hsmtlib.Solvers.Cmd.ScriptCmd -import SMTLib2 -import System.IO (Handle, - IOMode (WriteMode), - openFile) - -{- - TODO: Why the flag --status frezzes the process. --} - -cvc4ConfigOnline :: SolverConfig -cvc4ConfigOnline = - Config { path = "cvc4" - , args = ["--interactive", "--lang=smt2", "--quiet"] - } - --- Both Script configurations are the same but have diferent names --- so if anything changes it's easy to alter its configuration. - -cvc4ConfigScript :: SolverConfig -cvc4ConfigScript = - Config { path = "cvc4" - , args = ["--lang=smt2"] - } - -cvc4ConfigBatch :: SolverConfig -cvc4ConfigBatch = - Config { path = "cvc4" - , args = ["--lang=smt2"] - } - -{- | - Function that initialyzes a Cvc4 Solver. - It Receives a Mode, an SMT Logic, it can receive a diferent configuration - for the solver and an anternative path to create the script in Script Mode. - - In Context and Online Mode if a FilePath is passed then it's ignored. --} -startCvc4 :: Mode -> String -> Maybe SolverConfig -> Maybe FilePath -> IO Solver -startCvc4 Slv.Batch logic sConf _ = startCvc4Batch logic sConf -startCvc4 Slv.Online logic sConf _ = startCvc4Online logic sConf -startCvc4 Slv.Script logic sConf scriptFilePath = - startCvc4Script logic sConf scriptFilePath - - - --- Start Cvc4 Online. - -startCvc4Online :: String -> Maybe SolverConfig -> IO Solver -startCvc4Online logic Nothing = startCvc4Online' logic cvc4ConfigOnline -startCvc4Online logic (Just conf) = startCvc4Online' logic conf - -startCvc4Online':: String -> SolverConfig -> IO Solver -startCvc4Online' logic conf = do - -- Starts a Cvc4 Process. - process <- beginProcess (path conf) (args conf) - --Set Option to print success after accepting a Command. - onlineSetOption process (OptPrintSuccess True) - -- Sets the SMT Logic. - onlineSetLogic process (N logic) - -- Initialize the solver Functions and return them. - return $ onlineSolver process - - ---Start Cvc4 Script. - -startCvc4Script :: String -> Maybe SolverConfig -> Maybe FilePath -> IO Solver -startCvc4Script logic Nothing Nothing = - startCvc4Script' logic cvc4ConfigScript "temp.smt2" -startCvc4Script logic (Just conf) Nothing = - startCvc4Script' logic conf "temp.smt2" -startCvc4Script logic Nothing (Just scriptFilePath) = - startCvc4Script' logic cvc4ConfigScript scriptFilePath -startCvc4Script logic (Just conf) (Just scriptFilePath) = - startCvc4Script' logic conf scriptFilePath - -{- - In this function a file is created where the commands are kept. - - Every function in the ScriptCmd Module needs a ScriptConf data which has: - - - sHandle: The handle of the script file - - sCmdPath: The Path to initilyze the solver - - sArgs: The options of the solver - - sFilePath: The file path of the script so it can be passed to the solver - when started. --} -startCvc4Script' :: String -> SolverConfig -> FilePath -> IO Solver -startCvc4Script' logic conf scriptFilePath = do - -- Create a file with the give file path. - -- Since the handle is created with WriteMode it overrides a file if it - -- already exists. - scriptHandle <- openFile scriptFilePath WriteMode - -- Creates the arguments for the functions in ScriptCmd - let srcmd = newScriptArgs conf scriptHandle scriptFilePath - --Set Option to print success after accepting a Command. - scriptSetOption srcmd (OptPrintSuccess True) - -- Initialize the solver Functions and return them. - scriptSetLogic srcmd (N logic) - return $ scriptSolver srcmd - ---Function which creates the ScriptConf for the script functions. -newScriptArgs :: SolverConfig -> Handle -> FilePath -> ScriptConf -newScriptArgs solverConfig nHandle scriptFilePath = - ScriptConf { sHandle = nHandle - , sCmdPath = path solverConfig - , sArgs = args solverConfig - , sFilePath = scriptFilePath - } - - --- start Cvc4 Batch -startCvc4Batch :: String -> Maybe SolverConfig -> IO Solver -startCvc4Batch logic Nothing = startCvc4Batch' logic cvc4ConfigBatch -startCvc4Batch logic (Just conf) = startCvc4Batch' logic conf - -startCvc4Batch' :: String -> SolverConfig -> IO Solver -startCvc4Batch' logic conf = return $ batchSolver logic conf - - - --- Creates the functions for online mode with the process already running. --- Each function will send the command to the solver and wait for the response. -onlineSolver :: Process -> Solver -onlineSolver process = - Solver { setLogic = onlineSetLogic process - , setOption = onlineSetOption process - , setInfo = onlineSetInfo process - , declareType = onlineDeclareType process - , defineType = onlineDefineType process - , declareFun = onlineDeclareFun process - , defineFun = onlineDefineFun process - , push = onlinePush process - , pop = onlinePop process - , assert = onlineAssert process - , checkSat = onlineCheckSat process - , getAssertions = onlineGetAssertions process - , getValue = onlineGetValue process - , getProof = onlineGetProof process - , getUnsatCore = onlineGetUnsatCore process - , getInfo = onlineGetInfo process - , getOption = onlineGetOption process - , exit = onlineExit process - } - --- Creates the funtion for the script mode. --- The configuration of the file is passed. -scriptSolver :: ScriptConf -> Solver -scriptSolver srcmd = - Solver { setLogic = scriptSetLogic srcmd - , setOption = scriptSetOption srcmd - , setInfo = scriptSetInfo srcmd - , declareType = scriptDeclareType srcmd - , defineType = scriptDefineType srcmd - , declareFun = scriptDeclareFun srcmd - , defineFun = scriptDefineFun srcmd - , push = scriptPush srcmd - , pop = scriptPop srcmd - , assert = scriptAssert srcmd - , checkSat = scriptCheckSat srcmd - , getAssertions = scriptGetAssertions srcmd - , getValue = scriptGetValue srcmd - , getProof = scriptGetProof srcmd - , getUnsatCore = scriptGetUnsatCore srcmd - , getInfo = scriptGetInfo srcmd - , getOption = scriptGetOption srcmd - , exit = scriptExit srcmd - } - - -batchSolver :: String -> SolverConfig -> Solver -batchSolver logic config = - BSolver { Slv.executeBatch = B.executeBatch (path config) (args config) logic} +{- | +Module : Hsmtlib.Solvers.Cvc4 + Module wich has the standard configuration for all Cvc4 Modes and + provides the initilizing function. +-} +module Hsmtlib.Solvers.Cvc4(startCvc4) where + + +import Hsmtlib.Solver as Slv +import Hsmtlib.Solvers.Cmd.BatchCmd as B (executeBatch) +import Hsmtlib.Solvers.Cmd.OnlineCmd +import Hsmtlib.Solvers.Cmd.ProcCom.Process +import Hsmtlib.Solvers.Cmd.ScriptCmd +import SMTLib2 +import System.IO (Handle, + IOMode (WriteMode), + openFile) + +{- + TODO: Why the flag --status frezzes the process. +-} + +cvc4ConfigOnline :: SolverConfig +cvc4ConfigOnline = + Config { path = "cvc4" + , args = ["--interactive", "--smtlib-strict", "--print-success", "-q"] + } + +-- Both Script configurations are the same but have diferent names +-- so if anything changes it's easy to alter its configuration. + +cvc4ConfigScript :: SolverConfig +cvc4ConfigScript = + Config { path = "cvc4" + , args = [] + } + +cvc4ConfigBatch :: SolverConfig +cvc4ConfigBatch = + Config { path = "cvc4" + , args = [] + } + +{- | + Function that initialyzes a Cvc4 Solver. + It Receives a Mode, an SMT Logic, it can receive a diferent configuration + for the solver and an anternative path to create the script in Script Mode. + + In Context and Online Mode if a FilePath is passed then it's ignored. +-} +startCvc4 :: Mode -> String -> Maybe SolverConfig -> Maybe FilePath -> IO Solver +startCvc4 Slv.Batch logic sConf _ = startCvc4Batch logic sConf +startCvc4 Slv.Online logic sConf _ = startCvc4Online logic sConf +startCvc4 Slv.Script logic sConf scriptFilePath = + startCvc4Script logic sConf scriptFilePath + + + +-- Start Cvc4 Online. + +startCvc4Online :: String -> Maybe SolverConfig -> IO Solver +startCvc4Online logic Nothing = startCvc4Online' logic cvc4ConfigOnline +startCvc4Online logic (Just conf) = startCvc4Online' logic conf + +startCvc4Online':: String -> SolverConfig -> IO Solver +startCvc4Online' logic conf = do + -- Starts a Cvc4 Process. + process <- beginProcess (path conf) (args conf) + --Set Option to print success after accepting a Command. + --_ <- onlineSetOption Cvc4 process (OptPrintSuccess True) + -- Sets the SMT Logic. + _ <- onlineSetLogic Cvc4 process (N logic) + -- Initialize the solver Functions and return them. + return $ onlineSolver process + + +--Start Cvc4 Script. + +startCvc4Script :: String -> Maybe SolverConfig -> Maybe FilePath -> IO Solver +startCvc4Script logic Nothing Nothing = + startCvc4Script' logic cvc4ConfigScript "temp.smt2" +startCvc4Script logic (Just conf) Nothing = + startCvc4Script' logic conf "temp.smt2" +startCvc4Script logic Nothing (Just scriptFilePath) = + startCvc4Script' logic cvc4ConfigScript scriptFilePath +startCvc4Script logic (Just conf) (Just scriptFilePath) = + startCvc4Script' logic conf scriptFilePath + +{- + In this function a file is created where the commands are kept. + + Every function in the ScriptCmd Module needs a ScriptConf data which has: + + - sHandle: The handle of the script file + - sCmdPath: The Path to initilyze the solver + - sArgs: The options of the solver + - sFilePath: The file path of the script so it can be passed to the solver + when started. +-} +startCvc4Script' :: String -> SolverConfig -> FilePath -> IO Solver +startCvc4Script' logic conf scriptFilePath = do + -- Create a file with the give file path. + -- Since the handle is created with WriteMode it overrides a file if it + -- already exists. + scriptHandle <- openFile scriptFilePath WriteMode + -- Creates the arguments for the functions in ScriptCmd + let srcmd = newScriptArgs conf scriptHandle scriptFilePath + --Set Option to print success after accepting a Command. + _ <- scriptSetOption srcmd (OptPrintSuccess True) + -- Initialize the solver Functions and return them. + _ <- scriptSetLogic srcmd (N logic) + return $ scriptSolver srcmd + +--Function which creates the ScriptConf for the script functions. +newScriptArgs :: SolverConfig -> Handle -> FilePath -> ScriptConf +newScriptArgs solverConfig nHandle scriptFilePath = + ScriptConf { sHandle = nHandle + , sCmdPath = path solverConfig + , sArgs = args solverConfig + , sFilePath = scriptFilePath + } + + +-- start Cvc4 Batch +startCvc4Batch :: String -> Maybe SolverConfig -> IO Solver +startCvc4Batch logic Nothing = startCvc4Batch' logic cvc4ConfigBatch +startCvc4Batch logic (Just conf) = startCvc4Batch' logic conf + +startCvc4Batch' :: String -> SolverConfig -> IO Solver +startCvc4Batch' logic conf = return $ batchSolver logic conf + + + +-- Creates the functions for online mode with the process already running. +-- Each function will send the command to the solver and wait for the response. +onlineSolver :: Process -> Solver +onlineSolver process = + Solver { setLogic = onlineSetLogic Cvc4 process + , setOption = onlineSetOption Cvc4 process + , setInfo = onlineSetInfo Cvc4 process + , declareType = onlineDeclareType Cvc4 process + , defineType = onlineDefineType Cvc4 process + , declareFun = onlineDeclareFun Cvc4 process + , defineFun = onlineDefineFun Cvc4 process + , push = onlinePush Cvc4 process + , pop = onlinePop Cvc4 process + , assert = onlineAssert Cvc4 process + , checkSat = onlineCheckSat Cvc4 process + , getAssertions = onlineGetAssertions Cvc4 process + , getValue = onlineGetValue Cvc4 process + , getProof = onlineGetProof Cvc4 process + , getUnsatCore = onlineGetUnsatCore Cvc4 process + , getInfo = onlineGetInfo Cvc4 process + , getOption = onlineGetOption Cvc4 process + , exit = onlineExit process + } + +-- Creates the funtion for the script mode. +-- The configuration of the file is passed. +scriptSolver :: ScriptConf -> Solver +scriptSolver srcmd = + Solver { setLogic = scriptSetLogic srcmd + , setOption = scriptSetOption srcmd + , setInfo = scriptSetInfo srcmd + , declareType = scriptDeclareType srcmd + , defineType = scriptDefineType srcmd + , declareFun = scriptDeclareFun srcmd + , defineFun = scriptDefineFun srcmd + , push = scriptPush srcmd + , pop = scriptPop srcmd + , assert = scriptAssert srcmd + , checkSat = scriptCheckSat srcmd + , getAssertions = scriptGetAssertions srcmd + , getValue = scriptGetValue srcmd + , getProof = scriptGetProof srcmd + , getUnsatCore = scriptGetUnsatCore srcmd + , getInfo = scriptGetInfo srcmd + , getOption = scriptGetOption srcmd + , exit = scriptExit srcmd + } + + +batchSolver :: String -> SolverConfig -> Solver +batchSolver logic config = + BSolver { Slv.executeBatch = B.executeBatch (path config) (args config) logic} diff --git a/Hsmtlib/Solvers/MathSAT.hs b/Hsmtlib/Solvers/MathSAT.hs --- a/Hsmtlib/Solvers/MathSAT.hs +++ b/Hsmtlib/Solvers/MathSAT.hs @@ -1,183 +1,183 @@ -{- | -Module : Hsmtlib.Solvers.MathSAT - Module wich has the standard configuration for all mathSat Modes and - provides the initilizing function. --} -module Hsmtlib.Solvers.MathSAT(startMathSat) where - -import Hsmtlib.Solver as Slv -import Hsmtlib.Solvers.Cmd.BatchCmd as B (executeBatch) -import Hsmtlib.Solvers.Cmd.OnlineCmd -import Hsmtlib.Solvers.Cmd.ProcCom.Process -import Hsmtlib.Solvers.Cmd.ScriptCmd -import SMTLib2 -import System.IO (Handle, - IOMode (WriteMode), - openFile) - --- All the configurations are the same but have diferent names so if anything --- changes it's easy to alter its configuration. - - -mathSatConfigOnline :: SolverConfig -mathSatConfigOnline = - Config { path = "mathsat" - , args = [] - } - -mathSatConfigScript :: SolverConfig -mathSatConfigScript = - Config { path = "mathsat" - , args = [] - } - -mathSatConfigBatch :: SolverConfig -mathSatConfigBatch = - Config { path = "mathsat" - , args = [] - } - -{- | - Function that initialyzes a mathSat Solver. - It Receives a Mode, an SMT Logic, it can receive a diferent configuration - for the solver and an anternative path to create the script in Script Mode. - - In Online Mode if a FilePath is passed then it's ignored. --} -startMathSat :: Mode - -> String - -> Maybe SolverConfig - -> Maybe FilePath - -> IO Solver - -startMathSat Slv.Batch logic sConf _ = startMathSatBatch logic sConf -startMathSat Slv.Online logic sConf _ = startMathSatOnline logic sConf -startMathSat Slv.Script logic sConf scriptFilePath = - startMathSatScript logic sConf scriptFilePath - --- Start mathSat Online. - -startMathSatOnline :: String -> Maybe SolverConfig -> IO Solver -startMathSatOnline logic Nothing = - startMathSatOnline' logic mathSatConfigOnline - -startMathSatOnline logic (Just conf) = startMathSatOnline' logic conf - -startMathSatOnline' :: String -> SolverConfig -> IO Solver -startMathSatOnline' logic conf = do - -- Starts a Z4 Process. - process <- beginProcess (path conf) (args conf) - --Set Option to print success after accepting a Command. - onlineSetOption process (OptPrintSuccess True) - -- Sets the SMT Logic. - onlineSetLogic process (N logic) - -- Initialize the solver Functions and return them. - return $ onlineSolver process - ---Start mathSat Script. - -startMathSatScript :: String -> Maybe SolverConfig -> Maybe FilePath -> IO Solver -startMathSatScript logic Nothing Nothing = - startMathSatScript' logic mathSatConfigScript "temp.smt2" -startMathSatScript logic (Just conf) Nothing = - startMathSatScript' logic conf "temp.smt2" -startMathSatScript logic Nothing (Just scriptFilePath) = - startMathSatScript' logic mathSatConfigScript scriptFilePath -startMathSatScript logic (Just conf) (Just scriptFilePath) = - startMathSatScript' logic conf scriptFilePath - -{- - In this function a file is created where the commands are kept. - - Every function in the ScriptCmd Module needs a ScriptConf data which has: - - - sHandle: The handle of the script file - - sCmdPath: The Path to initilyze the solver - - sArgs: The options of the solver - - sFilePath: The file path of the script so it can be passed to the solver - when started. --} -startMathSatScript' :: String -> SolverConfig -> FilePath -> IO Solver -startMathSatScript' logic conf scriptFilePath = do - scriptHandle <- openFile scriptFilePath WriteMode - let srcmd = newScriptArgs conf scriptHandle scriptFilePath - scriptSetOption srcmd (OptPrintSuccess True) - scriptSetLogic srcmd (N logic) - return $ scriptSolver srcmd - ---Function which creates the ScriptConf for the script functions. -newScriptArgs :: SolverConfig -> Handle -> FilePath -> ScriptConf -newScriptArgs solverConfig nHandle scriptFilePath = - ScriptConf { sHandle = nHandle - , sCmdPath = path solverConfig - , sArgs = args solverConfig - , sFilePath = scriptFilePath - } - - --- Start MathSat batch mode - -startMathSatBatch :: String -> Maybe SolverConfig -> IO Solver -startMathSatBatch logic Nothing = startMathSatBatch' logic mathSatConfigBatch -startMathSatBatch logic (Just conf) = startMathSatBatch' logic conf - -startMathSatBatch' :: String -> SolverConfig -> IO Solver -startMathSatBatch' logic conf = return $ batchSolver logic conf - - - - - - --- Creates the functions for online mode with the process already running. --- Each function will send the command to the solver and wait for the response. -onlineSolver :: Process -> Solver -onlineSolver process = - Solver { setLogic = onlineSetLogic process - , setOption = onlineSetOption process - , setInfo = onlineSetInfo process - , declareType = onlineDeclareType process - , defineType = onlineDefineType process - , declareFun = onlineDeclareFun process - , defineFun = onlineDefineFun process - , push = onlinePush process - , pop = onlinePop process - , assert = onlineAssert process - , checkSat = onlineCheckSat process - , getAssertions = onlineGetAssertions process - , getValue = onlineGetValue process - , getProof = onlineGetProof process - , getUnsatCore = onlineGetUnsatCore process - , getInfo = onlineGetInfo process - , getOption = onlineGetOption process - , exit = onlineExit process - } - --- Creates the funtion for the script mode. --- The configuration of the file is passed. -scriptSolver :: ScriptConf -> Solver -scriptSolver srcmd = - Solver { setLogic = scriptSetLogic srcmd - , setOption = scriptSetOption srcmd - , setInfo = scriptSetInfo srcmd - , declareType = scriptDeclareType srcmd - , defineType = scriptDefineType srcmd - , declareFun = scriptDeclareFun srcmd - , defineFun = scriptDefineFun srcmd - , push = scriptPush srcmd - , pop = scriptPop srcmd - , assert = scriptAssert srcmd - , checkSat = scriptCheckSat srcmd - , getAssertions = scriptGetAssertions srcmd - , getValue = scriptGetValue srcmd - , getProof = scriptGetProof srcmd - , getUnsatCore = scriptGetUnsatCore srcmd - , getInfo = scriptGetInfo srcmd - , getOption = scriptGetOption srcmd - , exit = scriptExit srcmd - } - - -batchSolver :: String -> SolverConfig -> Solver -batchSolver logic config = +{- | +Module : Hsmtlib.Solvers.MathSAT + Module wich has the standard configuration for all mathSat Modes and + provides the initilizing function. +-} +module Hsmtlib.Solvers.MathSAT(startMathSat) where + +import Hsmtlib.Solver as Slv +import Hsmtlib.Solvers.Cmd.BatchCmd as B (executeBatch) +import Hsmtlib.Solvers.Cmd.OnlineCmd +import Hsmtlib.Solvers.Cmd.ProcCom.Process +import Hsmtlib.Solvers.Cmd.ScriptCmd +import SMTLib2 +import System.IO (Handle, + IOMode (WriteMode), + openFile) + +-- All the configurations are the same but have diferent names so if anything +-- changes it's easy to alter its configuration. + + +mathSatConfigOnline :: SolverConfig +mathSatConfigOnline = + Config { path = "mathsat" + , args = [] + } + +mathSatConfigScript :: SolverConfig +mathSatConfigScript = + Config { path = "mathsat" + , args = [] + } + +mathSatConfigBatch :: SolverConfig +mathSatConfigBatch = + Config { path = "mathsat" + , args = [] + } + +{- | + Function that initialyzes a mathSat Solver. + It Receives a Mode, an SMT Logic, it can receive a diferent configuration + for the solver and an anternative path to create the script in Script Mode. + + In Online Mode if a FilePath is passed then it's ignored. +-} +startMathSat :: Mode + -> String + -> Maybe SolverConfig + -> Maybe FilePath + -> IO Solver + +startMathSat Slv.Batch logic sConf _ = startMathSatBatch logic sConf +startMathSat Slv.Online logic sConf _ = startMathSatOnline logic sConf +startMathSat Slv.Script logic sConf scriptFilePath = + startMathSatScript logic sConf scriptFilePath + +-- Start mathSat Online. + +startMathSatOnline :: String -> Maybe SolverConfig -> IO Solver +startMathSatOnline logic Nothing = + startMathSatOnline' logic mathSatConfigOnline + +startMathSatOnline logic (Just conf) = startMathSatOnline' logic conf + +startMathSatOnline' :: String -> SolverConfig -> IO Solver +startMathSatOnline' logic conf = do + -- Starts a Z4 Process. + process <- beginProcess (path conf) (args conf) + --Set Option to print success after accepting a Command. + _ <- onlineSetOption Mathsat process (OptPrintSuccess True) + -- Sets the SMT Logic. + _ <- onlineSetLogic Mathsat process (N logic) + -- Initialize the solver Functions and return them. + return $ onlineSolver process + +--Start mathSat Script. + +startMathSatScript :: String -> Maybe SolverConfig -> Maybe FilePath -> IO Solver +startMathSatScript logic Nothing Nothing = + startMathSatScript' logic mathSatConfigScript "temp.smt2" +startMathSatScript logic (Just conf) Nothing = + startMathSatScript' logic conf "temp.smt2" +startMathSatScript logic Nothing (Just scriptFilePath) = + startMathSatScript' logic mathSatConfigScript scriptFilePath +startMathSatScript logic (Just conf) (Just scriptFilePath) = + startMathSatScript' logic conf scriptFilePath + +{- + In this function a file is created where the commands are kept. + + Every function in the ScriptCmd Module needs a ScriptConf data which has: + + - sHandle: The handle of the script file + - sCmdPath: The Path to initilyze the solver + - sArgs: The options of the solver + - sFilePath: The file path of the script so it can be passed to the solver + when started. +-} +startMathSatScript' :: String -> SolverConfig -> FilePath -> IO Solver +startMathSatScript' logic conf scriptFilePath = do + scriptHandle <- openFile scriptFilePath WriteMode + let srcmd = newScriptArgs conf scriptHandle scriptFilePath + _ <- scriptSetOption srcmd (OptPrintSuccess True) + _ <- scriptSetLogic srcmd (N logic) + return $ scriptSolver srcmd + +--Function which creates the ScriptConf for the script functions. +newScriptArgs :: SolverConfig -> Handle -> FilePath -> ScriptConf +newScriptArgs solverConfig nHandle scriptFilePath = + ScriptConf { sHandle = nHandle + , sCmdPath = path solverConfig + , sArgs = args solverConfig + , sFilePath = scriptFilePath + } + + +-- Start MathSat batch mode + +startMathSatBatch :: String -> Maybe SolverConfig -> IO Solver +startMathSatBatch logic Nothing = startMathSatBatch' logic mathSatConfigBatch +startMathSatBatch logic (Just conf) = startMathSatBatch' logic conf + +startMathSatBatch' :: String -> SolverConfig -> IO Solver +startMathSatBatch' logic conf = return $ batchSolver logic conf + + + + + + +-- Creates the functions for online mode with the process already running. +-- Each function will send the command to the solver and wait for the response. +onlineSolver :: Process -> Solver +onlineSolver process = + Solver { setLogic = onlineSetLogic Mathsat process + , setOption = onlineSetOption Mathsat process + , setInfo = onlineSetInfo Mathsat process + , declareType = onlineDeclareType Mathsat process + , defineType = onlineDefineType Mathsat process + , declareFun = onlineDeclareFun Mathsat process + , defineFun = onlineDefineFun Mathsat process + , push = onlinePush Mathsat process + , pop = onlinePop Mathsat process + , assert = onlineAssert Mathsat process + , checkSat = onlineCheckSat Mathsat process + , getAssertions = onlineGetAssertions Mathsat process + , getValue = onlineGetValue Mathsat process + , getProof = onlineGetProof Mathsat process + , getUnsatCore = onlineGetUnsatCore Mathsat process + , getInfo = onlineGetInfo Mathsat process + , getOption = onlineGetOption Mathsat process + , exit = onlineExit process + } + +-- Creates the funtion for the script mode. +-- The configuration of the file is passed. +scriptSolver :: ScriptConf -> Solver +scriptSolver srcmd = + Solver { setLogic = scriptSetLogic srcmd + , setOption = scriptSetOption srcmd + , setInfo = scriptSetInfo srcmd + , declareType = scriptDeclareType srcmd + , defineType = scriptDefineType srcmd + , declareFun = scriptDeclareFun srcmd + , defineFun = scriptDefineFun srcmd + , push = scriptPush srcmd + , pop = scriptPop srcmd + , assert = scriptAssert srcmd + , checkSat = scriptCheckSat srcmd + , getAssertions = scriptGetAssertions srcmd + , getValue = scriptGetValue srcmd + , getProof = scriptGetProof srcmd + , getUnsatCore = scriptGetUnsatCore srcmd + , getInfo = scriptGetInfo srcmd + , getOption = scriptGetOption srcmd + , exit = scriptExit srcmd + } + + +batchSolver :: String -> SolverConfig -> Solver +batchSolver logic config = BSolver { Slv.executeBatch = B.executeBatch (path config) (args config) logic} diff --git a/Hsmtlib/Solvers/Yices.hs b/Hsmtlib/Solvers/Yices.hs --- a/Hsmtlib/Solvers/Yices.hs +++ b/Hsmtlib/Solvers/Yices.hs @@ -1,180 +1,180 @@ -{- | -Module : Hsmtlib.Solvers.Yices - Module wich has the standard configuration for all Yices Modes and - provides the initilizing function. --} -module Hsmtlib.Solvers.Yices(startYices) where - -import Hsmtlib.Solver as Slv -import Hsmtlib.Solvers.Cmd.BatchCmd as B (executeBatch) -import Hsmtlib.Solvers.Cmd.OnlineCmd -import Hsmtlib.Solvers.Cmd.ProcCom.Process -import Hsmtlib.Solvers.Cmd.ScriptCmd -import SMTLib2 -import System.IO (Handle, - IOMode (WriteMode), - openFile) - - -yicesConfigOnline :: SolverConfig -yicesConfigOnline = - Config { path = "yices-smt2" - , args = [ "--interactive"] - } - --- Script configurations is the same but has diferent names --- so if anything changes it's easy to alter its configuration. - -yicesConfigScript :: SolverConfig -yicesConfigScript = - Config { path = "yices-smt2" - , args = [] - } - -yicesConfigBatch :: SolverConfig -yicesConfigBatch = - Config { path = "yices-smt2" - , args = [] - } - -{- | - Function that initialyzes a Yices Solver. - It Receives a Mode, an SMT Logic, it can receive a diferent configuration - for the solver and an anternative path to create the script in Script Mode. - - In Online Mode if a FilePath is passed then it's ignored. --} -startYices :: Mode -> String -> Maybe SolverConfig -> Maybe FilePath -> IO Solver -startYices Slv.Batch logic sConf _ = startYicesBatch logic sConf -startYices Slv.Online logic sConf _ = startYicesOnline logic sConf -startYices Slv.Script logic sConf scriptFilePath = - startYicesScript logic sConf scriptFilePath - - - --- Start Yices Online. - -startYicesOnline :: String -> Maybe SolverConfig -> IO Solver -startYicesOnline logic Nothing = startYicesOnline' logic yicesConfigOnline -startYicesOnline logic (Just conf) = startYicesOnline' logic conf - -startYicesOnline':: String -> SolverConfig -> IO Solver -startYicesOnline' logic conf = do - -- Starts a Yices Process. - process <- beginProcess (path conf) (args conf) - --Set Option to print success after accepting a Command. - onlineSetOption process (OptPrintSuccess True) - -- Sets the SMT Logic. - onlineSetLogic process (N logic) - -- Initialize the solver Functions and return them. - return $ onlineSolver process - - ---Start Yices Script. - -startYicesScript :: String -> Maybe SolverConfig -> Maybe FilePath -> IO Solver -startYicesScript logic Nothing Nothing = - startYicesScript' logic yicesConfigScript "temp.smt2" -startYicesScript logic (Just conf) Nothing = - startYicesScript' logic conf "temp.smt2" -startYicesScript logic Nothing (Just scriptFilePath) = - startYicesScript' logic yicesConfigScript scriptFilePath -startYicesScript logic (Just conf) (Just scriptFilePath) = - startYicesScript' logic conf scriptFilePath - -{- - In this function a file is created where the commands are kept. - - Every function in the ScriptCmd Module needs a ScriptConf data which has: - - - sHandle: The handle of the script file - - sCmdPath: The Path to initilyze the solver - - sArgs: The options of the solver - - sFilePath: The file path of the script so it can be passed to the solver - when started. --} -startYicesScript' :: String -> SolverConfig -> FilePath -> IO Solver -startYicesScript' logic conf scriptFilePath = do - -- Create a file with the give file path. - -- Since the handle is created with WriteMode it overrides a file if it - -- already exists. - scriptHandle <- openFile scriptFilePath WriteMode - -- Creates the arguments for the functions in ScriptCmd - let srcmd = newScriptArgs conf scriptHandle scriptFilePath - --Set Option to print success after accepting a Command. - scriptSetOption srcmd (OptPrintSuccess True) - -- Initialize the solver Functions and return them. - scriptSetLogic srcmd (N logic) - return $ scriptSolver srcmd - ---Function which creates the ScriptConf for the script functions. -newScriptArgs :: SolverConfig -> Handle -> FilePath -> ScriptConf -newScriptArgs solverConfig nHandle scriptFilePath = - ScriptConf { sHandle = nHandle - , sCmdPath = path solverConfig - , sArgs = args solverConfig - , sFilePath = scriptFilePath - } - --- start Yices solver - -startYicesBatch :: String -> Maybe SolverConfig -> IO Solver -startYicesBatch logic Nothing = startYicesBatch' logic yicesConfigBatch -startYicesBatch logic (Just conf) = startYicesBatch' logic conf - -startYicesBatch' :: String -> SolverConfig -> IO Solver -startYicesBatch' logic conf = return $ batchSolver logic conf - - --- Creates the functions for online mode with the process already running. --- Each function will send the command to the solver and wait for the response. -onlineSolver :: Process -> Solver -onlineSolver process = - Solver { setLogic = onlineSetLogic process - , setOption = onlineSetOption process - , setInfo = onlineSetInfo process - , declareType = onlineDeclareType process - , defineType = onlineDefineType process - , declareFun = onlineDeclareFun process - , defineFun = onlineDefineFun process - , push = onlinePush process - , pop = onlinePop process - , assert = onlineAssert process - , checkSat = onlineCheckSat process - , getAssertions = onlineGetAssertions process - , getValue = onlineGetValue process - , getProof = onlineGetProof process - , getUnsatCore = onlineGetUnsatCore process - , getInfo = onlineGetInfo process - , getOption = onlineGetOption process - , exit = onlineExit process - } - - --- Creates the funtion for the script mode. --- The configuration of the file is passed. -scriptSolver :: ScriptConf -> Solver -scriptSolver srcmd = - Solver { setLogic = scriptSetLogic srcmd - , setOption = scriptSetOption srcmd - , setInfo = scriptSetInfo srcmd - , declareType = scriptDeclareType srcmd - , defineType = scriptDefineType srcmd - , declareFun = scriptDeclareFun srcmd - , defineFun = scriptDefineFun srcmd - , push = scriptPush srcmd - , pop = scriptPop srcmd - , assert = scriptAssert srcmd - , checkSat = scriptCheckSat srcmd - , getAssertions = scriptGetAssertions srcmd - , getValue = scriptGetValue srcmd - , getProof = scriptGetProof srcmd - , getUnsatCore = scriptGetUnsatCore srcmd - , getInfo = scriptGetInfo srcmd - , getOption = scriptGetOption srcmd - , exit = scriptExit srcmd - } - -batchSolver :: String -> SolverConfig -> Solver -batchSolver logic config = +{- | +Module : Hsmtlib.Solvers.Yices + Module wich has the standard configuration for all Yices Modes and + provides the initilizing function. +-} +module Hsmtlib.Solvers.Yices(startYices) where + +import Hsmtlib.Solver as Slv +import Hsmtlib.Solvers.Cmd.BatchCmd as B (executeBatch) +import Hsmtlib.Solvers.Cmd.OnlineCmd +import Hsmtlib.Solvers.Cmd.ProcCom.Process +import Hsmtlib.Solvers.Cmd.ScriptCmd +import SMTLib2 +import System.IO (Handle, + IOMode (WriteMode), + openFile) + + +yicesConfigOnline :: SolverConfig +yicesConfigOnline = + Config { path = "yices-smt2" + , args = [ "--interactive"] + } + +-- Script configurations is the same but has diferent names +-- so if anything changes it's easy to alter its configuration. + +yicesConfigScript :: SolverConfig +yicesConfigScript = + Config { path = "yices-smt2" + , args = [] + } + +yicesConfigBatch :: SolverConfig +yicesConfigBatch = + Config { path = "yices-smt2" + , args = [] + } + +{- | + Function that initialyzes a Yices Solver. + It Receives a Mode, an SMT Logic, it can receive a diferent configuration + for the solver and an anternative path to create the script in Script Mode. + + In Online Mode if a FilePath is passed then it's ignored. +-} +startYices :: Mode -> String -> Maybe SolverConfig -> Maybe FilePath -> IO Solver +startYices Slv.Batch logic sConf _ = startYicesBatch logic sConf +startYices Slv.Online logic sConf _ = startYicesOnline logic sConf +startYices Slv.Script logic sConf scriptFilePath = + startYicesScript logic sConf scriptFilePath + + + +-- Start Yices Online. + +startYicesOnline :: String -> Maybe SolverConfig -> IO Solver +startYicesOnline logic Nothing = startYicesOnline' logic yicesConfigOnline +startYicesOnline logic (Just conf) = startYicesOnline' logic conf + +startYicesOnline':: String -> SolverConfig -> IO Solver +startYicesOnline' logic conf = do + -- Starts a Yices Process. + process <- beginProcess (path conf) (args conf) + --Set Option to print success after accepting a Command. + _ <- onlineSetOption Yices process (OptPrintSuccess True) + -- Sets the SMT Logic. + _ <-onlineSetLogic Yices process (N logic) + -- Initialize the solver Functions and return them. + return $ onlineSolver process + + +--Start Yices Script. + +startYicesScript :: String -> Maybe SolverConfig -> Maybe FilePath -> IO Solver +startYicesScript logic Nothing Nothing = + startYicesScript' logic yicesConfigScript "temp.smt2" +startYicesScript logic (Just conf) Nothing = + startYicesScript' logic conf "temp.smt2" +startYicesScript logic Nothing (Just scriptFilePath) = + startYicesScript' logic yicesConfigScript scriptFilePath +startYicesScript logic (Just conf) (Just scriptFilePath) = + startYicesScript' logic conf scriptFilePath + +{- + In this function a file is created where the commands are kept. + + Every function in the ScriptCmd Module needs a ScriptConf data which has: + + - sHandle: The handle of the script file + - sCmdPath: The Path to initilyze the solver + - sArgs: The options of the solver + - sFilePath: The file path of the script so it can be passed to the solver + when started. +-} +startYicesScript' :: String -> SolverConfig -> FilePath -> IO Solver +startYicesScript' logic conf scriptFilePath = do + -- Create a file with the give file path. + -- Since the handle is created with WriteMode it overrides a file if it + -- already exists. + scriptHandle <- openFile scriptFilePath WriteMode + -- Creates the arguments for the functions in ScriptCmd + let srcmd = newScriptArgs conf scriptHandle scriptFilePath + --Set Option to print success after accepting a Command. + _ <- scriptSetOption srcmd (OptPrintSuccess True) + -- Initialize the solver Functions and return them. + _ <-scriptSetLogic srcmd (N logic) + return $ scriptSolver srcmd + +--Function which creates the ScriptConf for the script functions. +newScriptArgs :: SolverConfig -> Handle -> FilePath -> ScriptConf +newScriptArgs solverConfig nHandle scriptFilePath = + ScriptConf { sHandle = nHandle + , sCmdPath = path solverConfig + , sArgs = args solverConfig + , sFilePath = scriptFilePath + } + +-- start Yices solver + +startYicesBatch :: String -> Maybe SolverConfig -> IO Solver +startYicesBatch logic Nothing = startYicesBatch' logic yicesConfigBatch +startYicesBatch logic (Just conf) = startYicesBatch' logic conf + +startYicesBatch' :: String -> SolverConfig -> IO Solver +startYicesBatch' logic conf = return $ batchSolver logic conf + + +-- Creates the functions for online mode with the process already running. +-- Each function will send the command to the solver and wait for the response. +onlineSolver :: Process -> Solver +onlineSolver process = + Solver { setLogic = onlineSetLogic Yices process + , setOption = onlineSetOption Yices process + , setInfo = onlineSetInfo Yices process + , declareType = onlineDeclareType Yices process + , defineType = onlineDefineType Yices process + , declareFun = onlineDeclareFun Yices process + , defineFun = onlineDefineFun Yices process + , push = onlinePush Yices process + , pop = onlinePop Yices process + , assert = onlineAssert Yices process + , checkSat = onlineCheckSat Yices process + , getAssertions = onlineGetAssertions Yices process + , getValue = onlineGetValue Yices process + , getProof = onlineGetProof Yices process + , getUnsatCore = onlineGetUnsatCore Yices process + , getInfo = onlineGetInfo Yices process + , getOption = onlineGetOption Yices process + , exit = onlineExit process + } + + +-- Creates the funtion for the script mode. +-- The configuration of the file is passed. +scriptSolver :: ScriptConf -> Solver +scriptSolver srcmd = + Solver { setLogic = scriptSetLogic srcmd + , setOption = scriptSetOption srcmd + , setInfo = scriptSetInfo srcmd + , declareType = scriptDeclareType srcmd + , defineType = scriptDefineType srcmd + , declareFun = scriptDeclareFun srcmd + , defineFun = scriptDefineFun srcmd + , push = scriptPush srcmd + , pop = scriptPop srcmd + , assert = scriptAssert srcmd + , checkSat = scriptCheckSat srcmd + , getAssertions = scriptGetAssertions srcmd + , getValue = scriptGetValue srcmd + , getProof = scriptGetProof srcmd + , getUnsatCore = scriptGetUnsatCore srcmd + , getInfo = scriptGetInfo srcmd + , getOption = scriptGetOption srcmd + , exit = scriptExit srcmd + } + +batchSolver :: String -> SolverConfig -> Solver +batchSolver logic config = BSolver { Slv.executeBatch = B.executeBatch (path config) (args config) logic} diff --git a/Hsmtlib/Solvers/Z3.hs b/Hsmtlib/Solvers/Z3.hs --- a/Hsmtlib/Solvers/Z3.hs +++ b/Hsmtlib/Solvers/Z3.hs @@ -1,172 +1,187 @@ -{- | -Module : Hsmtlib.Solvers.Z3 - Module wich has the standard configuration for all Z3 Modes and - provides the initilizing function. --} -module Hsmtlib.Solvers.Z3(startZ3) where - -import Hsmtlib.Solver as Slv -import Hsmtlib.Solvers.Cmd.BatchCmd as B (executeBatch) -import Hsmtlib.Solvers.Cmd.OnlineCmd -import Hsmtlib.Solvers.Cmd.ProcCom.Process -import Hsmtlib.Solvers.Cmd.ScriptCmd -import SMTLib2 -import System.IO (Handle, - IOMode (WriteMode), - openFile) - --- All the configurations are the same but have diferent names so if anything --- changes it's easy to alter its configuration. - -z3ConfigOnline :: SolverConfig -z3ConfigOnline = - Config { path = "z3" - , args = ["-smt2","-in"] - } - -z3ConfigScript :: SolverConfig -z3ConfigScript = - Config { path = "z3" - , args = ["-smt2"] - } - -z3ConfigBatch :: SolverConfig -z3ConfigBatch = - Config { path = "z3" - , args = ["-smt2"] - } - -{- | - Function that initialyzes a Z3 Solver. - It Receives a Mode, an SMT Logic, it can receive a diferent configuration - for the solver and an anternative path to create the script in Script Mode. - - In Online Mode if a FilePath is passed then it's ignored. --} -startZ3 :: Mode -> String -> Maybe SolverConfig -> Maybe FilePath -> IO Solver -startZ3 Slv.Batch logic sConf _ = startZ3Batch logic sConf -startZ3 Slv.Online logic sConf _ = startZ3Online logic sConf -startZ3 Slv.Script logic sConf scriptFilePath = - startZ3Script logic sConf scriptFilePath - --- Start Z3 Online. - -startZ3Online :: String -> Maybe SolverConfig -> IO Solver -startZ3Online logic Nothing = startZ3Online' logic z3ConfigOnline -startZ3Online logic (Just conf) = startZ3Online' logic conf - -startZ3Online' :: String -> SolverConfig -> IO Solver -startZ3Online' logic conf = do - -- Starts a Z4 Process. - process <- beginProcess (path conf) (args conf) - --Set Option to print success after accepting a Command. - onlineSetOption process (OptPrintSuccess True) - -- Sets the SMT Logic. - onlineSetLogic process (N logic) - -- Initialize the solver Functions and return them. - return $ onlineSolver process - ---Start Z3 Script. - -startZ3Script :: String -> Maybe SolverConfig -> Maybe FilePath -> IO Solver -startZ3Script logic Nothing Nothing = - startZ3Script' logic z3ConfigScript "temp.smt2" -startZ3Script logic (Just conf) Nothing = - startZ3Script' logic conf "temp.smt2" -startZ3Script logic Nothing (Just scriptFilePath) = - startZ3Script' logic z3ConfigScript scriptFilePath -startZ3Script logic (Just conf) (Just scriptFilePath) = - startZ3Script' logic conf scriptFilePath - -{- - In this function a file is created where the commands are kept. - - Every function in the ScriptCmd Module needs a ScriptConf data which has: - - - sHandle: The handle of the script file - - sCmdPath: The Path to initilyze the solver - - sArgs: The options of the solver - - sFilePath: The file path of the script so it can be passed to the solver - when started. --} -startZ3Script' :: String -> SolverConfig -> FilePath -> IO Solver -startZ3Script' logic conf scriptFilePath = do - scriptHandle <- openFile scriptFilePath WriteMode - let srcmd = newScriptArgs conf scriptHandle scriptFilePath - scriptSetOption srcmd (OptPrintSuccess True) - scriptSetLogic srcmd (N logic) - return $ scriptSolver srcmd - ---Function which creates the ScriptConf for the script functions. -newScriptArgs :: SolverConfig -> Handle -> FilePath -> ScriptConf -newScriptArgs solverConfig nHandle scriptFilePath = - ScriptConf { sHandle = nHandle - , sCmdPath = path solverConfig - , sArgs = args solverConfig - , sFilePath = scriptFilePath - } - - --- Start z3 batch mode - -startZ3Batch :: String -> Maybe SolverConfig -> IO Solver -startZ3Batch logic Nothing = startZ3Batch' logic z3ConfigBatch -startZ3Batch logic (Just conf) = startZ3Batch' logic conf - -startZ3Batch' :: String -> SolverConfig -> IO Solver -startZ3Batch' logic conf = return $ batchSolver logic conf - - - - --- Creates the functions for online mode with the process already running. --- Each function will send the command to the solver and wait for the response. -onlineSolver :: Process -> Solver -onlineSolver process = - Solver { setLogic = onlineSetLogic process - , setOption = onlineSetOption process - , setInfo = onlineSetInfo process - , declareType = onlineDeclareType process - , defineType = onlineDefineType process - , declareFun = onlineDeclareFun process - , defineFun = onlineDefineFun process - , push = onlinePush process - , pop = onlinePop process - , assert = onlineAssert process - , checkSat = onlineCheckSat process - , getAssertions = onlineGetAssertions process - , getValue = onlineGetValue process - , getProof = onlineGetProof process - , getUnsatCore = onlineGetUnsatCore process - , getInfo = onlineGetInfo process - , getOption = onlineGetOption process - , exit = onlineExit process - } - --- Creates the funtion for the script mode. --- The configuration of the file is passed. -scriptSolver :: ScriptConf -> Solver -scriptSolver srcmd = - Solver { setLogic = scriptSetLogic srcmd - , setOption = scriptSetOption srcmd - , setInfo = scriptSetInfo srcmd - , declareType = scriptDeclareType srcmd - , defineType = scriptDefineType srcmd - , declareFun = scriptDeclareFun srcmd - , defineFun = scriptDefineFun srcmd - , push = scriptPush srcmd - , pop = scriptPop srcmd - , assert = scriptAssert srcmd - , checkSat = scriptCheckSat srcmd - , getAssertions = scriptGetAssertions srcmd - , getValue = scriptGetValue srcmd - , getProof = scriptGetProof srcmd - , getUnsatCore = scriptGetUnsatCore srcmd - , getInfo = scriptGetInfo srcmd - , getOption = scriptGetOption srcmd - , exit = scriptExit srcmd - } - -batchSolver :: String -> SolverConfig -> Solver -batchSolver logic config = - BSolver { Slv.executeBatch = B.executeBatch (path config) (args config) logic} +{- | +Module : Hsmtlib.Solvers.Z3 + Module wich has the standard configuration for all Z3 Modes and + provides the initilizing function. +-} +module Hsmtlib.Solvers.Z3(startZ3) where + +import Control.Applicative (liftA) +import Hsmtlib.Solver as Slv +import Hsmtlib.Solvers.Cmd.BatchCmd as B (executeBatch) +import Hsmtlib.Solvers.Cmd.OnlineCmd +import Hsmtlib.Solvers.Cmd.ProcCom.Process +import Hsmtlib.Solvers.Cmd.ScriptCmd +import Hsmtlib.Solvers.Cmd.CmdResult +import SMTLib2 +import System.IO (Handle, + IOMode (WriteMode), + openFile) + +-- All the configurations are the same but have diferent names so if anything +-- changes it's easy to alter its configuration. + +z3ConfigOnline :: SolverConfig +z3ConfigOnline = + Config { path = "z3" + , args = ["-smt2","-in"] + } + +z3ConfigScript :: SolverConfig +z3ConfigScript = + Config { path = "z3" + , args = ["-smt2"] + } + +z3ConfigBatch :: SolverConfig +z3ConfigBatch = + Config { path = "z3" + , args = ["-smt2"] + } + +{- | + Function that initialyzes a Z3 Solver. + It Receives a Mode, an SMT Logic, it can receive a diferent configuration + for the solver and an anternative path to create the script in Script Mode. + + In Online Mode if a FilePath is passed then it's ignored. +-} +startZ3 :: Mode -> String -> Maybe SolverConfig -> Maybe FilePath -> IO Solver +startZ3 Slv.Batch logic sConf _ = startZ3Batch logic sConf +startZ3 Slv.Online logic sConf _ = startZ3Online logic sConf +startZ3 Slv.Script logic sConf scriptFilePath = + startZ3Script logic sConf scriptFilePath + +-- Start Z3 Online. + +startZ3Online :: String -> Maybe SolverConfig -> IO Solver +startZ3Online logic Nothing = startZ3Online' logic z3ConfigOnline +startZ3Online logic (Just conf) = startZ3Online' logic conf + +startZ3Online' :: String -> SolverConfig -> IO Solver +startZ3Online' logic conf = do + -- Starts a Z3 Process. + process <- beginProcess (path conf) (args conf) + --Set Option to print success after accepting a Command. + onlineSetOption Z3 process (OptPrintSuccess True) + -- Sets the SMT Logic. + onlineSetLogic Z3 process (N logic) + -- Initialize the solver Functions and return them. + return $ onlineSolver process + +--Start Z3 Script. + +startZ3Script :: String -> Maybe SolverConfig -> Maybe FilePath -> IO Solver +startZ3Script logic Nothing Nothing = + startZ3Script' logic z3ConfigScript "temp.smt2" +startZ3Script logic (Just conf) Nothing = + startZ3Script' logic conf "temp.smt2" +startZ3Script logic Nothing (Just scriptFilePath) = + startZ3Script' logic z3ConfigScript scriptFilePath +startZ3Script logic (Just conf) (Just scriptFilePath) = + startZ3Script' logic conf scriptFilePath + +{- + In this function a file is created where the commands are kept. + + Every function in the ScriptCmd Module needs a ScriptConf data which has: + + - sHandle: The handle of the script file + - sCmdPath: The Path to initilyze the solver + - sArgs: The options of the solver + - sFilePath: The file path of the script so it can be passed to the solver + when started. +-} +startZ3Script' :: String -> SolverConfig -> FilePath -> IO Solver +startZ3Script' logic conf scriptFilePath = do + scriptHandle <- openFile scriptFilePath WriteMode + let srcmd = newScriptArgs conf scriptHandle scriptFilePath + scriptSetOption srcmd (OptPrintSuccess True) + scriptSetLogic srcmd (N logic) + return $ scriptSolver srcmd + +--Function which creates the ScriptConf for the script functions. +newScriptArgs :: SolverConfig -> Handle -> FilePath -> ScriptConf +newScriptArgs solverConfig nHandle scriptFilePath = + ScriptConf { sHandle = nHandle + , sCmdPath = path solverConfig + , sArgs = args solverConfig + , sFilePath = scriptFilePath + } + + +-- Start z3 batch mode + +startZ3Batch :: String -> Maybe SolverConfig -> IO Solver +startZ3Batch logic Nothing = startZ3Batch' logic z3ConfigBatch +startZ3Batch logic (Just conf) = startZ3Batch' logic conf + +startZ3Batch' :: String -> SolverConfig -> IO Solver +startZ3Batch' logic conf = return $ batchSolver logic conf + + + + +-- Creates the functions for online mode with the process already running. +-- Each function will send the command to the solver and wait for the response. +onlineSolver :: Process -> Solver +onlineSolver process = + Solver { setLogic = onlineSetLogic Z3 process + , setOption = onlineSetOption Z3 process + , setInfo = onlineSetInfo Z3 process + , declareType = onlineDeclareType Z3 process + , defineType = onlineDefineType Z3 process + , declareFun = onlineDeclareFun Z3 process + , defineFun = onlineDefineFun Z3 process + , push = onlinePush Z3 process + , pop = onlinePop Z3 process + , assert = onlineAssert Z3 process + , checkSat = onlineCheckSat Z3 process + , getAssertions = onlineGetAssertions Z3 process + , getValue = onlineGetValue Z3 process + , getProof = onlineGetProof Z3 process + , getUnsatCore = onlineGetUnsatCore Z3 process + , getInfo = onlineGetInfo Z3 process + , getOption = onlineGetOption Z3 process + , exit = onlineExit process + } +{-Specific parse result functions that works only in case of Z3 because it breaks the result with new line and not space-} +scriptGetValueResponseZ3 :: ScriptConf -> Command -> IO Result +scriptGetValueResponseZ3 conf cmd = + liftA getValueResponse (scriptFunExecZ3 conf cmd) + +scriptFunExecZ3 :: ScriptConf -> Command -> IO String +scriptFunExecZ3 sConf cmd = do + writeToScript sConf cmd + res <- sendScript (sCmdPath sConf) (sArgs sConf) (sFilePath sConf) + return $ unlines $ drop 1 $ snd $ break (==['s','a','t']) $ lines $ res + +scriptGetValueZ3 :: ScriptConf -> [Expr] -> IO Result +scriptGetValueZ3 sConf exprs = scriptGetValueResponseZ3 sConf (CmdGetValue exprs) + +-- Creates the funtion for the script mode. +-- The configuration of the file is passed. +scriptSolver :: ScriptConf -> Solver +scriptSolver srcmd = + Solver { setLogic = scriptSetLogic srcmd + , setOption = scriptSetOption srcmd + , setInfo = scriptSetInfo srcmd + , declareType = scriptDeclareType srcmd + , defineType = scriptDefineType srcmd + , declareFun = scriptDeclareFun srcmd + , defineFun = scriptDefineFun srcmd + , push = scriptPush srcmd + , pop = scriptPop srcmd + , assert = scriptAssert srcmd + , checkSat = scriptCheckSat srcmd + , getAssertions = scriptGetAssertions srcmd + , getValue = scriptGetValueZ3 srcmd + , getProof = scriptGetProof srcmd + , getUnsatCore = scriptGetUnsatCore srcmd + , getInfo = scriptGetInfo srcmd + , getOption = scriptGetOption srcmd + , exit = scriptExit srcmd + } + +batchSolver :: String -> SolverConfig -> Solver +batchSolver logic config = + BSolver { Slv.executeBatch = B.executeBatch (path config) (args config) logic} diff --git a/LICENSE b/LICENSE --- a/LICENSE +++ b/LICENSE @@ -1,20 +1,20 @@ -Copyright (c) 2014 Nuno Laranjo and Rogério Pontes. - -Permission is hereby granted, free of charge, to any person obtaining -a copy of this software and associated documentation files (the -"Software"), to deal in the Software without restriction, including -without limitation the rights to use, copy, modify, merge, publish, -distribute, sublicense, and/or sell copies of the Software, and to -permit persons to whom the Software is furnished to do so, subject to -the following conditions: - -The above copyright notice and this permission notice shall be -included in all copies or substantial portions of the Software. - -THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, -EXPRESS OR IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF -MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND -NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS BE -LIABLE FOR ANY CLAIM, DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION -OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT OF OR IN CONNECTION -WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE. +Copyright (c) 2014 Nuno Laranjo and Rogerio Pontes + +Permission is hereby granted, free of charge, to any person obtaining +a copy of this software and associated documentation files (the +"Software"), to deal in the Software without restriction, including +without limitation the rights to use, copy, modify, merge, publish, +distribute, sublicense, and/or sell copies of the Software, and to +permit persons to whom the Software is furnished to do so, subject to +the following conditions: + +The above copyright notice and this permission notice shall be included +in all copies or substantial portions of the Software. + +THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, +EXPRESS OR IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF +MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. +IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY +CLAIM, DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION OF CONTRACT, +TORT OR OTHERWISE, ARISING FROM, OUT OF OR IN CONNECTION WITH THE +SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE. diff --git a/Setup.hs b/Setup.hs --- a/Setup.hs +++ b/Setup.hs @@ -1,2 +1,2 @@ -import Distribution.Simple -main = defaultMain +import Distribution.Simple +main = defaultMain