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

Safe HaskellNone
LanguageHaskell98

Language.Fixpoint.Graph.Partition

Contents

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

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 #

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

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

Constructors

MCInfo 
Instances
Show MCInfo Source # 
Instance details

Defined in Language.Fixpoint.Graph.Partition

Debug

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