diff --git a/Hsmtlib.cabal b/Hsmtlib.cabal new file mode 100644 --- /dev/null +++ b/Hsmtlib.cabal @@ -0,0 +1,76 @@ +-- Initial Hsmtlib.cabal generated by cabal init. For further +-- documentation, see http://haskell.org/cabal/users-guide/ + +-- The name of the package. +name: Hsmtlib + +-- The package version. See the Haskell package versioning policy (PVP) +-- for standards guiding when and how versions should be incremented. +-- http://www.haskell.org/haskellwiki/Package_versioning_policy +-- PVP summary: +-+------- breaking API changes +-- | | +----- non-breaking API additions +-- | | | +--- code changes with no API change +version: 0.2.0.6 + +-- A short (one-line) description of the package. +synopsis: Haskell library for easy interaction with SMT-LIB 2 compliant solvers. + +-- A longer description of the package. +description: + Hsmtl provides functions to interact with several smt solvers using SMT-LIB 2. + + The current suported solvers are Alt-Ergo, Cvc4, MathSat, Yices, Z3. + Additional solvers can be used if they are SMT-LIB 2 compliant. + + More information and tutorials can be found in + +-- URL for the project homepage or repository. +homepage: https://github.com/MfesGA/Hsmtlib + +-- The license under which the package is released. +license: BSD3 + +-- The file containing the license text. +license-file: LICENSE + +-- The package author(s). +author: Nuno Laranjo and Rogerio Pontes + +-- An email address to which users can send suggestions, bug reports, and +-- patches. +maintainer: numicola@gmail.com and rogeriop062@gmail.com + +-- A copyright notice. +-- copyright: + +category: SMT + +build-type: Simple + +-- Extra files to be distributed with the package, such as examples or a +-- README. +-- extra-source-files: + +-- Constraint on the version of Cabal needed to build this package. +cabal-version: >=1.10 + + +library + -- Modules exported by the library. + exposed-modules: Hsmtlib, Hsmtlib.Solver, Hsmtlib.HighLevel, Hsmtlib.Solvers.Z3, Hsmtlib.Solvers.Yices, Hsmtlib.Solvers.MathSAT, Hsmtlib.Solvers.Cvc4, Hsmtlib.Solvers.Boolector, Hsmtlib.Solvers.Altergo, Hsmtlib.Solvers.Cmd.ScriptCmd, Hsmtlib.Solvers.Cmd.OnlineCmd, Hsmtlib.Solvers.Cmd.BatchCmd, Hsmtlib.Solvers.Cmd.ProcCom.Process, Hsmtlib.Solvers.Cmd.Parser.Visualizers, Hsmtlib.Solvers.Cmd.Parser.Syntax, Hsmtlib.Solvers.Cmd.Parser.Parsers, Hsmtlib.Solvers.Cmd.Parser.CmdResult + + -- Modules included in this library but not exported. + -- other-modules: + + -- LANGUAGE extensions used by modules in this package. + -- other-extensions: + + -- Other library packages from which modules are imported. + build-depends: base >=4.6 && <= 4.7, smtLib >=1.0 && <1.1, containers >=0.5 && <0.6, pretty >=1.1 && <1.2, process >=1.1 && <= 1.2 , transformers >=0.3 && <0.4, parsec >=3.1 && <3.2 + + -- Directories containing source files. + -- hs-source-dirs: + + -- Base language which the package is written in. + default-language: Haskell2010 + diff --git a/Hsmtlib.hs b/Hsmtlib.hs new file mode 100644 --- /dev/null +++ b/Hsmtlib.hs @@ -0,0 +1,58 @@ +{- | + 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 + + + diff --git a/Hsmtlib/HighLevel.hs b/Hsmtlib/HighLevel.hs new file mode 100644 --- /dev/null +++ b/Hsmtlib/HighLevel.hs @@ -0,0 +1,112 @@ +{- | + 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) diff --git a/Hsmtlib/Solver.hs b/Hsmtlib/Solver.hs new file mode 100644 --- /dev/null +++ b/Hsmtlib/Solver.hs @@ -0,0 +1,130 @@ +{- | +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 + { executeBatch :: [Command] -> IO String } diff --git a/Hsmtlib/Solvers/Altergo.hs b/Hsmtlib/Solvers/Altergo.hs new file mode 100644 --- /dev/null +++ b/Hsmtlib/Solvers/Altergo.hs @@ -0,0 +1,178 @@ +{- | +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} diff --git a/Hsmtlib/Solvers/Boolector.hs b/Hsmtlib/Solvers/Boolector.hs new file mode 100644 --- /dev/null +++ b/Hsmtlib/Solvers/Boolector.hs @@ -0,0 +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} diff --git a/Hsmtlib/Solvers/Cmd/BatchCmd.hs b/Hsmtlib/Solvers/Cmd/BatchCmd.hs new file mode 100644 --- /dev/null +++ b/Hsmtlib/Solvers/Cmd/BatchCmd.hs @@ -0,0 +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 diff --git a/Hsmtlib/Solvers/Cmd/OnlineCmd.hs b/Hsmtlib/Solvers/Cmd/OnlineCmd.hs new file mode 100644 --- /dev/null +++ b/Hsmtlib/Solvers/Cmd/OnlineCmd.hs @@ -0,0 +1,88 @@ +{- | +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 diff --git a/Hsmtlib/Solvers/Cmd/Parser/CmdResult.hs b/Hsmtlib/Solvers/Cmd/Parser/CmdResult.hs new file mode 100644 --- /dev/null +++ b/Hsmtlib/Solvers/Cmd/Parser/CmdResult.hs @@ -0,0 +1,388 @@ +module Hsmtlib.Solvers.Cmd.Parser.CmdResult where + +import Control.Applicative ((<|>),(<$>)) +import Control.Monad +import Data.List (intercalate) +import Data.Map as M +import Data.Maybe (isJust) +import Hsmtlib.Solver as Solv +import Hsmtlib.Solvers.Cmd.Parser.Parsers hiding (numeral, symbol) +import Hsmtlib.Solvers.Cmd.Parser.Syntax as S +import Hsmtlib.Solvers.Cmd.Parser.Visualizers +import Prelude as P +import Text.ParserCombinators.Parsec.Prim (parse) + +genResponse :: String -> GenResult +genResponse stg = + case result of + Left err -> Solv.GUError $ show err + Right cmdRep -> case cmdRep of + CmdGenResponse S.Success -> Solv.Success + CmdGenResponse S.Unsupported -> Solv.Unsupported + CmdGenResponse (S.Error err) -> Solv.Error err + where result = parse parseCmdGenResponse "" stg + + +checkSatResponse :: String -> SatResult +checkSatResponse stg = + case result of + Left err -> Solv.SUError $ show err + Right cmdRep -> case cmdRep of + S.Sat -> Solv.Sat + S.Unsat -> Solv.Unsat + S.Unknown -> Solv.Unknown + where result = parse parseCheckSatResponse "" stg + + +{- +getValueResponse :: String -> GValResult +getValueResponse stg = GVUError $ stg ++ "\n" ++ tree + where result = parse parseGetValueResponse "" stg + tree = getVR' result + + +getVR' :: Show a => Either a [ValuationPair] -> String +getVR' result = + case result of + Left err -> show err + Right vals -> intercalate "\n" (fmap (showValuationPair 0) vals) + +-} +getValueResponse :: String -> GValResult +getValueResponse stg = case result of + Left err -> GVUError $ stg ++ "|"++show err + Right vals -> getVR' $ getValResponse vals + where result = parse parseGetValueResponse "" stg + + +getVR' :: [GValResult] -> GValResult +getVR' xs | length xs == 1 = head xs + | otherwise = Results xs + +getValResponse::[ValuationPair] -> [GValResult] +getValResponse vp = arrays ++ errors + -- gets the results in a Maybe GValResult. + where res = getValResponses vp + --Produes UErrors from the results that gave Nothing. + errors = valErrors' vp res + cRes = P.filter isJust res -- Removes the Nothings. + -- Joins all arrays in one and + --removes the Just from all results. + arrays = joinArrays cRes + + + +valErrors' :: [ValuationPair] -> [Maybe GValResult] -> [GValResult] +valErrors' [] [] = [] +valErrors' (x:xs) (Nothing:gs) = + GVUError (showValuationPair 0 x) : valErrors' xs gs +valErrors' (_:xs) (_:gs) = valErrors' xs gs + + + +joinArrays :: [Maybe GValResult] -> [GValResult] +joinArrays = joinArrays' $ VArrays empty + + +joinArrays' :: GValResult -> [Maybe GValResult] -> [GValResult] +-- if there was no array in the result then don't put an empty one. +joinArrays' (VArrays n) [] | M.null n = [] + | otherwise = [VArrays n] +joinArrays' res (x:xs) = case nVal of + (VArrays _) -> joinArrays' nVal xs + _ -> nVal : joinArrays' res xs + where nVal = checkGVal res x + +checkGVal :: GValResult -> Maybe GValResult -> GValResult +checkGVal (VArrays oarr) (Just(VArrays arr)) = + VArrays $ unionWith union oarr arr +checkGVal _ (Just x) = x + + +getValResponses :: [ValuationPair] -> [Maybe GValResult] +getValResponses = fmap getGValResult + +getGValResult :: ValuationPair -> Maybe GValResult +getGValResult vp = getVar vp + <|> getArray vp + <|> getFun vp + <|> getBitVec vp + +{- | Retrives the value of a BitVector. + Works with: + - Z3. +-} +getBitVec :: ValuationPair -> Maybe GValResult +getBitVec vp = getBitVec' name vhex + where name = getVarName vp + vhex = getHexVal vp + + +-- auxiliar function to getBitVec +getBitVec' :: Maybe String -> Maybe String -> Maybe GValResult +getBitVec' (Just name) (Just vhex) = Just $ Res name $ VHex vhex +getBitVec' _ _ = Nothing + +{- | Retrives the value of a function. + Works with: + - Z3. +-} +getFun :: ValuationPair -> Maybe GValResult +getFun vp = getFun' name value + where name = getFunName vp + value = getFunResult vp + +-- auxiliar function to getFun +getFun' :: Maybe String -> Maybe Value -> Maybe GValResult +getFun' (Just name) (Just res) = Just $ Res name res +getFun' _ _ = Nothing + + +{- | Retrives the value of a variable. + Works with: + - Z3. +-} +getVar :: ValuationPair -> Maybe GValResult +getVar vp = getVar' name value + where name = getVarName vp + value = getVarValue vp + +-- auxiliar function to getVar +getVar' :: Maybe String -> Maybe Integer -> Maybe GValResult +getVar' Nothing _ = Nothing +getVar' _ Nothing = Nothing +getVar' (Just name) (Just value) = Just $ Res name $ VInt value + + + + +{- | Retrives the value of an array. + Works with: + - Z3. +-} +getArray :: ValuationPair -> Maybe GValResult +getArray vp = + case isArr of + Nothing -> Nothing + Just _ -> case res of + Just arr -> Just $ VArrays arr + Nothing -> Nothing + + where name = arrayName vp + posInt = arrayIntPos vp + posVar = arrayVarPos vp + val = arrayVal vp + isArr = isArray vp + res = getArray' name posInt posVar val + + +-- Auxiliar function to getArray. +getArray' :: Maybe String + -> Maybe Integer + -> Maybe String + -> Maybe Integer + -> Maybe Arrays +getArray' (Just name) (Just pos) Nothing (Just val) = + Just $ singleton name $ singleton (show pos) val +getArray' (Just name) Nothing (Just pos) (Just val) = + Just $ singleton name $ singleton pos val +getArray' _ _ _ _ = Nothing + + + + +-- Auxiliar functions to get values from constructed ast. + + + + + +isArray :: ValuationPair -> Maybe Bool +isArray = isArray' + <=< symbol + <=< qIdentifier + <=< fstTermQualIdentierT + <=< fstTerm + + +{- | Verifies if the string correspond to a certain notation that indicates + that is an Array. + For example Z3 would have the keyword select therefor it's an array. + If it isn't an array then returns nothing + +-} +isArray' :: String -> Maybe Bool +isArray' "select" = Just True +isArray' _ = Nothing + + +-- Auxliar functions to work with arrays. +{- | Retrives the name of the array. + Works with: + - Z3. +-} + +arrayName :: ValuationPair -> Maybe String +arrayName = symbol + <=< qIdentifier + <=< termQualIdentifier + <=< fstValArray + <=< sndTermQualIdentierT + <=< fstTerm + where fstValArray x = Just $ head x + +{-| Retrives the position of the array if it is an Integer. + Works with: + - Z3. +-} +arrayIntPos :: ValuationPair -> Maybe Integer +arrayIntPos = numeral + <=< getTermSpecConstant + <=< sndValArray + <=< sndTermQualIdentierT + <=< fstTerm + where sndValArray x = Just $ x !! 1 + +{-| Retrives the position of the array if it is a String. + Works with: + - Z3. +-} +arrayVarPos :: ValuationPair -> Maybe String +arrayVarPos = symbol + <=< qIdentifier + <=< termQualIdentifier + <=< sndValArray + <=< sndTermQualIdentierT + <=< fstTerm + where sndValArray x = Just $ x !! 1 + + +{-| Retrives the value of an array. + Works with: + - Z3. +-} +arrayVal :: ValuationPair -> Maybe Integer +arrayVal = numeral <=< getTermSpecConstant <=< sndTerm + + + +{- | Retrive the name of a variable. + Works with: + - Z3. + +-} + +getVarName :: ValuationPair -> Maybe String +getVarName = symbol <=< qIdentifier <=< termQualIdentifier <=< fstTerm + + +{- | Retrive the variable of a variable. + Works with: + - Z3. + +-} +getVarValue :: ValuationPair -> Maybe Integer +getVarValue = numeral <=< getTermSpecConstant <=< sndTerm + + + +{- | Retrives the name of a function. + Works with: + - Z3 +-} +getFunName :: ValuationPair -> Maybe String +getFunName = symbol <=< qIdentifier <=< fstTermQualIdentierT <=< fstTerm + + + +{- | Retrives the result of a function if it is a Integer. + Works with: + - Z3. +-} + + +getFunResult :: ValuationPair -> Maybe Value +getFunResult vp = getFunResultBool vp <|> getFunResultInt vp + +getFunResultBool :: ValuationPair -> Maybe Value +getFunResultBool = VBool <#> toBool <=< getFunResultBool' + + +getFunResultInt :: ValuationPair -> Maybe Value +getFunResultInt = VInt <#> getFunResultInt' + + + +(<#>):: Functor m => (b -> c) -> (a -> m b) -> a -> m c +(<#>) f m = \x -> f <$> m x + +toBool :: String -> Maybe Bool +toBool "true" = Just True +toBool "false" = Just False +toBool _ = Nothing + +getFunResultInt' :: ValuationPair -> Maybe Integer +getFunResultInt' = numeral <=< getTermSpecConstant <=< sndTerm + + +getFunResultBool' :: ValuationPair -> Maybe String +getFunResultBool' = symbol <=< qIdentifier <=< termQualIdentifier <=< sndTerm + + +{- | Retrives the result of a bitvector. + Works with: + - Z3 +-} +getHexVal :: ValuationPair -> Maybe String +getHexVal = hex <=< getTermSpecConstant <=< fstTerm + + +-- Auxiliar functions to get specific value from ast. + + +-- | Returns the first term of a valuation pair. +fstTerm :: ValuationPair -> Maybe Term +fstTerm (ValuationPair a _) = Just a + + +-- | Returns the second term of a valuation pair. +sndTerm :: ValuationPair -> Maybe Term +sndTerm (ValuationPair _ b) = Just b + + +-- | Returns the list of terms from TermQualIdeintifierT +sndTermQualIdentierT :: Term -> Maybe [Term] +sndTermQualIdentierT (TermQualIdentifierT _ ts) = Just ts +sndTermQualIdentierT _ = Nothing + +fstTermQualIdentierT :: Term -> Maybe QualIdentifier +fstTermQualIdentierT (TermQualIdentifierT qi _) = Just qi +fstTermQualIdentierT _ = Nothing + + +termQualIdentifier :: Term -> Maybe QualIdentifier +termQualIdentifier (TermQualIdentifier a) = Just a +termQualIdentifier _ = Nothing + + +getTermSpecConstant :: Term -> Maybe SpecConstant +getTermSpecConstant (TermSpecConstant spc) = Just spc +getTermSpecConstant _ = Nothing + + +qIdentifier :: QualIdentifier -> Maybe Identifier +qIdentifier (QIdentifier a) = Just a +qIdentifier _ = Nothing + +symbol :: Identifier -> Maybe String +symbol (ISymbol s) = Just s +symbol _ = Nothing + + +numeral :: SpecConstant -> Maybe Integer +numeral (SpecConstantNumeral n) = Just n +numeral _ = Nothing + +hex :: SpecConstant -> Maybe String +hex (SpecConstantHexadecimal shex) = Just shex +hex _ = Nothing diff --git a/Hsmtlib/Solvers/Cmd/Parser/Parsers.hs b/Hsmtlib/Solvers/Cmd/Parser/Parsers.hs new file mode 100644 --- /dev/null +++ b/Hsmtlib/Solvers/Cmd/Parser/Parsers.hs @@ -0,0 +1,538 @@ + module Hsmtlib.Solvers.Cmd.Parser.Parsers where + +import Control.Applicative as Ctr hiding ((<|>)) +import Control.Monad +import Data.Functor.Identity +import Hsmtlib.Solvers.Cmd.Parser.Syntax as CmdRsp +import Text.Parsec.Prim as Prim +import Text.ParserCombinators.Parsec as Pc + + + +(<:>) :: Applicative f => f a -> f [a] -> f [a] +(<:>) a b = (:) <$> a <*> b + +(<++>) :: Applicative f => f [a] -> f [a] -> f [a] +(<++>) a b = (++) <$> a <*> b + + +--Auxiliar parsers +aspO :: ParsecT String u Identity Char +aspO = char '(' + +aspC :: ParsecT String u Identity Char +aspC = char ')' + +aspUS :: ParsecT String u Identity Char +aspUS = char '_' + +numeral :: ParsecT String u Identity String +numeral = many1 digit + +decimal :: ParsecT String u Identity String +decimal = numeral <++> dot <++> zeros <++> numeral + +zeros :: ParsecT String u Identity String +zeros = Pc.many $ char '0' + +dot :: ParsecT String u Identity String +dot = string "." + +hexadecimal :: ParsecT String u Identity String +hexadecimal = string "#x" *> many1 hexDigit + +binary :: ParsecT String u Identity String +binary = string "#b" *> many1 bin + +bin :: ParsecT String u Identity Char +bin = char '0' <|> char '1' + + +str :: ParsecT String u Identity String +str = string "\"" <++> Pc.many (alphaNum <|> char ' ') <++> string "\"" + + +symbol :: ParsecT String u Identity String +symbol = simpleSymbol <|> quotedSymbol + +quotedSymbol :: ParsecT String u Identity String +quotedSymbol = char '|' <:> Pc.many alphaNum <++> string "|" + +simpleSymbol :: ParsecT String u Identity String +simpleSymbol = (letter <|> spcSymb) <:> sq + where sq = Pc.many (alphaNum <|> spcSymb) + +spcSymb :: ParsecT String u Identity Char +spcSymb = oneOf "+-/*=%?!.$_~^&<>" + + +keyword :: ParsecT String u Identity String +keyword = char ':' <:> Pc.many (alphaNum<|> spcSymb) + + +reservedWords :: ParsecT String u Identity String +reservedWords = string "let" + <|> string "par" + <|> string "_" + <|> string "!" + <|> string "as" + <|> string "forall" + <|> string "exists" + <|> string "NUMERAL" + <|> string "DECIMAL" + <|> string "STRING" + +bValue :: ParsecT String u Identity Bool +bValue = (string "true" >> return True) <|> + (string "false" >> return False) + + +-- Parse spec_constant +parseNumeral :: ParsecT String u Identity SpecConstant +parseNumeral = liftM SpecConstantNumeral (read <$> numeral) + +parseDecimal :: ParsecT String u Identity SpecConstant +parseDecimal = liftM SpecConstantDecimal decimal + +parseHexadecimal :: ParsecT String u Identity SpecConstant +parseHexadecimal = liftM SpecConstantHexadecimal hexadecimal + +parseBinary :: ParsecT String u Identity SpecConstant +parseBinary = liftM SpecConstantBinary binary + +parseString :: ParsecT String u Identity SpecConstant +parseString = liftM SpecConstantString str + + + +parseSpecConstant :: ParsecT String u Identity SpecConstant +parseSpecConstant = Pc.try parseDecimal + <|> parseNumeral + <|> parseHexadecimal + <|> parseBinary + <|> parseString + + + +-- parse S-expressions, for the parsing to work newlines must be removed + +parseSexprConstant :: ParsecT String u Identity Sexpr +parseSexprConstant = liftM SexprSpecConstant parseSpecConstant + +parseSexprSymbol :: ParsecT String u Identity Sexpr +parseSexprSymbol = liftM SexprSymbol symbol + +parseSexprKeyword :: ParsecT String u Identity Sexpr +parseSexprKeyword = liftM SexprSymbol keyword + +parseSexprS :: ParsecT String u Identity Sexpr +parseSexprS = do + aspO + spaces + res <- sepBy parseSexpr' spaces + aspC + spaces + return $ SexprSxp res + + +parseSexpr' :: ParsecT String u Identity Sexpr +parseSexpr' = parseSexprConstant + <|> parseSexprSymbol + <|> parseSexprKeyword + <|> parseSexprS + +parseSexpr :: ParsecT String u Identity [Sexpr] +parseSexpr = sepBy parseSexpr' spaces + + + + +-- Parse identifier +parseIdentifier :: ParsecT String u Identity Identifier +parseIdentifier = parseOnlySymbol <|> parseNSymbol + +parseOnlySymbol :: ParsecT String u Identity Identifier +parseOnlySymbol = liftM ISymbol symbol + +parseNSymbol :: ParsecT String u Identity Identifier +parseNSymbol = + do aspO + spaces + aspUS + spaces + symb <- symbol + spaces + num <- many1 (numeral <|> string " ") + spaces + aspC + return $ I_Symbol symb num + + +-- Parse Sorts +parseSort :: ParsecT String u Identity [Sort] +parseSort = sepBy parseSort' spaces + +parseSort' :: ParsecT String u Identity Sort +parseSort' = Pc.try parseIdentifierS <|> parseIdentifierSort + +parseIdentifierS :: ParsecT String u Identity Sort +parseIdentifierS = liftM SortId parseIdentifier + +parseIdentifierSort :: ParsecT String u Identity Sort +parseIdentifierSort = do + aspO + spaces + identifier <- parseIdentifier + spaces + sorts <- sepBy1 parseSort' spaces + spaces + aspC + return $ SortIdentifiers identifier sorts + + + + +--Parse Attribute Value +parseAttributeValue :: ParsecT String u Identity AttrValue +parseAttributeValue = parseAVSC <|> parseAVS <|> parseAVSexpr + +parseAVSC :: ParsecT String u Identity AttrValue +parseAVSC = liftM AttrValueConstant parseSpecConstant + +parseAVS :: ParsecT String u Identity AttrValue +parseAVS = liftM AttrValueSymbol symbol + +parseAVSexpr :: ParsecT String u Identity AttrValue +parseAVSexpr = do + aspO + spaces + expr <- parseSexpr + aspC + return $ AttrValueSexpr expr + +-- Parse Attribute +parseAttribute :: ParsecT String u Identity Attribute +parseAttribute = do + key <- keyword + spaces + attr <- optionMaybe parseAttributeValue + case attr of + Nothing -> return $ Attribute key + Just val -> return $ AttributeVal key val + + + + +-- Parse terms + +-- -- Parse Qual identifier +parseQualIdentifier :: ParsecT String u Identity QualIdentifier +parseQualIdentifier = Pc.try parseQID <|> parseQIAs + +parseQID :: ParsecT String u Identity QualIdentifier +parseQID = liftM QIdentifier parseIdentifier + +parseQIAs :: ParsecT String u Identity QualIdentifier +parseQIAs = do + aspO + spaces + string "as" + spaces + ident <- parseIdentifier + spaces + sort <- parseSort' + spaces + aspC + return $ QIdentifierAs ident sort + + +-- -- Parse Var Binding +parseVarBinding :: ParsecT String u Identity VarBinding +parseVarBinding = do + aspO + spaces + symb <- symbol + spaces + term <- parseTerm + spaces + aspC + return $ VB symb term + + + + +-- -- Parse Sorted Var +parseSortedVar :: ParsecT String u Identity SortedVar +parseSortedVar = do + aspO + spaces + symb <- symbol + spaces + sort <- parseSort' + spaces + aspC + return $ SV symb sort + + +-- Term +parseTerm :: ParsecT String u Identity Term +parseTerm = parseTSPC + <|> Pc.try parseTQID + <|> Pc.try parseTQIT + <|> Pc.try parseTermLet + <|> Pc.try parseTermFA + <|> Pc.try parseTermEX + <|> parseTermAnnot + +parseTSPC :: ParsecT String u Identity Term +parseTSPC = liftM TermSpecConstant parseSpecConstant + +parseTQID :: ParsecT String u Identity Term +parseTQID = liftM TermQualIdentifier parseQualIdentifier + +parseTQIT :: ParsecT String u Identity Term +parseTQIT = do + aspO + spaces + iden <- parseQualIdentifier + spaces + terms <- sepBy1 parseTerm spaces + aspC + return $ TermQualIdentifierT iden terms + +parseTermLet :: ParsecT String u Identity Term +parseTermLet = do + aspO + spaces + string "let" + spaces + aspO + spaces + vb <- sepBy1 parseVarBinding spaces + aspC + spaces + term <- parseTerm + spaces + aspC + return $ TermLet vb term + +parseTermFA :: ParsecT String u Identity Term +parseTermFA = do + aspO + spaces + string "forall" + spaces + aspO + sv <- sepBy1 parseSortedVar spaces + aspC + spaces + term <- parseTerm + spaces + aspC + return $ TermForall sv term + + +parseTermEX :: ParsecT String u Identity Term +parseTermEX = do + aspO + spaces + string "exists" + spaces + aspO + sv <- sepBy1 parseSortedVar spaces + aspC + spaces + term <- parseTerm + spaces + aspC + return $ TermExists sv term + +parseTermAnnot :: ParsecT String u Identity Term +parseTermAnnot = do + aspO + spaces + char '!' + spaces + term <- parseTerm + spaces + attr <- sepBy1 parseAttribute spaces + aspC + return $ TermAnnot term attr + + + + +--Parser for CmdGenResponse + +parseCmdGenResponse :: ParsecT String u Identity CmdResponse +parseCmdGenResponse = + (string "unsupported" >> return (CmdGenResponse Unsupported)) + <|> (string "success" >> return (CmdGenResponse Success)) + <|> parseCmdGenRepError + +parseCmdGenRepError :: ParsecT String u Identity CmdResponse +parseCmdGenRepError = do + aspO + string "error" + space + char '"' + cont <- Pc.many (alphaNum<|> char ':'<|> char ' ') + char '"' + aspC + return $ CmdGenResponse $ CmdRsp.Error cont + +-- Parsers for CmdGetInfoResponse + +parseCmdGetInfoResponse :: ParsecT String u Identity CmdResponse +parseCmdGetInfoResponse = liftM CmdGetInfoResponse parseGetInfoResponse + + +parseGetInfoResponse :: ParsecT String u Identity [InfoResponse] +parseGetInfoResponse = do + aspO + spaces + infoResp <- sepBy1 parseInfoResponse spaces + aspC + return infoResp + + +parseInfoResponse :: ParsecT String u Identity InfoResponse +parseInfoResponse = + Pc.try parseResponseName <|> + Pc.try parseResponseErrorBehavior <|> + Pc.try parseResponseAuthors <|> + Pc.try parseResponseVersion <|> + Pc.try parseResponseReasonUnknown <|> + parseResponseAttribute + + + + +parseResponseName :: ParsecT String u Identity InfoResponse +parseResponseName = string "name" *> space *> liftM ResponseName str + + +parseResponseErrorBehavior :: ParsecT String u Identity InfoResponse +parseResponseErrorBehavior = string "error-behavior" *> space *> + liftM ResponseErrorBehavior parseErrorBehavior + +parseErrorBehavior :: ParsecT String u Identity ErrorBehavior +parseErrorBehavior = + (string "immediate-exit" >> return ImmediateExit) <|> + (string "continued-execution" >> return ContinuedExecution) + + +parseResponseAuthors :: ParsecT String u Identity InfoResponse +parseResponseAuthors = string "authors" *> space *> + liftM ResponseAuthors str + +parseResponseVersion :: ParsecT String u Identity InfoResponse +parseResponseVersion = string "version" *> space *> + liftM ResponseVersion str + + +parseResponseReasonUnknown :: ParsecT String u Identity InfoResponse +parseResponseReasonUnknown = string "reason" *> space *> + liftM ResponseReasonUnknown parseReasonUnknown + +parseResponseAttribute :: ParsecT String u Identity InfoResponse +parseResponseAttribute = liftM ResponseAttribute parseAttribute + + +-- Parser for check sat response +parseCheckSatResponse :: ParsecT String u Identity CheckSatResponse +parseCheckSatResponse = + (string "sat" >> return Sat) <|> + (string "unsat" >> return Unsat) <|> + (string "unknown" >> return Unknown) + +-- parse Get Assertion Response +parseGetAssertionResponse :: ParsecT String u Identity [Term] +parseGetAssertionResponse = do + aspO + spaces + terms <- sepBy1 parseTerm spaces + aspC + return terms + +-- parse Get Proof response +parseGetProofResponse :: ParsecT String u Identity Sexpr +parseGetProofResponse = parseSexpr' + + +-- parse Get unsat core response +parseGetUnsatCoreResp :: ParsecT String u Identity [String] +parseGetUnsatCoreResp = do + aspO + spaces + symb <- sepBy1 symbol spaces + aspC + return symb + + +-- parse Get Value response +parseGetValueResponse :: ParsecT String u Identity [ValuationPair] +parseGetValueResponse = aspO *> sepBy1 parseValuationPair spaces <* aspC + +parseValuationPair :: ParsecT String u Identity ValuationPair +parseValuationPair = do + aspO + spaces + term1 <- parseTerm + spaces + term2 <- parseTerm + spaces + aspC + return $ ValuationPair term1 term2 + + +-- parse t valuation pair +parseTValuationPair :: ParsecT String u Identity TValuationPair +parseTValuationPair = do + aspO + spaces + symb <- symbol + spaces + bval <- bValue + spaces + aspC + return $ TValuationPair symb bval + + + +-- parse get Assignent Response +parseGetAssignmentResp :: ParsecT String u Identity [TValuationPair] +parseGetAssignmentResp = do + aspO + spaces + pairs <- sepBy1 parseTValuationPair spaces + aspC + return pairs + + +-- parse Get Option Response +parseGetOptionResponse :: ParsecT String u Identity AttrValue +parseGetOptionResponse = parseAttributeValue + + + +parseReasonUnknown :: ParsecT String u Identity ReasonUnknown +parseReasonUnknown = + (string "memout" >> return Memout) <|> + (string "incomplete" >> return Incomplete) + + +--Parser for CmdResponse +{-- +resultParser :: ParsecT String u Identity CmdResponse +resultParser = parseCmdGenResponse + <|> parseCmdGetInfoResponse + +--} + +main :: IO a +main = forever $ do putStrLn "Enter a string: " + input <- getLine + parseTest parseGetValueResponse input + --parseIdentifier + --parseTest parseTerm input diff --git a/Hsmtlib/Solvers/Cmd/Parser/Syntax.hs b/Hsmtlib/Solvers/Cmd/Parser/Syntax.hs new file mode 100644 --- /dev/null +++ b/Hsmtlib/Solvers/Cmd/Parser/Syntax.hs @@ -0,0 +1,153 @@ +module Hsmtlib.Solvers.Cmd.Parser.Syntax where + + +-- S-expressions + +data SpecConstant = SpecConstantNumeral Integer + | SpecConstantDecimal String + | SpecConstantHexadecimal String + | SpecConstantBinary String + | SpecConstantString String + deriving (Show) + + + +data Sexpr = SexprSpecConstant SpecConstant + | SexprSymbol String + | SexprKeyword String + | SexprSxp [Sexpr] + deriving (Show) + + +-- Identifiers + +data Identifier = ISymbol String + | I_Symbol String [String] deriving (Show) + + + +-- Sorts + +data Sort = SortId Identifier | SortIdentifiers Identifier [Sort] + deriving (Show) + + + +-- Attributes + +data AttrValue = AttrValueConstant SpecConstant + | AttrValueSymbol String + | AttrValueSexpr [Sexpr] + deriving (Show) + + + +data Attribute = Attribute String + | AttributeVal String AttrValue + deriving (Show) + +-- Terms + +data QualIdentifier = QIdentifier Identifier + | QIdentifierAs Identifier Sort + deriving (Show) + + + +data VarBinding = VB String Term deriving (Show) + + + +data SortedVar = SV String Sort deriving (Show) + + + +data Term = TermSpecConstant SpecConstant + | TermQualIdentifier QualIdentifier + | TermQualIdentifierT QualIdentifier [Term] + | TermLet [VarBinding] Term + | TermForall [SortedVar] Term + | TermExists [SortedVar] Term + | TermAnnot Term [Attribute] + deriving (Show) + +-- Command Responses + +-- Gen Response + + + +data GenResponse = Unsupported | Success | Error String deriving (Show) + + +-- Error behavior + +data ErrorBehavior = ImmediateExit | ContinuedExecution deriving (Show) + + +-- Reason unknown + +data ReasonUnknown = Memout | Incomplete deriving (Show) + +-- Status + +data CheckSatResponse = Sat | Unsat | Unknown deriving (Show) + +-- Info Response + +type GetInfoResponse = [InfoResponse] + +data InfoResponse = ResponseErrorBehavior ErrorBehavior + | ResponseName String + | ResponseAuthors String + | ResponseVersion String + | ResponseReasonUnknown ReasonUnknown + | ResponseAttribute Attribute + deriving (Show) + +-- Get Assertion Response + +type GetAssertionsResponse = [Term] + + +-- Get Proof Response + +type GetProofResponse = Sexpr + + +--Get Unsat Core Response + +type GetUnsatCoreResponse = [String] + + +-- Get Valuation Pair + +data ValuationPair = ValuationPair Term Term deriving (Show) + + +type GetValueResponse = [ValuationPair] + + +-- get Assignment Response + +data TValuationPair = TValuationPair String Bool deriving (Show) + +type GetAssignmentResponse = [TValuationPair] + + +-- Get Option Response + +type GetOptionResponse = AttrValue + +-- CmdResponse + +data CmdResponse = CmdGenResponse GenResponse + | CmdGetInfoResponse GetInfoResponse + | CmdCheckSatResponse CheckSatResponse + | CmdGetAssertionResponse GetAssignmentResponse + | CmdGetProofResponse GetProofResponse + | CmdGetUnsatCoreResoponse GetUnsatCoreResponse + | CmdGetValueResponse GetValueResponse + | CmdGetAssigmnentResponse TValuationPair + | CmdGetOptionResponse GetOptionResponse + deriving (Show) diff --git a/Hsmtlib/Solvers/Cmd/Parser/Visualizers.hs b/Hsmtlib/Solvers/Cmd/Parser/Visualizers.hs new file mode 100644 --- /dev/null +++ b/Hsmtlib/Solvers/Cmd/Parser/Visualizers.hs @@ -0,0 +1,180 @@ +module Hsmtlib.Solvers.Cmd.Parser.Visualizers where + +import Hsmtlib.Solvers.Cmd.Parser.Syntax as S +import Data.List + + + + +spaces' :: Int -> Int -> String +spaces' n limit | n == limit = "" + | otherwise = " " ++ spaces' (n+1) limit + +spaces :: Int -> String +spaces = spaces' 0 + +branch' :: Int -> String +branch' nsp = "\n" ++ spaces nsp++"|\n" ++ spaces nsp ++ "|- " + +branchAr' :: Int -> String +branchAr' nsp = "\n" ++ spaces nsp ++"\n" ++ spaces (nsp+1) ++ "[" + +fbranch :: Int -> String -> String -> String +fbranch nsp mark fin = mark ++ branch' nsp ++ fin + +branch :: String -> (Int -> a -> String) -> Int -> a -> String +branch mark f nsp arg = mark ++ branch' nsp ++ f (nsp+3) arg + + +nLines :: String -> Int +nLines = length.lines + +mLines :: String ->Int -> String +mLines _ 0 = "" +mLines sps n = sps ++ "|\n" ++ mLines sps (n-1) + +showValuationPair :: Int -> ValuationPair-> String +showValuationPair nsp (ValuationPair t1 t2) = tup "ValP" nsp t1 t2 showTerm showTerm + +showSpecConstant :: SpecConstant -> String +showSpecConstant (SpecConstantNumeral int) = "Num " ++ show int +showSpecConstant (SpecConstantDecimal st) = "Dec " ++ st +showSpecConstant (SpecConstantHexadecimal st) = "Hex " ++ st +showSpecConstant (SpecConstantBinary it) = "Bin " ++ show it +showSpecConstant (SpecConstantString st) = "Str " ++ st + + +aTup :: String + -> Int + -> [a] + -> (Int -> a -> String) + -> String +aTup mark nsp arg f = + mark ++ " -[ " ++ hd ++ arr ++ endSpace++"]" + where + hd =f (nsp+8) (head arg) + bd = drop 1 arg + arr = backSpace ++ intercalate backSpace (fmap (f (nsp+8)) bd) + backSpace = "\n" ++ spaces (nsp+6) ++ ", " + endSpace = "\n" ++ spaces (nsp+6) + +dTup :: String + -> Int + -> String + -> a + -> (Int -> a -> String) + -> String +dTup mark nsp st arg f = + bMark ++ st ++ sndStr + where bMark = mark ++ branch' nsp + sndStr = branch' nsp ++ f (nsp+3) arg + +tup :: String + -> Int + -> a + -> b + -> (Int -> a -> String) + -> (Int -> b -> String) + -> String +tup mark nsp arg1 arg2 f1 f2 = + bMark ++ bf1 ++ bf2 + where bMark = mark ++ branch' nsp + bf1 = f1 (nsp+3) arg1 ++ "\n" ++ spaces nsp ++"|- " + bf2 = f2 (nsp+3) arg2 + + +tupArray :: String + -> Int + -> a + -> [b] + -> (Int -> a -> String) + -> (Int -> b -> String) + -> String +tupArray mark nsp arg1 arg2 f1 f2 = + mark ++ fstf ++ sndf + where fstf = "\n" ++spaces nsp ++ "|- " ++ f1 (nsp+3) arg1 + sndf ="\n" ++ spaces nsp ++ "|-[ " ++ hd ++ strs ++ endSpace + hd = f2 (nsp+5) (head arg2) ++ backSpace + bd = drop 1 arg2 + strs = intercalate backSpace (fmap (f2 (nsp+5)) bd) + backSpace = "\n" ++ spaces (nsp+2) ++ ", " + endSpace = "\n" ++ spaces (nsp+2) ++ "]" + +showQualIdentifier :: Int -> QualIdentifier -> String +showQualIdentifier nsp (QIdentifier qid) = branch "QI" showIdentifier nsp qid +showQualIdentifier nsp (QIdentifierAs iden srt) = + tup "QIAS" nsp iden srt showIdentifier showSort + + + +showSort :: Int -> Sort -> String +showSort nsp (SortId iden) = branch "SID" showIdentifier nsp iden +showSort nsp (SortIdentifiers iden sorts) = + tupArray "SIden" nsp iden sorts showIdentifier showSort + + + +showIdentifier :: Int -> Identifier -> String +showIdentifier _ (ISymbol st) = "IS " ++ st +showIdentifier nsp (I_Symbol str1 str2) = + "I_S" ++ fstr ++ sstr + where brc = "\n" ++ spaces nsp ++ "|\n" ++ spaces nsp + fstr = brc ++ "|- " ++ str1 + sstr = brc ++ "|- [ " ++hd ++ strs ++ end + hd = head str2 ++ "\n" + bd = drop 1 str2 + strs = intercalate "\n" (fmap ((spaces (nsp + 3) ++ ", ") ++) bd) + end = "\n" ++ spaces (nsp+3) ++ "]" + + + + +showTerm ::Int -> Term -> String +showTerm nsp (TermSpecConstant sc) = + fbranch nsp "TSC" $ showSpecConstant sc +showTerm nsp (TermQualIdentifier qi) = + branch "TQI" showQualIdentifier nsp qi +showTerm nsp (TermQualIdentifierT qi ts) = + tupArray "TQIT" nsp qi ts showQualIdentifier showTerm +showTerm nsp (TermLet vb t) = + tupArray "TLt" nsp t vb showTerm showVarBinding +showTerm nsp (TermForall sv t) = + tupArray "TFA" nsp t sv showTerm showSortedVar +showTerm nsp (TermExists sv t) = + tupArray "TE" nsp t sv showTerm showSortedVar +showTerm nsp (TermAnnot t attrs) = + tupArray "TAN" nsp t attrs showTerm showAttribute + + + + + +showVarBinding :: Int -> VarBinding -> String +showVarBinding nsp (VB stg term) = dTup "VB" nsp stg term showTerm + +showSortedVar :: Int -> SortedVar -> String +showSortedVar nsp (SV stg st) = dTup "SV" nsp stg st showSort + +showAttribute :: Int -> Attribute -> String +showAttribute nsp (Attribute st) = fbranch nsp "Attribute" st +showAttribute nsp (AttributeVal stg av) = + dTup "AttrVal" nsp stg av showAttrValue + +showAttrValue :: Int -> AttrValue -> String +showAttrValue nsp (AttrValueConstant sc) = + fbranch nsp "AVC" $ showSpecConstant sc +showAttrValue nsp (AttrValueSymbol st) = + fbranch nsp "AVS" st +showAttrValue nsp (AttrValueSexpr sxpr) = + aTup "AVSP" nsp sxpr showSexpr + + +showSexpr :: Int -> Sexpr -> String +showSexpr nsp (SexprSpecConstant sc) = + fbranch nsp "SSC" $ showSpecConstant sc +showSexpr nsp (SexprSymbol st) = + fbranch nsp "SSymb" st +showSexpr nsp (SexprKeyword st) = + fbranch nsp "SK" st +showSexpr nsp (SexprSxp sexprs) = + aTup "SSxp" nsp sexprs showSexpr diff --git a/Hsmtlib/Solvers/Cmd/ProcCom/Process.hs b/Hsmtlib/Solvers/Cmd/ProcCom/Process.hs new file mode 100644 --- /dev/null +++ b/Hsmtlib/Solvers/Cmd/ProcCom/Process.hs @@ -0,0 +1,156 @@ +{- | +Module : Process + + The following module contains method that facilitate the comunication with + the SMTSolvers. +-} +module Hsmtlib.Solvers.Cmd.ProcCom.Process + ( beginProcess + , send + , endProcess + , sendContext + , sendScript + , Process + , CmdPath + , Args + ) where + +import Control.Exception +import GHC.IO.Handle +import System.Exit +import System.Process + + +-- | Path to the process +type CmdPath = String + +-- | Argumants passed to process +type Args = [String] + +-- |Type returned by CreateProcess +type Process = + ( Maybe Handle -- process std_in pipe + , Maybe Handle -- process std_out pipe + , Maybe Handle -- process std_err pipe + , ProcessHandle -- process pid + ) + +-- | Context is just a string wich will be sent to std_in +type Context = String + + +-- Functions used in Online Mode + + +{- | + Generates a CreateProcess + with just the command, + the arguments + and creates the pipes to comunicate + -} +newProcess :: CmdPath -> Args -> CreateProcess +newProcess p a = CreateProcess + { cmdspec = RawCommand p a + , cwd = Nothing + , env = Nothing + , std_in = CreatePipe + , std_out = CreatePipe + , std_err = CreatePipe + , close_fds = False + , create_group = False + } + +-- | Creates a Process ready to be executed. +beginProcess :: CmdPath -> Args -> IO Process +beginProcess cmd path = createProcess (newProcess cmd path) + + +-- | trys to run the function. +tryIO ::(a -> IO b ) -> a -> IO ( Either IOException b ) +tryIO f arg = try $ f arg + + +{-| + Sends the desired input to the process std_in and then reads from std out. + Working smt with this method: + - z3 + - mathSat + - cvc4 +-} +send :: Process -> String -> IO String +send (Just hIn, Just hOut,_,_) cmd = do + let put_str = flip hPutStr cmd + resPut <-tryIO put_str hIn -- trys to write to std in + case resPut of + --If there was an excepion writing then return the error + Left exception -> return $ "send1: " ++ show exception + Right _ -> do -- if it was successeful + resFlush <- tryIO hFlush hIn -- trys to flush std in + case resFlush of + --if there was an exception flushing then return the error + Left exception -> return $ "send2: " ++ show exception + --if it was succeful then start reading from the std out + Right _ -> readResponse (-1) "" hOut + + +{-| + Receive a inital time to wait for the process to write to the handle, + a String wich will be added the text read from the handle and the handle. + If it was able to read a line from the handle then call the function again + but with time equals to 10. + Working smt with this methid: + - z3 + - mathSat + - cvc4 +-} +readResponse :: Int -> String -> Handle -> IO String +readResponse time str procHandle = do + -- if the process dosent write to std out this function will block. + let hWait = flip hWaitForInput time + readOut <- tryIO hWait procHandle -- trys to wait for some output in std out. + case readOut of + -- if the wait gave an exception returns the error. + Left exception -> return $ "readResponse1:" ++ show exception + Right False -> return str -- returns the lines read until now. + Right True -> do + -- if there is something to read then trys to read a line. + res_get <- tryIO hGetLine procHandle + case res_get of + -- if there was an exception then return it. + Left exception -> return $ "readResponse2:" ++ show exception + -- if some text was read then trys to read the pipe again. + Right text -> readResponse 10 (str++text) procHandle + + + +-- | Sends the signal to terminate to the running process. +endProcess :: Process -> IO ExitCode +endProcess (_,_,_,processHandle) = do + terminateProcess processHandle + waitForProcess processHandle + + + +-- Function used in ContextMode + +{-| + It's the same function as readProcess. + + -} +sendContext :: CmdPath -> Args -> Context -> IO String +sendContext = readProcess + + + +{-| +Calls readProcess and pass as arguments the arguments given plus the name of +the file with the context. +An empty String is passed to the std_in. + +It's the same function as readProcess. +readProcess: + +-} +sendScript :: CmdPath -> Args -> FilePath -> IO String +sendScript cmdPath args script_name = + readProcess cmdPath (args ++ [script_name]) "" diff --git a/Hsmtlib/Solvers/Cmd/ScriptCmd.hs b/Hsmtlib/Solvers/Cmd/ScriptCmd.hs new file mode 100644 --- /dev/null +++ b/Hsmtlib/Solvers/Cmd/ScriptCmd.hs @@ -0,0 +1,129 @@ +{- | +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 diff --git a/Hsmtlib/Solvers/Cvc4.hs b/Hsmtlib/Solvers/Cvc4.hs new file mode 100644 --- /dev/null +++ b/Hsmtlib/Solvers/Cvc4.hs @@ -0,0 +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} diff --git a/Hsmtlib/Solvers/MathSAT.hs b/Hsmtlib/Solvers/MathSAT.hs new file mode 100644 --- /dev/null +++ b/Hsmtlib/Solvers/MathSAT.hs @@ -0,0 +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 = + BSolver { Slv.executeBatch = B.executeBatch (path config) (args config) logic} diff --git a/Hsmtlib/Solvers/Yices.hs b/Hsmtlib/Solvers/Yices.hs new file mode 100644 --- /dev/null +++ b/Hsmtlib/Solvers/Yices.hs @@ -0,0 +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 = + BSolver { Slv.executeBatch = B.executeBatch (path config) (args config) logic} diff --git a/Hsmtlib/Solvers/Z3.hs b/Hsmtlib/Solvers/Z3.hs new file mode 100644 --- /dev/null +++ b/Hsmtlib/Solvers/Z3.hs @@ -0,0 +1,172 @@ +{- | +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} diff --git a/LICENSE b/LICENSE new file mode 100644 --- /dev/null +++ b/LICENSE @@ -0,0 +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. diff --git a/Setup.hs b/Setup.hs new file mode 100644 --- /dev/null +++ b/Setup.hs @@ -0,0 +1,2 @@ +import Distribution.Simple +main = defaultMain