Coverage.ExtractSourceExtracts witness paths from coverage analysis graphs. Propagates rejectable lookaheads backward from sink nodes through predecessor links, identifying maximal nodes where user-reached goals intersect with unaccepted lookaheads.
val compute_maximal_prefixes :
graph:('n, 'term) Enum._graph ->
iter_sinks:(('n Fix.Indexing.index -> int -> unit) -> unit) ->
reached:('n Fix.Indexing.index -> 'goal Utils.Misc.indexset) ->
('n Fix.Indexing.index list * 'term Utils.IndexSet.t) list arrayCompute maximal prefixes: paths from sink nodes back to nodes where goals have been reached. Rejectable lookaheads are propagated backward through predecessors, intersected with each predecessor's unaccepted set. Results are grouped by propagation depth.
val compute_global_prefixes :
graph:('n, 'term) Enum._graph ->
maximals:('n Fix.Indexing.index list * 'term Utils.Misc.indexset) list array ->
reached:('n Fix.Indexing.index -> 'goal Utils.Misc.indexset) ->
('n Fix.Indexing.index list * 'term Utils.Misc.indexset) list arrayCompute global prefixes: propagate rejectable lookaheads from maximal nodes further backward, collecting all nodes where goals were reached. Unlike compute_maximal_prefixes, which stops at the first goal node, this continues propagation to find all goal intersections along each path. Results are grouped by propagation depth.