Module Ir.Schedule_space

The partial-schedule decision space (gh-ocannl-514 phases 1-2): the representation branch-and-bound schedule search operates on, per docs/proposals/gh-ocannl-514.md.

A search node is a partial schedule shape — some decisions committed, the rest open. Two kinds of decision level make up the space:

Phase 2 makes the tree carry legality over partial shapes: each choice's children are judged with the same three-valued logic as Schedule.op_legality, quantified over completions — child.Refuted asserts no completion below the child is valid (with the violated constraint as witness, a decline explanation produced before any compilation, gh-ocannl-479), child.Unknown never fathoms, and construction commits to a verdict at the moment the domain is built rather than leaving branches to fail at candidate compile. A fourth verdict, child.Excluded, keeps the landed policy/legality separation (gh-ocannl-555: preferences suppress heuristic caps only, legality is non-negotiable) visible in the space itself: an Excluded branch is valid but suppressed by default-policy search economy — a driver may re-propose it by lifting the policy; it must never re-propose a Refuted one.

type placement =
  1. | Pl_inline
  2. | Pl_stage_at of Indexing.symbol
  3. | Pl_materialize

One tensor node's placement level. Pl_stage_at s materializes the node at loop s's scope — recomputed per iteration of the loops outside s, shared by the loops inside. Pl_inline and Pl_materialize are the poles the greedy flip chain already searches. Loop identity is by lowering-local symbol: persistence across fresh lowerings (schedule-cache rebinding) is the later phases' concern, like instantiation.

val sexp_of_placement : placement -> Sexplib0.Sexp.t
val compare_placement : placement -> placement -> int
val equal_placement : placement -> placement -> bool
type ('l, 'a) child =
  1. | Child of ('l, 'a) tree Stdlib.Lazy.t
    (*

    Feasible as far as construction can decide.

    *)
  2. | Unknown of string * ('l, 'a) tree Stdlib.Lazy.t
    (*

    The Op_unknown analogue: construction cannot decide (the witness says why — e.g. a permissively detected site whose mis-detections only candidate compilation rejects), so the subtree stays enumerable and a fathom must never prune it; its completions settle at candidate compile.

    *)
  3. | Excluded of string * ('l, 'a) child Stdlib.Lazy.t
    (*

    Valid but not proposed: default-policy search economy (a dominated or degenerate shape, a twin whose measured cost exceeds its possible win). The witness states the policy; the payload is the same judgment with only this policy lifted — forcing it is the driver's lift operation (lift_excluded), and the result remains subject to legality (a lifted branch may still be Refuted on other grounds). leaves, enumerate and the collectors treat the exclusion as opaque: they neither enumerate nor descend into the payload.

    *)
  4. | Refuted of string
    (*

    The Op_illegal analogue, quantified over completions: no completion below this child satisfies the family's contract — an op precondition, a resource cap, or a statically-decided emission constraint refutes them all. The witness is the violated constraint: a decline explanation produced before any compilation.

    *)
and ('l, 'a) tree =
  1. | Leaf of 'a
    (*

    A fully committed schedule shape — today, one sketch-seed parameter set.

    *)
  2. | Choice of {
    1. level : string;
    2. children : ('l * ('l, 'a) child) list;
    }
    (*

    One open decision: level names it, each child one way to commit it — carried as 'l, the decision datum identifying that commitment rather than a rendering of it (gh-ocannl-591: a consumer reading a decision back off a path matches on data, it never re-parses a display string; Autotune.Family_decision is the matmul family's such type, and its to_label with render_path is the rendering). level names the node for display and grouping only — the datum is the identity, so renaming a level is a rendering change and cannot change what a path means. A Choice whose children are all Refuted/Excluded is an infeasible node (leaves is empty). Levels appear in emission order (the order candidates reach timing), not necessarily dependency order. Verdicts are decided when the parent is constructed — fathoming needs them without expansion — while feasible children's subtrees stay lazy: expanding one is a decision, not a side effect of construction.

    *)
val leaves : ('l, 'a) tree -> 'a list

All completions of Child and Unknown branches, in tree traversal order — the order the flat enumerations produced, so a factored family's leaves replaces its seed list drop-in. Forces the reachable subtrees.

val enumerate : ('l, 'a) tree -> ((string * 'l) list * 'a) list

leaves with each completion's decision path — the committed (level, decision) vector that identifies the leaf; prefixes of these paths are the partial vectors interior nodes stand for.

val refutations : ('l, 'a) tree -> ((string * 'l) list * string) list

Every Refuted child with its decision path (ending at the refuted commitment) and witness: the shape's pre-compilation decline explanations (gh-ocannl-479), in traversal order.

val exclusions : ('l, 'a) tree -> ((string * 'l) list * string) list

Every Excluded child with path and policy witness — the branches a driver could re-propose by lifting default-policy economy.

val unknowns : ('l, 'a) tree -> ((string * 'l) list * string) list

Every Unknown child with path and witness — the branches whose verdicts only candidate compilation settles; a fathom must treat them as feasible.

type search_stats = {
  1. st_expanded : int;
    (*

    Choice nodes entered.

    *)
  2. st_scored : int;
    (*

    Leaves the score hook priced.

    *)
  3. st_unscored : int;
    (*

    Leaves the score hook declined to price (None) — never winners. The hook's None covers both genuine no-coverage and caller-side rejections; a caller wanting the split tracks it inside the hook (as Autotune.model_default does).

    *)
  4. st_fathomed : int;
    (*

    Subtrees pruned by the bound against the running threshold.

    *)
  5. st_refuted : int;
    (*

    Refuted children encountered (never entered).

    *)
  6. st_excluded : int;
    (*

    Excluded children encountered (never entered; a driver may lift).

    *)
  7. st_unknown : int;
    (*

    Unknown children entered — the bound never fathoms them.

    *)
}

The fathomed-vs-scored ledger (gh-ocannl-514 phase 6's evaluation data): how much of the space the verdicts and the bound dispatched without pricing.

val sexp_of_search_stats : search_stats -> Sexplib0.Sexp.t
val no_search_stats : search_stats

Branch-and-bound minimization over the refinement tree (gh-ocannl-514 phase 4). Depth-first in child order — the emission order — so on a bound-free run the returned minimum is the first leaf achieving it, matching the flat enumerations' min_elt tie behavior that candidate ordering relies on. The running threshold starts at incumbent (an existing candidate's cost — e.g. the untuned default's model score, or a measured time) and tightens to each new best score; a leaf wins only by strict improvement, preserving ties-to-the-incumbent.

bound is the optimistic (lower-bound) cost of a subtree's completions: a subtree whose bound is at or above the threshold is fathomed — equality fathoms because displacement needs strict improvement. Soundness is the caller's contract (Cost_model.completion_floor's): a bound that can exceed a completion's true cost prunes true winners. path is the committed (level, decision) vector down to and including the judged child — the partial vector the subtree stands for (a prefix of enumerate's paths; [] for the root) — so a bound whose floor depends on the commitments (the placement levels, where Cost_model.completion_floor's open_placement narrows as Pl_materialize commitments accumulate) can price the exact node being judged; a commitment-invariant bound (the schedule-invariant family floor) ignores it.

Verdict-fathoming and cost-fathoming are distinct relations. The Op_unknown-never-fathoms contract is about verdicts: an Unknown child is never treated as Refuted, so a directly encountered one is entered without consulting the bound (legality uncertainty is its dominant unknown, and a sound bound over possibly-nonexistent completions is vacuous there). A cost bound, by contrast, may fathom any Child subtree — nested Unknowns included — because its soundness quantifies over every completion independently of how verdicts resolve: a subtree that cannot beat the incumbent even where legal is correctly pruned. Refuted/Excluded children are never entered (the construction-time fathoms, counted separately). Unscored leaves (score = None) are counted and never win: in the untuned regime a pick must have a model price, and the measured regime handles no-coverage candidates outside the bound-driven walk.

val lift_excluded : ('l, 'a) child -> ('l, 'a) child

The policy-lift operation: Excluded (_, payload) becomes the forced payload — the same judgment with only that one policy lifted, still subject to legality; any other child is returned unchanged. Lifting is per exclusion: a payload may itself contain further Excluded children deeper in its subtree.

val count_choices : ('l, 'a) tree -> int

Interior (decision) nodes reachable through Child/Unknown; forces them.

val depth : ('l, 'a) tree -> int

Longest reachable decision chain root-to-leaf; forces reachable subtrees.

val render_path : label:('l -> string) -> (string * 'l) list -> string

A decision path as "level=label > level=label > …", each decision rendered by label. The one display form for paths: rendering is a consumer's presentation step, never how a decision is identified.