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

Safe HaskellNone
LanguageHaskell98

Language.Fixpoint.Graph.Deps

Contents

Synopsis

Remove Constraints that don't affect Targets

slice :: TaggedC c a => Config -> 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 #

DO NOT DELETE! sliceCSucc :: Slice -> CSucc sliceCSucc sl = i -> M.lookupDefault [] i im where im = M.fromList [(i, is) | (i,_,is) <- slEdges sl]

Eliminatable KVars

data Elims a Source #

Generic Dependencies ------------------------------------------------------

Constructors

Deps 

Fields

Instances

Show a => Show (Elims a) Source # 

Methods

showsPrec :: Int -> Elims a -> ShowS #

show :: Elims a -> String #

showList :: [Elims a] -> ShowS #

(Eq a, Hashable a) => Monoid (Elims a) Source # 

Methods

mempty :: Elims a #

mappend :: Elims a -> Elims a -> Elims a #

mconcat :: [Elims a] -> Elims a #

PPrint (Elims a) Source # 

Methods

pprintTidy :: Tidy -> Elims a -> Doc Source #

pprintPrec :: Int -> Tidy -> Elims a -> Doc Source #

elimVars :: TaggedC c a => Config -> GInfo c a -> ([CEdge], Elims KVar) Source #

Compute Dependencies and Cuts ---------------------------------------------

elimDeps :: TaggedC c a => GInfo c a -> [CEdge] -> HashSet KVar -> CDeps Source #

Eliminated Dependencies

Compute Raw Dependencies

kvEdges :: TaggedC c a => GInfo c a -> [CEdge] Source #

Partition

Debug

graphStatistics :: TaggedC c a => Config -> GInfo c a -> IO () Source #