Function evaluate_wfs_rules 

pub fn evaluate_wfs_rules(
    rules: &[WfsRule],
    pir: &mut PirGraph,
    config: &WfsConfig,
) -> Result<WfsResult>

Evaluate a non-monotone SCC using Well-Founded Semantics.

This function takes pre-grounded rules for the SCC and computes the well-founded model using the alternating fixed-point algorithm.

Arguments

• rules - Ground rules for atoms in this SCC
• pir - PIR graph for building provenance formulas
• config - Configuration options

Returns

WfsResult containing true atoms (with provenance), false atoms, and implicitly undefined atoms (in neither set).

Algorithm

The alternating fixed-point works by interleaving two operators:

1. Unfounded set computation (Φ): Find atoms with no possible support
2. Consequence derivation (Ψ): Find atoms that must be true

Starting from (T={}, F={}):

• Compute unfounded set U = Φ(T, F)
• Add U to F
• Compute consequences C = Ψ(T, F)
• Add C to T
• Repeat until no changes