liquid-fixpoint-0.9.6.3: Predicate Abstraction-based Horn-Clause/Implication Constraint Solver
Safe HaskellSafe-Inferred
LanguageHaskell98

Language.Fixpoint.Graph.Partition

Description

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

Synopsis

Split constraints

data CPart c a Source #

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

Constructors

CPart 

Fields

Instances

Instances details
Monoid (CPart c a) Source # 
Instance details

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 #

Semigroup (CPart c a) Source # 
Instance details

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 #

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

partition' :: TaggedC c a => Maybe MCInfo -> GInfo c a -> [GInfo c a] Source #

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 Source #

Arguments

:: MCInfo

Describes thresholds and partition 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 Source #

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

Constructors

MCInfo 

Instances

Instances details
Show MCInfo Source # 
Instance details

Defined in Language.Fixpoint.Graph.Partition

Debug

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