liquid-fixpoint-0.9.2.5: Predicate Abstraction-based Horn-Clause/Implication Constraint Solver
Safe HaskellSafe-Inferred
LanguageHaskell98

Language.Fixpoint.Solver.Monad

Description

This is a wrapper around IO that permits SMT queries

Synopsis

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

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

data Stats Source #

Instances

Instances details
FromJSON Stats Source # 
Instance details

Defined in Language.Fixpoint.Solver.Stats

ToJSON Stats Source # 
Instance details

Defined in Language.Fixpoint.Solver.Stats

Data Stats Source # 
Instance details

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 #

toConstr :: Stats -> Constr #

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 # 
Instance details

Defined in Language.Fixpoint.Solver.Stats

Methods

mempty :: Stats #

mappend :: Stats -> Stats -> Stats #

mconcat :: [Stats] -> Stats #

Semigroup Stats Source # 
Instance details

Defined in Language.Fixpoint.Solver.Stats

Methods

(<>) :: Stats -> Stats -> Stats #

sconcat :: NonEmpty Stats -> Stats #

stimes :: Integral b => b -> Stats -> Stats #

Generic Stats Source # 
Instance details

Defined in Language.Fixpoint.Solver.Stats

Associated Types

type Rep Stats :: Type -> Type #

Methods

from :: Stats -> Rep Stats x #

to :: Rep Stats x -> Stats #

Show Stats Source # 
Instance details

Defined in Language.Fixpoint.Solver.Stats

Methods

showsPrec :: Int -> Stats -> ShowS #

show :: Stats -> String #

showList :: [Stats] -> ShowS #

Serialize Stats Source # 
Instance details

Defined in Language.Fixpoint.Solver.Stats

Methods

put :: Putter Stats #

get :: Get Stats #

NFData Stats Source # 
Instance details

Defined in Language.Fixpoint.Solver.Stats

Methods

rnf :: Stats -> () #

Eq Stats Source # 
Instance details

Defined in Language.Fixpoint.Solver.Stats

Methods

(==) :: Stats -> Stats -> Bool #

(/=) :: Stats -> Stats -> Bool #

PTable Stats Source # 
Instance details

Defined in Language.Fixpoint.Solver.Stats

Store Stats Source # 
Instance details

Defined in Language.Fixpoint.Solver.Stats

Methods

size :: Size Stats #

poke :: Stats -> Poke () #

peek :: Peek Stats #

type Rep Stats Source # 
Instance details

Defined in Language.Fixpoint.Solver.Stats

type Rep Stats = D1 ('MetaData "Stats" "Language.Fixpoint.Solver.Stats" "liquid-fixpoint-0.9.2.5-8VOJ4a5jXPy7nyhLFTxkOW" '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)))))

numIter :: Stats -> Int Source #

# Refine Iterations

data SolverState ann Source #

Constructors

SS 

Fields