| Safe Haskell | Safe-Inferred |
|---|
Hsmtlib.Solver
Description
This module has most types,data and functions that a user might need to utilize the library.
- data Logic
- data Solvers
- data GenResult
- data SatResult
- data GValResult
- type Arrays = Map String (Map String Integer)
- data Value
- data Mode
- data SolverConfig = Config {}
- 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
- = Solver {
Documentation
Logics that can be passed to the start of the solver
Solvers that are currently supported.
Response from most commands that do not demand a feedback from the solver, e.g: setLogic,push,pop...
Response from the command checkSat.
data GValResult Source
Response from the command getValue
Constructors
| 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. |
Instances
type Arrays = Map String (Map String Integer)Source
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.
The type returned by getValue on constants or functions.
data SolverConfig Source
Alternative configuration of a solver which can be passed in the function
startSolver in Main
Solver data type that has all the functions.
Constructors
| Solver | |
Fields
| |
| BSolver | |
Fields
| |