Mutual Refinement for CFL Reachability

include/CFL/InterleavedDyck/MutualRefinement/ and lib/CFL/InterleavedDyck/MutualRefinement/ contain a grammar-agnostic CNF reachability and derivation-tracing engine. It is a low-level dependency of Interleaved-Dyck Staged Bounds, not a second domain-facing interleaved-Dyck solver.

Location: include/CFL/InterleavedDyck/MutualRefinement/, lib/CFL/InterleavedDyck/MutualRefinement/

Main components:

CnfGrammar stores the integer-encoded grammar.
CnfGraph stores the encoded graph instance.
IntPairHasher supports the compact map/set structures used internally.
MutualRefinementMain.cpp provides the standalone driver.

The reusable operations are ordinary CFL saturation, saturation with unary/binary derivation records, and backward closure from derived results to the original edges that contributed to them. The client supplies the grammar, integer graph encoding, refinement schedule, and result semantics.

Tracing the contributing edges comes in two modes. The eager mode, which is the default, records unary and binary derivations during saturation and walks those records backward to the original edges. The opt-in factorized mode runs ordinary saturation, which allocates no provenance records, and then lazily reconstructs the contributing edges from the saturated relations. It builds factorized Out_X/In_X views of the closure and probes the smaller relation at each binary join.

StagedBounds exposes the same choice through Options::factorized_tracing, which defaults to false; see Interleaved-Dyck Staged Bounds.

MutualRefinementMain.cpp additionally preserves the original generic file-driven experiment and its alternating refinement loop. It treats parsed labels as opaque grammar symbols; it does not assign parenthesis/bracket meaning or expose the application pipeline implemented by StagedBounds.

Responsibility Boundary

MutualRefinement does not own:

typed op/cp/ob/cb label parsing;
projected, union-Dyck, parity, or endpoint grammar selection;
regularization, condensation, or on-demand policy;
taint and value-flow benchmark semantics; or
lower-bound versus upper-bound interpretation.

Those responsibilities belong to Interleaved-Dyck Staged Bounds, which translates its structured graph into the integer representation here and uses the derivation records to decide which original edges survive the next refinement round.

The implementation is best treated as a focused research component within the broader CFL subsystem.

Experiment workflow

Prepare the grammar and graph using the integer encodings expected by the component, then run the standalone driver to evaluate the refinement process. The local Grammar and Graph types are intentionally specialized; use a different CFL frontend when an application needs a stable LLVM-facing API or human-readable input format. Record the encoding and benchmark corpus when comparing refinement strategies.

cmake --build build --target lotus-cfl-interleaved-dyck-mutual-refinement
build/bin/lotus-cfl-interleaved-dyck-mutual-refinement grammars.txt graph.dot refine
build/bin/lotus-cfl-interleaved-dyck-mutual-refinement grammars.txt graph.dot refine --factorized-tracing

The mode is naive or refine. Grammar symbols and graph labels are opaque strings that are encoded to integers before invoking CnfGraph. Pass --factorized-tracing after the mode to replace eager derivation records with lazy reconstruction from the saturated relations; without it the driver keeps the original eager records.