Language.Fixpoint.Graph.Partition

This module implements functions to build constraint / kvar dependency graphs, partition them and print statistics about their structure.

Split constraints

data CPart a

Constraint Partition Container --------------------------------------------

Constructors

CPart

Fields

• pws :: !(HashMap KVar (WfC a))
• pcm :: !(HashMap Integer (SubC a))

Instances

Monoid (CPart a)

Methods

mempty :: CPart a

mappend :: CPart a -> CPart a -> CPart a

mconcat :: [CPart a] -> CPart a

partition :: Fixpoint a => Config -> FInfo a -> IO (Result (Integer, a))

partition' :: Maybe MCInfo -> FInfo a -> [FInfo a]

Partition an FInfo into multiple disjoint FInfos. Info is Nothing to produce the maximum possible number of partitions. Or a MultiCore Info to control the partitioning

partitionN

Arguments

:: MCInfo

describes thresholds and partiton amounts

-> FInfo a

The originial FInfo

-> [CPart a]

A list of the smallest possible CParts

-> [FInfo a]

At most N partitions of at least thresh work

Partition an FInfo into a specific number of partitions of roughly equal amounts of work

Information about cores

data MCInfo

Multicore info ------------------------------------------------------------

Constructors

MCInfo

Fields

• mcCores :: !Int
• mcMinPartSize :: !Int
• mcMaxPartSize :: !Int

Instances

Show MCInfo

Methods

showsPrec :: Int -> MCInfo -> ShowS

show :: MCInfo -> String

showList :: [MCInfo] -> ShowS

mcInfo :: Config -> IO MCInfo

Debug

dumpPartitions :: Fixpoint a => Config -> [FInfo a] -> IO ()