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 c a

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

Constructors

CPart

Fields

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

Instances

Semigroup (CPart c a)

Defined in Language.Fixpoint.Graph.Partition

Methods

(<>) :: CPart c a -> CPart c a -> CPart c a

sconcat :: NonEmpty (CPart c a) -> CPart c a

stimes :: Integral b => b -> CPart c a -> CPart c a

Monoid (CPart c a)

Defined in Language.Fixpoint.Graph.Partition

Methods

mempty :: CPart c a

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

mconcat :: [CPart c a] -> CPart c a

partition :: (Fixpoint a, Fixpoint (c a), TaggedC c a) => Config -> GInfo c a -> IO (Result (Integer, a))

partition' :: TaggedC c a => Maybe MCInfo -> GInfo c a -> [GInfo c 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

-> GInfo c a

The originial FInfo

-> [CPart c a]

A list of the smallest possible CParts

-> [GInfo c 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

Defined in Language.Fixpoint.Graph.Partition

Methods

showsPrec :: Int -> MCInfo -> ShowS

show :: MCInfo -> String

showList :: [MCInfo] -> ShowS

mcInfo :: Config -> IO MCInfo

Debug

dumpPartitions :: (Fixpoint (c a), Fixpoint a) => Config -> [GInfo c a] -> IO ()