| 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
- = Success
- | Unsupported
- | Error String
- | GUError String
- 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
Constructors
| 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 |
Instances
| Show Logic |
Solvers that are currently supported.
Response from most commands that do not demand a feedback from the solver, e.g: setLogic,push,pop...
Constructors
| 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 |
Response from the command checkSat.
Constructors
| 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 |
Instances
| Show SatResult |
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
| Show GValResult |
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.
Instances
| Show Value |
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
| |