| Safe Haskell | Safe-Inferred |
|---|---|
| Language | Haskell98 |
Language.Fixpoint.Solver.Monad
Description
This is a wrapper around IO that permits SMT queries
Synopsis
- type SolveM ann = StateT (SolverState ann) IO
- runSolverM :: Config -> SolverInfo ann c -> SolveM ann a -> IO a
- getBinds :: SolveM ann (BindEnv ann)
- filterRequired :: Cand a -> Expr -> SolveM ann [a]
- filterValid :: SrcSpan -> Expr -> Cand a -> SolveM ann [a]
- filterValidGradual :: [Expr] -> Cand a -> SolveM ann [a]
- checkSat :: Expr -> SolveM ann Bool
- smtEnablembqi :: SolveM ann ()
- sendConcreteBindingsToSMT :: IBindEnv -> (IBindEnv -> SolveM ann a) -> SolveM ann a
- data Stats
- tickIter :: Bool -> SolveM ann Int
- stats :: SolveM ann Stats
- numIter :: Stats -> Int
- data SolverState ann = SS {}
Type
type SolveM ann = StateT (SolverState ann) IO Source #
Solver Monadic API --------------------------------------------------------
Execution
runSolverM :: Config -> SolverInfo ann c -> SolveM ann a -> IO a Source #
Get Binds
SMT Query
filterRequired :: Cand a -> Expr -> SolveM ann [a] Source #
`filterRequired [(x1, p1),...,(xn, pn)] q` returns a minimal list [xi] s.t. / [pi] => q
filterValid :: SrcSpan -> Expr -> Cand a -> SolveM ann [a] Source #
`filterValid p [(q1, x1),...,(qn, xn)]` returns the list `[ xi | p => qi]`
filterValidGradual :: [Expr] -> Cand a -> SolveM ann [a] Source #
`filterValidGradual ps [(x1, q1),...,(xn, qn)]` returns the list `[ xi | p => qi]` | for some p in the list ps
smtEnablembqi :: SolveM ann () Source #
sendConcreteBindingsToSMT :: IBindEnv -> (IBindEnv -> SolveM ann a) -> SolveM ann 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
| FromJSON Stats Source # | |
Defined in Language.Fixpoint.Solver.Stats | |
| ToJSON 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 # | |
| Monoid Stats Source # | |
| Semigroup Stats Source # | |
| Generic Stats Source # | |
| Show Stats Source # | |
| Serialize Stats Source # | |
| NFData Stats Source # | |
Defined in Language.Fixpoint.Solver.Stats | |
| Eq Stats Source # | |
| PTable Stats Source # | |
| Store 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.9.6.3-Fxo1c9HahAZtZcvzlvNkk" '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))))) | |