Hsmtlib (empty) → 0.2.0.6

raw patch · 20 files changed

+3123/−0 lines, 20 filesdep +basedep +containersdep +parsecsetup-changed

Dependencies added: base, containers, parsec, pretty, process, smtLib, transformers

Files

Hsmtlib.cabal +76/−0
Hsmtlib.hs +58/−0
Hsmtlib/HighLevel.hs +112/−0
Hsmtlib/Solver.hs +130/−0
Hsmtlib/Solvers/Altergo.hs +178/−0
Hsmtlib/Solvers/Boolector.hs +176/−0
Hsmtlib/Solvers/Cmd/BatchCmd.hs +19/−0
Hsmtlib/Solvers/Cmd/OnlineCmd.hs +88/−0
Hsmtlib/Solvers/Cmd/Parser/CmdResult.hs +388/−0
Hsmtlib/Solvers/Cmd/Parser/Parsers.hs +538/−0
Hsmtlib/Solvers/Cmd/Parser/Syntax.hs +153/−0
Hsmtlib/Solvers/Cmd/Parser/Visualizers.hs +180/−0
Hsmtlib/Solvers/Cmd/ProcCom/Process.hs +156/−0
Hsmtlib/Solvers/Cmd/ScriptCmd.hs +129/−0
Hsmtlib/Solvers/Cvc4.hs +185/−0
Hsmtlib/Solvers/MathSAT.hs +183/−0
Hsmtlib/Solvers/Yices.hs +180/−0
Hsmtlib/Solvers/Z3.hs +172/−0
LICENSE +20/−0
Setup.hs +2/−0

+ Hsmtlib.cabal view

@@ -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 <https://github.com/MfesGA/Hsmtlib>
+
+-- URL for the project homepage or repository.
+homepage:            https://github.com/MfesGA/Hsmtlib
+
+-- The license under which the package is released.
+license:          BSD3               
+
+-- The file containing the license text.
+license-file:        LICENSE
+
+-- The package author(s).
+author:              Nuno Laranjo and Rogerio Pontes
+
+-- An email address to which users can send suggestions, bug reports, and 
+-- patches.
+maintainer:          numicola@gmail.com and rogeriop062@gmail.com
+
+-- A copyright notice.
+-- copyright:           
+
+category:            SMT          
+
+build-type:          Simple
+
+-- Extra files to be distributed with the package, such as examples or a 
+-- README.
+-- extra-source-files:  
+
+-- Constraint on the version of Cabal needed to build this package.
+cabal-version:       >=1.10
+
+
+library
+  -- Modules exported by the library.
+  exposed-modules:     Hsmtlib, Hsmtlib.Solver, Hsmtlib.HighLevel, Hsmtlib.Solvers.Z3, Hsmtlib.Solvers.Yices, Hsmtlib.Solvers.MathSAT, Hsmtlib.Solvers.Cvc4, Hsmtlib.Solvers.Boolector, Hsmtlib.Solvers.Altergo, Hsmtlib.Solvers.Cmd.ScriptCmd, Hsmtlib.Solvers.Cmd.OnlineCmd, Hsmtlib.Solvers.Cmd.BatchCmd, Hsmtlib.Solvers.Cmd.ProcCom.Process, Hsmtlib.Solvers.Cmd.Parser.Visualizers, Hsmtlib.Solvers.Cmd.Parser.Syntax, Hsmtlib.Solvers.Cmd.Parser.Parsers, Hsmtlib.Solvers.Cmd.Parser.CmdResult
+  
+  -- Modules included in this library but not exported.
+  -- other-modules:       
+  
+  -- LANGUAGE extensions used by modules in this package.
+  -- other-extensions:    
+  
+  -- Other library packages from which modules are imported.
+  build-depends:       base >=4.6 && <= 4.7, smtLib >=1.0 && <1.1, containers >=0.5 && <0.6, pretty >=1.1 && <1.2, process >=1.1 && <= 1.2 , transformers >=0.3 && <0.4, parsec >=3.1 && <3.2
+  
+  -- Directories containing source files.
+  -- hs-source-dirs:      
+  
+  -- Base language which the package is written in.
+  default-language:    Haskell2010
+

+ Hsmtlib.hs view

@@ -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
+
+
+

+ Hsmtlib/HighLevel.hs view

@@ -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)

+ Hsmtlib/Solver.hs view

@@ -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 }

+ Hsmtlib/Solvers/Altergo.hs view

@@ -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}

+ Hsmtlib/Solvers/Boolector.hs view

@@ -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}

+ Hsmtlib/Solvers/Cmd/BatchCmd.hs view

@@ -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

+ Hsmtlib/Solvers/Cmd/OnlineCmd.hs view

@@ -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

+ Hsmtlib/Solvers/Cmd/Parser/CmdResult.hs view

@@ -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

+ Hsmtlib/Solvers/Cmd/Parser/Parsers.hs view

@@ -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

+ Hsmtlib/Solvers/Cmd/Parser/Syntax.hs view

@@ -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)

+ Hsmtlib/Solvers/Cmd/Parser/Visualizers.hs view

@@ -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

+ Hsmtlib/Solvers/Cmd/ProcCom/Process.hs view

@@ -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.
+<http://hackage.haskell.org/package/process-1.1.0.1/docs/System-Process.html>
+ -}
+sendContext :: CmdPath -> Args -> Context -> IO String
+sendContext = readProcess
+
+
+
+{-|
+Calls readProcess and pass as arguments the arguments given plus the name of
+the file with the context.
+An empty String is passed to the std_in.
+
+It's the same function as readProcess.
+readProcess:
+<http://hackage.haskell.org/package/process-1.1.0.1/docs/System-Process.html>
+-}
+sendScript :: CmdPath -> Args -> FilePath -> IO String
+sendScript cmdPath args script_name =
+    readProcess cmdPath (args ++ [script_name]) ""

+ Hsmtlib/Solvers/Cmd/ScriptCmd.hs view

@@ -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

+ Hsmtlib/Solvers/Cvc4.hs view

@@ -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}

+ Hsmtlib/Solvers/MathSAT.hs view

@@ -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}

+ Hsmtlib/Solvers/Yices.hs view

@@ -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}

+ Hsmtlib/Solvers/Z3.hs view

@@ -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}

+ LICENSE view

@@ -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.

+ Setup.hs view

@@ -0,0 +1,2 @@+import Distribution.Simple
+main = defaultMain