Safe Haskell | Safe-Inferred |
---|---|
Language | GHC2021 |
Synopsis
- data Solver
- data SolverInstance = SolverInstance {
- solvertype :: Solver
- stdin :: Handle
- stdout :: Handle
- stderr :: Handle
- process :: ProcessHandle
- newtype SolverGroup = SolverGroup (Chan Task)
- data Task = Task {}
- data CheckSatResult
- isSat :: CheckSatResult -> Bool
- isErr :: CheckSatResult -> Bool
- isUnsat :: CheckSatResult -> Bool
- checkSat :: SolverGroup -> SMT2 -> IO CheckSatResult
- withSolvers :: Solver -> Natural -> Maybe Natural -> (SolverGroup -> IO a) -> IO a
- getModel :: SolverInstance -> CexVars -> IO SMTCex
- mkTimeout :: Maybe Natural -> Text
- solverArgs :: Solver -> Maybe Natural -> [Text]
- spawnSolver :: Solver -> Maybe Natural -> IO SolverInstance
- stopSolver :: SolverInstance -> IO ()
- sendScript :: SolverInstance -> SMT2 -> IO (Either Text ())
- sendCommand :: SolverInstance -> Text -> IO Text
- sendLine :: SolverInstance -> Text -> IO Text
- sendLine' :: SolverInstance -> Text -> IO ()
- getValue :: SolverInstance -> Text -> IO Text
- readSExpr :: Handle -> IO [Text]
- splitSExpr :: [Text] -> Text
- data Par
- getSExpr :: Text -> (Text, Text)
Documentation
Supported solvers
data SolverInstance Source #
A running solver instance
SolverInstance | |
|
A script to be executed, a list of models to be extracted in the case of a sat result, and a channel where the result should be written
Task | |
|
data CheckSatResult Source #
The result of a call to (check-sat)
Instances
Show CheckSatResult Source # | |
Defined in EVM.Solvers showsPrec :: Int -> CheckSatResult -> ShowS # show :: CheckSatResult -> String # showList :: [CheckSatResult] -> ShowS # | |
Eq CheckSatResult Source # | |
Defined in EVM.Solvers (==) :: CheckSatResult -> CheckSatResult -> Bool # (/=) :: CheckSatResult -> CheckSatResult -> Bool # |
isSat :: CheckSatResult -> Bool Source #
isErr :: CheckSatResult -> Bool Source #
isUnsat :: CheckSatResult -> Bool Source #
checkSat :: SolverGroup -> SMT2 -> IO CheckSatResult Source #
withSolvers :: Solver -> Natural -> Maybe Natural -> (SolverGroup -> IO a) -> IO a Source #
solverArgs :: Solver -> Maybe Natural -> [Text] Source #
Arguments used when spawing a solver instance
spawnSolver :: Solver -> Maybe Natural -> IO SolverInstance Source #
Spawns a solver instance, and sets the various global config options that we use for our queries
stopSolver :: SolverInstance -> IO () Source #
Cleanly shutdown a running solver instnace
sendScript :: SolverInstance -> SMT2 -> IO (Either Text ()) Source #
Sends a list of commands to the solver. Returns the first error, if there was one.
sendCommand :: SolverInstance -> Text -> IO Text Source #
Sends a single command to the solver, returns the first available line from the output buffer
sendLine :: SolverInstance -> Text -> IO Text Source #
Sends a string to the solver and appends a newline, returns the first available line from the output buffer
sendLine' :: SolverInstance -> Text -> IO () Source #
Sends a string to the solver and appends a newline, doesn't return stdout
getValue :: SolverInstance -> Text -> IO Text Source #
Returns a string representation of the model for the requested variable
splitSExpr :: [Text] -> Text Source #