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

Safe HaskellNone
LanguageHaskell98

Language.Fixpoint.Solver.Graph

Contents

Synopsis

Remove Constraints that don't affect Targets

slice :: TaggedC c a => GInfo c a -> GInfo c a Source

Compute constraints that transitively affect target constraints, and delete everything else from F.SInfo a

Predicate describing Targets

isTarget :: TaggedC c a => c a -> Bool Source

Compute Ranks / SCCs

graphRanks :: Graph -> (Vertex -> DepEdge) -> (CMap Int, [[Vertex]]) Source

Ranks from Graph -----------------------------------------------------

Compute Kvar dependencies

cGraph :: TaggedC c a => GInfo c a -> CGraph Source

Constraint Graph -----------------------------------------------------

Kvars written and read by a constraint

kvWriteBy :: TaggedC c a => CMap (c a) -> CId -> [KVar] Source