CAT and IEOCE Engines

Lotus contains faithful, SVF-independent implementations of two more recent classical CFL-reachability algorithms:

• CAT (context-aware tabulation) prunes redundant derivation work using per-symbol usage contexts and guarded grammar rewrites.

• IEOCE (iterative-epoch online cycle elimination) collapses cycles during solving and, in its OCR variant, maintains a minimum-equivalent graph.

Both engines share the input vocabulary and the compressed result representation of the Skewed engine through Solvers/Engines/Common/Reachability.h. No import or conversion is necessary between the three solvers.

CAT: Context-Aware Tabulation

Paper

The engine implements Shi and Li, ICSE 2026 (DOI 10.1145/3744916.3773222). The header describes it as an independent implementation of Figure 3 and Algorithm 2 of the paper.

Problem and key idea

The engine is a context-aware tabulation. Before solving, it analyzes the grammar and annotates the graph with usage contexts:

analyzeGrammar

Computes the first, last, left, and right terminal sets of every symbol and records which symbols have unary uses. Two semantics are available: the literal Figure-3 inference rules, including their conservative epsilon propagation, and Definitions 4.1/4.2, under which a binary right-hand side is nullable iff both operands are nullable.

annotateGraph

Computes per-node usage contexts. For each symbol, a node either has incoming or outgoing edges in the base graph, or the context holds everywhere and is recorded only as a universal flag. Sparse sets store the remaining contexts.

rewriteTransitivity

Applies the Section 4.2.1 language-preserving transitivity rewrites. The guards never add epsilon to a nonnullable transitive symbol, reverse prefix-closure orientation only for an epsilon-based one-sided closure (general B X -> X B replacement is not language preserving), and otherwise expand left and right consumers in their original order. The transformation records every rewrite event and the symbols skipped by the guards.

solve

Runs the tabulation with the configured Options. Options selects the FirstLastSemantics, whether transitivity rewriting runs, whether the earlier explicitly limited static Skewed pass is reused (conservative_static_skewing), and whether propagating symbols and dynamic skewing are enabled. The Stats record the worklist behavior, the attempts fully pruned by the usage contexts, how insertions were indexed (incoming-only, outgoing-only, fully indexed, or unindexed), and how many context annotations and universal contexts were produced.

Lotus implementation

Public API

include/CFL/Classical/Solvers/Engines/CAT/ContextAwareTabulation.h

Algorithm

lib/CFL/Classical/Solvers/Engines/CAT/ContextAwareTabulation.cpp

Integration

SolverBackend::Cat in SolverSession and --solver cat in the classical, alias, and value-flow drivers.

The engine shares the common input types (Grammar, Graph, Query, Limits) and the compressed Reachability result with the Skewed and IEOCE engines. Result additionally exposes the working grammar, the grammar analysis, the applied transformation, and the optional static-skewing rewrites. RebuildingSession wraps solve for incremental terminal-edge additions; base-graph changes invalidate the offline context annotations and rebuild rather than reuse a stale context.

Validation

The Classical CFL tests compare the complete labeled relation of Cat with the SparseSet baseline and exercise incremental additions. A focused test covers usage-context pruning of adjacency.

IEOCE: Iterative-Epoch Online Cycle Elimination

Paper

The engine implements Xu et al., OOPSLA 2024 (DOI 10.1145/3649862), covering Sections 4-5 and Algorithms 2-5 of the paper.

Problem and key idea

The engine eliminates cycles online while solving. checkTransitiveSymbol and findTransitiveSymbols identify the transitive symbols of a grammar according to Definitions 4.1-4.6, checked against all requested nonterminals rather than only the start symbol. TransitivityCheck reports whether a symbol is eligible, whether it is doubly recursive, and its nonabsorbing targets and intransitive combinations.

solve then runs iterative epochs. Each epoch collapses strongly connected components into quotient nodes, replays the quotient facts, and continues until no further collapse is possible. The IeaOcr variant additionally maintains a minimum-equivalent graph (MEG) and removes redundant edges from it. Stats record the quotient nodes, epochs, SCC passes, collapsed components, merged nodes, quotient replays, MEG insertions and removals, and whether the run fell back to ordinary tabulation.

Options selects the Direction (directed or bidirected) and the Variant (Iea or IeaOcr). Bidirected mode requires a total involution and a syntactically reverse-closed grammar; solve additionally verifies reverse closure of the terminal input edges. An explicit transitive_symbol may be requested; an empty selection deterministically chooses the first admissible symbol, preferring an A A rule for IeaOcr. Requesting an unsafe symbol is an error. Generic grammars may have no collapsible relation; unless require_optimization is set, solve then performs exact ordinary tabulation and reports the fallback. trace_epochs records per-epoch statistics, and check_invariants runs expensive diagnostic checks on quotient canonicalization and, for IeaOcr, on MEG reachability and post-collapse minimality.

Lotus implementation

Public API

include/CFL/Classical/Solvers/Engines/IEOCE/IterativeEpoch.h

Algorithm

lib/CFL/Classical/Solvers/Engines/IEOCE/IterativeEpoch.cpp

Integration

SolverBackend::Iea and SolverBackend::IeaOcr in SolverSession and --solver iea / --solver iea-ocr in the classical, alias, and value-flow drivers.

The engine shares the common input types and the compressed Reachability result with the Skewed and CAT engines. Result additionally exposes the selected transitive symbol, the admissible symbols, and the per-epoch trace. RebuildingSession wraps solve for incremental terminal-edge additions; base-graph changes invalidate the quotient graph and rebuild rather than reuse a stale partition.

Validation

The Classical CFL tests compare the complete labeled relation of Iea and IeaOcr with the SparseSet baseline and exercise incremental additions. Focused tests cover cycle contraction for both variants, the IeaOcr MEG insertions, and the compressed storage of contracted results.

See also

Classical Grammar-Driven CFL Reachability documents the shared SolverSession backends, the common relation interface, and the command-line drivers.