| Safe Haskell | None |
|---|---|
| Language | Haskell98 |
Language.Fixpoint.Solver.Monad
Description
This is a wrapper around IO that permits SMT queries
Synopsis
- type SolveM = StateT SolverState IO
- runSolverM :: Config -> SolverInfo b c -> SolveM a -> IO a
- getBinds :: SolveM BindEnv
- 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 ()
- sendConcreteBindingsToSMT :: IBindEnv -> (IBindEnv -> SolveM a) -> SolveM a
- data Stats
- tickIter :: Bool -> SolveM Int
- stats :: SolveM Stats
- numIter :: Stats -> Int
- data SolverState = SS {}
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 #
`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 #
sendConcreteBindingsToSMT :: IBindEnv -> (IBindEnv -> SolveM a) -> SolveM a Source #
SMT Interface -------------------------------------------------------------
Takes the environment of bindings already known to the SMT, and the environment of all bindings that need to be known.
Yields the ids of bindings known to the SMT
Debug
Instances
| Eq Stats Source # | |
| Data Stats Source # | |
Defined in Language.Fixpoint.Solver.Stats Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Stats -> c Stats # gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c Stats # dataTypeOf :: Stats -> DataType # dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c Stats) # dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Stats) # gmapT :: (forall b. Data b => b -> b) -> Stats -> Stats # gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Stats -> r # gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Stats -> r # gmapQ :: (forall d. Data d => d -> u) -> Stats -> [u] # gmapQi :: Int -> (forall d. Data d => d -> u) -> Stats -> u # gmapM :: Monad m => (forall d. Data d => d -> m d) -> Stats -> m Stats # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Stats -> m Stats # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Stats -> m Stats # | |
| Show Stats Source # | |
| Generic Stats Source # | |
| Semigroup Stats Source # | |
| Monoid Stats Source # | |
| ToJSON Stats Source # | |
Defined in Language.Fixpoint.Solver.Stats | |
| FromJSON Stats Source # | |
| Serialize Stats Source # | |
| NFData Stats Source # | |
Defined in Language.Fixpoint.Solver.Stats | |
| Store Stats Source # | |
| PTable Stats Source # | |
| type Rep Stats Source # | |
Defined in Language.Fixpoint.Solver.Stats type Rep Stats = D1 ('MetaData "Stats" "Language.Fixpoint.Solver.Stats" "liquid-fixpoint-0.8.10.7-Dsb9ZI1V79FKe50LlwO7R" 'False) (C1 ('MetaCons "Stats" 'PrefixI 'True) ((S1 ('MetaSel ('Just "numCstr") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 Int) :*: S1 ('MetaSel ('Just "numIter") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 Int)) :*: (S1 ('MetaSel ('Just "numBrkt") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 Int) :*: (S1 ('MetaSel ('Just "numChck") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 Int) :*: S1 ('MetaSel ('Just "numVald") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 Int))))) | |