Language.Fixpoint.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)

cFileName :: FilePath

Instances

Monoid (CPart a)

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

partition'

Arguments

:: Maybe MCInfo

Nothing to produce the maximum possible number of partitions. Or a MultiCore Info to control the partitioning

-> FInfo a

-> (KVGraph, [FInfo a])

Partition an FInfo into multiple disjoint FInfos

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

mcInfo :: Config -> IO MCInfo

Queries over dependencies

graphStatistics :: Config -> SInfo a -> IO ()

data GDeps a

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

Constructors

Deps

Fields

depCuts :: !(HashSet a)

depNonCuts :: !(HashSet a)

Instances

Show a => Show (GDeps a)

(Eq a, Hashable a) => Monoid (GDeps a)

deps :: TaggedC c a => GInfo c a -> GDeps KVar

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

Debug

elimSolGraph :: Config -> Solution -> IO ()

Build and print the graph of post eliminate solution, which has an edge from k -> k' if k' appears directly inside the "solution" for k