| 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 -> SolverInfo b c -> SolveM a -> IO a
- getBinds :: SolveM SolEnv
- filterRequired :: Cand a -> Expr -> SolveM [a]
- filterValid :: SrcSpan -> Expr -> Cand a -> SolveM [a]
- filterValidGradual :: [Expr] -> Cand a -> SolveM [a]
- checkSat :: Expr -> SolveM Bool
- smtEnablembqi :: SolveM ()
- data Stats
- tickIter :: Bool -> SolveM Int
- stats :: SolveM Stats
- numIter :: Stats -> Int
Type
type SolveM = StateT SolverState IO Source #
Solver Monadic API --------------------------------------------------------
Execution
runSolverM :: Config -> SolverInfo b c -> SolveM a -> IO a Source #
Get Binds
SMT Query
filterRequired :: Cand a -> Expr -> SolveM [a] Source #
SMT Interface -------------------------------------------------------------
`filterRequired [(x1, p1),...,(xn, pn)] q` returns a minimal list [xi] s.t. / [pi] => q
filterValid :: SrcSpan -> Expr -> Cand a -> SolveM [a] Source #
`filterValid p [(x1, q1),...,(xn, qn)]` returns the list `[ xi | p => qi]`
filterValidGradual :: [Expr] -> Cand a -> SolveM [a] Source #
`filterValidGradual ps [(x1, q1),...,(xn, qn)]` returns the list `[ xi | p => qi]` | for some p in the list ps
smtEnablembqi :: SolveM () Source #