Function Stratify

analysis/stratification.go:79–101

Stratify checks whether a program can be stratified. It returns strongly-connected components and a map from predicate to stratum in the affirmative case, an error otherwise. The result list of strata is topologically sorted. Stratification means separating a list of intensional predicate symbols wi

(program Program)

// into strata (layers) such that each layer only depends on the
// evaluation of negated atoms for idb predicates in lower layers.
func Stratify(program Program) ([]Nodeset, map[ast.PredicateSym]int, error) {
	dep := makeDepGraph(program)
	strata := dep.sccs()
	predToStratum := make(map[ast.PredicateSym]int)
	for i, c := range strata {
		for sym := range c {
			predToStratum[sym] = i
		}
		for sym := range c {
			for dest, negated := range dep[sym] {
				if !negated {
					continue
				}
				// "Negative" dependency in same stratum indicates recursion through negation.
				if destStratum, ok := predToStratum[dest]; ok && destStratum == i {
					return nil, nil, fmt.Errorf("program cannot be stratified")
				}
			}
		}
	}
	strata, predToStratum = dep.sortResult(strata, predToStratum)
	return strata, predToStratum, nil
}

func (dep depGraph) initNode(src ast.PredicateSym) {
	if _, ok := dep[src]; !ok {