Fixpoint3.Phase.Stratifier

Definitions

def stratify(d: Datalog): Map[PredSym, (Int32, Int32)]§ Source

Computes the stratification of d.

Returns a map from PredSym to their position within their pseudostrata: predSym -> (pseudoStratumIndex, stratumIndexInPseudoStratum)

A pseudostratum is a group of mutually independent, consecutive strata. For example, predSym -> (2, 1) means predSym belongs to stratum 1 within pseudostrata 2.