liquid-fixpoint-0.4.0.0: Predicate Abstraction-based Horn-Clause/Implication Constraint Solver

Safe Haskell	None
Language	Haskell98

Language.Fixpoint.Solver.Worklist

Contents

Worklist type is opaque
Initialize
Pop off a constraint
Add a constraint and all its dependencies

Synopsis

Worklist type is opaque

data Worklist a Source

Instances

PPrint (Worklist a)

Initialize

init :: Config -> FInfo a -> Worklist a Source

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

Pop off a constraint

pop :: Worklist a -> Maybe (SubC a, Worklist a) Source

Add a constraint and all its dependencies

push :: SubC a -> Worklist a -> Worklist a Source