Language.Fixpoint.Solver.Worklist

Worklist type is opaque

data Worklist a

Worklist ------------------------------------------------------------------

Instances

PTable (Worklist a)

Defined in Language.Fixpoint.Solver.Worklist

Methods

ptable :: Worklist a -> DocTable

PPrint (Worklist a)

Defined in Language.Fixpoint.Solver.Worklist

Methods

pprintTidy :: Tidy -> Worklist a -> Doc

pprintPrec :: Int -> Tidy -> Worklist a -> Doc

data Stats

Instances

Eq Stats

Defined in Language.Fixpoint.Solver.Worklist

Methods

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

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

Show Stats

Defined in Language.Fixpoint.Solver.Worklist

Methods

showsPrec :: Int -> Stats -> ShowS

show :: Stats -> String

showList :: [Stats] -> ShowS

PTable Stats

Defined in Language.Fixpoint.Solver.Worklist

Methods

ptable :: Stats -> DocTable

Initialize

init :: SolverInfo a b -> Worklist a

Initialize worklist and slice out irrelevant constraints ------------------

Pop off a constraint

pop :: Worklist a -> Maybe (SimpC a, Worklist a, Bool, Int)

Add a constraint and all its dependencies

push :: SimpC a -> Worklist a -> Worklist a

Constraints with Concrete RHS

unsatCandidates :: Worklist a -> [SimpC a]

Candidate Constraints to be checked AFTER computing Fixpoint ---------

Statistics

wRanks :: Worklist a -> Int