pub fn try_plan_stratified_epistemic_program(
program: &Program,
) -> Result<Option<EpistemicStratifiedPlan>>Expand description
Plan a STRATIFIED epistemic execution when the program contains a modal literal over an epistemic-derived head that is itself epistemically DETERMINED.
This intercepts exactly the chained/nested-epistemic coupling that the joint
single-enumeration path fails closed on (b :- know a where a :- know p, p
invariant). It partitions the program’s epistemic heads into strata by modal
dependency, where a head whose modal ranges over a lower DETERMINED head sits in
a strictly-higher stratum. Each stratum is a self-contained sub-program compiled
through the EXISTING single/joint epistemic path; at runtime the executor
materializes each stratum’s GATED head into the store before the next stratum
runs, so the higher stratum gates against the materialized (now-base) relation
via the existing membership filter — never via resolve-into-body.
Returns:
Ok(Some(plan))when the program genuinely needs (and admits) stratification: at least one modal literal ranges over an epistemically-determined derived head, and a sound stratification exists.Ok(None)when no modal ranges over a determined derived head (the existing joint/split/single paths own the program — e.g. example 18’s shared base modal, where the modal targetqis EDB, not a determined derived head), OR when the nested target is NOT determined (circular modality / recursion / unfounded self-support is handed back to the recursive + FAEEL/G91 guards, which keep ownership and fail closed there).