Hsmtlib 0.2.0.6 → 2.8.8.8
raw patch · 27 files changed
+4312/−3120 lines, 27 filesdep ~basedep ~processdep ~transformerssetup-changed
Dependency ranges changed: base, process, transformers
Files
- Hsmtlib.cabal +37/−76
- Hsmtlib.hs +61/−58
- Hsmtlib/HighLevel.hs +125/−112
- Hsmtlib/Parsers/AuxParser.hs +116/−0
- Hsmtlib/Parsers/ParseResponse.hs +321/−0
- Hsmtlib/Parsers/ParseScript.hs +840/−0
- Hsmtlib/Parsers/Syntax.hs +235/−0
- Hsmtlib/Parsers/Visualizer.hs +180/−0
- Hsmtlib/Solver.hs +137/−129
- Hsmtlib/Solvers/Altergo.hs +223/−178
- Hsmtlib/Solvers/Boolector.hs +176/−176
- Hsmtlib/Solvers/Cmd/BatchCmd.hs +19/−19
- Hsmtlib/Solvers/Cmd/CmdResult.hs +237/−0
- Hsmtlib/Solvers/Cmd/OnlineCmd.hs +142/−88
- Hsmtlib/Solvers/Cmd/Parser/CmdResult.hs +0/−388
- Hsmtlib/Solvers/Cmd/Parser/Parsers.hs +0/−538
- Hsmtlib/Solvers/Cmd/Parser/Syntax.hs +0/−153
- Hsmtlib/Solvers/Cmd/Parser/Visualizers.hs +0/−180
- Hsmtlib/Solvers/Cmd/ProcCom/Process.hs +246/−156
- Hsmtlib/Solvers/Cmd/ResultHelpers.hs +295/−0
- Hsmtlib/Solvers/Cmd/ScriptCmd.hs +167/−129
- Hsmtlib/Solvers/Cvc4.hs +185/−185
- Hsmtlib/Solvers/MathSAT.hs +182/−182
- Hsmtlib/Solvers/Yices.hs +179/−179
- Hsmtlib/Solvers/Z3.hs +187/−172
- LICENSE +20/−20
- Setup.hs +2/−2
Hsmtlib.cabal view
@@ -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 <https://github.com/MfesGA/Hsmtlib> - --- 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 <https://github.com/MfesGA/Hsmtlib>+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
Hsmtlib.hs view
@@ -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
Hsmtlib/HighLevel.hs view
@@ -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) +
+ Hsmtlib/Parsers/AuxParser.hs view
@@ -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"
+ Hsmtlib/Parsers/ParseResponse.hs view
@@ -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 #+ # #+ #########################################################################+-}+
+ Hsmtlib/Parsers/ParseScript.hs view
@@ -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+++++++++++++++++++++++++++++++++
+ Hsmtlib/Parsers/Syntax.hs view
@@ -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+
+ Hsmtlib/Parsers/Visualizer.hs view
@@ -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
Hsmtlib/Solver.hs view
@@ -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 }
Hsmtlib/Solvers/Altergo.hs view
@@ -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}
Hsmtlib/Solvers/Boolector.hs view
@@ -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}
Hsmtlib/Solvers/Cmd/BatchCmd.hs view
@@ -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
+ Hsmtlib/Solvers/Cmd/CmdResult.hs view
@@ -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
Hsmtlib/Solvers/Cmd/OnlineCmd.hs view
@@ -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
− Hsmtlib/Solvers/Cmd/Parser/CmdResult.hs
@@ -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
− Hsmtlib/Solvers/Cmd/Parser/Parsers.hs
@@ -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
− Hsmtlib/Solvers/Cmd/Parser/Syntax.hs
@@ -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)
− Hsmtlib/Solvers/Cmd/Parser/Visualizers.hs
@@ -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
Hsmtlib/Solvers/Cmd/ProcCom/Process.hs view
@@ -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. -<http://hackage.haskell.org/package/process-1.1.0.1/docs/System-Process.html> - -} -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: -<http://hackage.haskell.org/package/process-1.1.0.1/docs/System-Process.html> --} -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.+<http://hackage.haskell.org/package/process-1.1.0.1/docs/System-Process.html>+ -}+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:+<http://hackage.haskell.org/package/process-1.1.0.1/docs/System-Process.html>+-}++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
+ Hsmtlib/Solvers/Cmd/ResultHelpers.hs view
@@ -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
Hsmtlib/Solvers/Cmd/ScriptCmd.hs view
@@ -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)
Hsmtlib/Solvers/Cvc4.hs view
@@ -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}
Hsmtlib/Solvers/MathSAT.hs view
@@ -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}
Hsmtlib/Solvers/Yices.hs view
@@ -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}
Hsmtlib/Solvers/Z3.hs view
@@ -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}
LICENSE view
@@ -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.
Setup.hs view
@@ -1,2 +1,2 @@-import Distribution.Simple -main = defaultMain +import Distribution.Simple+main = defaultMain