Language.Fixpoint.Solver.Monad

This is a wrapper around IO that permits SMT queries

Type

type SolveM = StateT SolverState IO

Solver Monadic API --------------------------------------------------------

Execution

runSolverM :: Config -> SolverInfo b c -> SolveM a -> IO a

Get Binds

getBinds :: SolveM BindEnv

SMT Query

filterRequired :: Cand a -> Expr -> SolveM [a]

`filterRequired [(x1, p1),...,(xn, pn)] q` returns a minimal list [xi] s.t. / [pi] => q

filterValid :: SrcSpan -> Expr -> Cand a -> SolveM [a]

`filterValid p [(x1, q1),...,(xn, qn)]` returns the list `[ xi | p => qi]`

filterValidGradual :: [Expr] -> Cand a -> SolveM [a]

`filterValidGradual ps [(x1, q1),...,(xn, qn)]` returns the list `[ xi | p => qi]` | for some p in the list ps

checkSat :: Expr -> SolveM Bool

smtEnablembqi :: SolveM ()

sendConcreteBindingsToSMT :: IBindEnv -> (IBindEnv -> SolveM a) -> SolveM a

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

Instances

Eq Stats

Defined in Language.Fixpoint.Solver.Stats

Methods

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

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

Data Stats

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

Show Stats

Defined in Language.Fixpoint.Solver.Stats

Methods

showsPrec :: Int -> Stats -> ShowS

show :: Stats -> String

showList :: [Stats] -> ShowS

Generic Stats

Defined in Language.Fixpoint.Solver.Stats

Associated Types

type Rep Stats :: Type -> Type

Methods

from :: Stats -> Rep Stats x

to :: Rep Stats x -> Stats

Semigroup Stats

Defined in Language.Fixpoint.Solver.Stats

Methods

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

sconcat :: NonEmpty Stats -> Stats

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

Monoid Stats

Defined in Language.Fixpoint.Solver.Stats

Methods

mempty :: Stats

mappend :: Stats -> Stats -> Stats

mconcat :: [Stats] -> Stats

ToJSON Stats

Defined in Language.Fixpoint.Solver.Stats

Methods

toJSON :: Stats -> Value

toEncoding :: Stats -> Encoding

toJSONList :: [Stats] -> Value

toEncodingList :: [Stats] -> Encoding

FromJSON Stats

Defined in Language.Fixpoint.Solver.Stats

Methods

parseJSON :: Value -> Parser Stats

parseJSONList :: Value -> Parser [Stats]

Serialize Stats

Defined in Language.Fixpoint.Solver.Stats

Methods

put :: Putter Stats

get :: Get Stats

NFData Stats

Defined in Language.Fixpoint.Solver.Stats

Methods

rnf :: Stats -> ()

Store Stats

Defined in Language.Fixpoint.Solver.Stats

Methods

size :: Size Stats

poke :: Stats -> Poke ()

peek :: Peek Stats

PTable Stats

Defined in Language.Fixpoint.Solver.Stats

Methods

ptable :: Stats -> DocTable

type Rep Stats

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)))))

tickIter :: Bool -> SolveM Int

stats :: SolveM Stats

numIter :: Stats -> Int

# Refine Iterations

data SolverState

Constructors

SS

Fields

• ssCtx :: !Context

  SMT Solver Context

• ssBinds :: !BindEnv

  All variables and types

• ssStats :: !Stats

  Solver Statistics