| Safe Haskell | None |
|---|---|
| Language | Haskell98 |
Language.Fixpoint.Solver.Monad
Description
This is a wrapper around IO that permits SMT queries
- type SolveM = StateT SolverState IO
- runSolverM :: Config -> GInfo c b -> Int -> SolveM a -> IO a
- getBinds :: SolveM BindEnv
- filterValid :: Expr -> Cand a -> SolveM [a]
- checkSat :: Expr -> SolveM Bool
- smtEnablrmbqi :: SolveM ()
- data Stats
- tickIter :: Bool -> SolveM Int
- stats :: SolveM Stats
- numIter :: Stats -> Int
Type
type SolveM = StateT SolverState IO Source
Solver Monadic API ---------------------------------------------------
Execution
Get Binds
SMT Query
filterValid :: Expr -> Cand a -> SolveM [a] Source
SMT Interface --------------------------------------------------------
smtEnablrmbqi :: SolveM () Source