dependency

Module for checking dependencies in a logic program.

AggregateDependencyGraphBuilder

Bases: DependencyGraphBuilder

Build an aggregate dependency graph.

visit_Literal(node: AST) -> AST

Process body literals: add a edge for each predicate in an aggregate.

DependencyGraphBuilder

Bases: Transformer, ABC

Base class for dependency graphs.

__init__() -> None

Initialize the dependency graph builder.

visit_Literal(node: AST) -> AST abstractmethod

Add dependencies for literals (implemented by subclasses).

visit_Rule(node: AST) -> AST

Process each rule: add head predicate as node and process body.

SignedDependencyGraphBuilder

Bases: DependencyGraphBuilder

Transformer to build a predicate dependency graph.

__init__(public_predicates: set[Predicate]) -> None

Initialize the builder with the set of public predicates.

visit_Literal(node: AST) -> AST

Process body literals: add a edge for body predicates.

has_negative_cycle(program: list[AST], public_predicates: set[Predicate]) -> bool

Check if a program fulfills uniqueness by checking a modified predicate dependency graph for negative cycles.

has_odd_negative_cycle(program: list[AST], public_predicates: set[Predicate]) -> bool

Check if a program has a negative cycle with an odd number of negations.

Only negated literals of private predicates are taken into account (exactly as for has_negative_cycle). A single negation counts as one negation while a double negation (including the implicit double negation of a private choice rule) counts as two; the latter therefore does not change the parity of a cycle.

The check reduces to a parity problem: the number of negations on a cycle is odd iff the number of single-negation private edges on it is odd. To detect such a cycle we build a parity-doubled graph with two copies of every node tagged with a parity bit, where traversing an edge flips the bit by the edge's parity. A directed cycle with odd parity through v then corresponds to (v, 0) and (v, 1) lying in the same strongly connected component of the doubled graph.

has_recursive_aggregates(program: list[AST]) -> bool

Check if a program contains recursive aggregates.