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]

SMT Interface -------------------------------------------------------------

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

Debug

data Stats

Instances

Show Stats

Defined in Language.Fixpoint.Solver.Monad

Methods

showsPrec :: Int -> Stats -> ShowS

show :: Stats -> String

showList :: [Stats] -> ShowS

Generic Stats

Defined in Language.Fixpoint.Solver.Monad

Associated Types

type Rep Stats :: Type -> Type

Methods

from :: Stats -> Rep Stats x

to :: Rep Stats x -> Stats

NFData Stats

Defined in Language.Fixpoint.Solver.Monad

Methods

rnf :: Stats -> ()

PTable Stats

Defined in Language.Fixpoint.Solver.Monad

Methods

ptable :: Stats -> DocTable

type Rep Stats

Defined in Language.Fixpoint.Solver.Monad

type Rep Stats = D1 (MetaData "Stats" "Language.Fixpoint.Solver.Monad" "liquid-fixpoint-0.8.0.2-JBYKSUH26o01SpAxHsWEYd" 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