liquid-fixpoint-0.5.0.1: 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
Constraints with Concrete RHS
Statistics

Synopsis

Worklist type is opaque

data Worklist a Source

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

Instances

PTable (Worklist a) Source
PPrint (Worklist a) Source

data Stats Source

Instances

Eq Stats Source
Show Stats Source
PTable Stats Source

Initialize

init :: SInfo a -> Worklist a Source

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

Pop off a constraint

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

Add a constraint and all its dependencies

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

Constraints with Concrete RHS

unsatCandidates :: Worklist a -> [SimpC a] Source

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

Statistics

wRanks :: Worklist a -> Int Source