Dynamic Bidirected Dyck Reachability ==================================== The module provides two independent algorithms: the POPL 2022 ``WeightedQuotientSolver`` and the POPL 2024 ``PrimaryComponentSolver`` described below. Both link through ``CanaryDynamicDyck`` and are driven by the same ``lotus-cfl-dynamic-dyck`` CLI. ``WeightedQuotientSolver`` directly ports the C++ dynamic algorithms from Li, Satya, and Zhang's `Efficient Algorithms for Dynamic Bidirected Dyck-Reachability `_ (POPL 2022). **Headers**: ``include/CFL/DynamicDyck/`` **Implementation**: ``lib/CFL/DynamicDyck/`` **Namespace**: ``lotus::cfl::dynamic_dyck`` Shared graph, file IO, and statistics headers live at the module root. The public solver headers live in their respective algorithm directories: ``WeightedQuotient/WeightedQuotientSolver.h`` and ``PrimaryComponent/PrimaryComponentSolver.h``. Their source files have the same relative paths under ``lib/CFL/DynamicDyck/``, with a ``.cpp`` extension. Shared ``Graph.cpp`` and the file-workflow adapter ``IO.cpp`` live at the implementation root. Each algorithm owns its sources and CMake source list: ``WeightedQuotient/`` contains the POPL 2022 solver, weighted engine, cycle-deletion correction and artifact DOT parser; ``PrimaryComponent/`` contains the primary-component solver and its two connectivity backends. Internal headers mirror those directories and use the ``weighted_quotient`` and ``primary_component`` namespaces. The ``CanaryDynamicDyck`` target builds both algorithms; template/container support is header-only. The POPL 2022 solver is built from degree-based merging, fully compressed disjoint sets, indexed linked worklists, weighted quotient updates, and acyclic recursive splitting. All mutable state belongs to a solver instance; preprocessing state is reset after every update, so duplicate insertions and missing deletions keep degree accounting correct and invalid arrow records are rejected. The `2024 cycle correction `_ motivates a conservative deletion fallback: if the affected quotient contains cycles, preprocess the remaining graph again. No original-paper update-time bound is claimed. Library API ----------- ``WeightedQuotientSolver`` supports ``addVertex``, ``insertEdge``, ``deleteEdge``, ``apply``, ``connected``, ``representative``, ``components``, ``graph``, and ``statistics``. Each edge denotes an opening arc and its closing reverse; updates operate on the pair. Duplicate insertion and absent deletion are no-ops. Numeric vertex IDs are signed 64-bit integers; labels are unsigned integers. Insertion creates endpoints; deletion does not. Queries involving unknown vertices return false. Concurrent access requires synchronization because representative queries compress paths. .. code-block:: cpp #include "CFL/DynamicDyck/WeightedQuotient/WeightedQuotientSolver.h" using namespace lotus::cfl::dynamic_dyck; WeightedQuotientSolver solver; solver.insertEdge({10, 30, 0}); solver.insertEdge({20, 30, 0}); assert(solver.connected(10, 20)); solver.deleteEdge({30, 20, 0, Parenthesis::Close}); assert(!solver.connected(10, 20)); ``IO.h`` exposes ``runFiles`` for the opaque string-ID workflow, returning timing results and final partitions. ``Graph.h`` offers stricter numeric convenience parsers separately. Only one Dyck language is supported; neutral and interleaved bracket constraints are outside this module. POPL 2024 algorithm ------------------- ``PrimaryComponentSolver.h`` provides DynamicAlgo from Krishna, Lal, Pavlogiannis and Tuppe, *On-the-Fly Static Analysis via Dynamic Bidirected Dyck Reachability* (POPL 2024). This implementation was integrated from the user-supplied ``lotus-dynamic-dyck-popl24-v2`` package; it is not an official authors' artifact. It maintains DSCCs, primary components, edge counts and sparse summaries. Deletion refines affected components and re-saturates summaries without a whole-input Dyck-reachability rebuild. The default edge convention is **reference counted**, unlike ``WeightedQuotientSolver``. Each insertion, including a complementary reverse record, adds one reference; deletion removes one reference. Choose ``PrimaryComponentEdgeSemantics::Set`` to match ``WeightedQuotientSolver``'s duplicate and deletion behavior. Both conventions create missing endpoints on insertion and retain vertices after deletion. ``graph()`` exports unique opening pairs; use ``edgeCounts()`` to retain counts. .. code-block:: cpp #include "CFL/DynamicDyck/PrimaryComponent/PrimaryComponentSolver.h" using namespace lotus::cfl::dynamic_dyck; PrimaryComponentSolver solver(PrimaryComponentEdgeSemantics::Set); solver.insertEdge({10, 30, 7}); solver.insertEdge({20, 30, 7}); auto first = solver.vertexIndex(10); auto second = solver.vertexIndex(20); assert(solver.connectedByIndex(first, second)); solver.deleteEdge({30, 20, 7, Parenthesis::Close}); assert(!solver.connectedByIndex(first, second)); The default ``Deterministic`` connectivity backend uses a strong-certificate hierarchy. The package's implementation-level complexity argument gives O(n alpha(n)) worst-case update work for a constant alphabet in its stated RAM model; this is not a machine-checked proof or hard-real-time guarantee. It is not the exact Eppstein backend from the paper. Select ``PrimaryComponentConnectivityBackend::HDT`` as the practical alternative, with different amortized/treap cost qualifications. Neither backend is claimed uniformly faster. External-ID queries require O(log n) lookup; stable dense-index queries are O(1) with the deterministic backend. Graph construction inserts edges individually, not through an optimal bulk initializer. Unknown-ID connectivity queries return false; representative and index lookups throw for unknown vertices. Instances are independent, movable and noncopyable; access to one instance requires synchronization. Interrupted mutations fail closed: subsequent queries throw, and the instance must be replaced. There is no transactional rollback. ``validate()`` is an expensive debug check. The supplied implementation package documents its algorithm mapping, complexity qualifications, provenance and MIT license. .. code-block:: bash cmake --build build --target lotus-cfl-dynamic-dyck cfl_tests build/bin/lotus-cfl-dynamic-dyck --algorithm primary-component --stats initial.dot updates.seq build/bin/lotus-cfl-dynamic-dyck --algorithm primary-component --backend hdt --counted \ --print-components initial.dot updates.seq ctest --test-dir build -R 'cfl_tests.PrimaryComponent' --output-on-failure The existing CLI exposes POPL 2024 with ``--algorithm primary-component`` and accepts the same opaque node IDs and type suffixes. It defaults to **set semantics** for compatibility; ``--counted`` enables reference counts. ``--backend`` selects ``deterministic`` (default) or ``hdt``. Sequence endpoints are preallocated and timing covers update calls only, excluding parsing and initial saturation. The default output is the timing-only format consumed by the table scripts; ``--stats`` identifies the selected algorithm, backend and semantics. POPL 2024 rejects ``0``/``--recompute``. Omitting ``--algorithm`` selects the POPL 2022 solver and its modes; POPL 2024 is exposed by the same executable, with no separate tool. Tests include a Boolean Dyck-grammar oracle, primary-connectivity BFS, pre-fixpoint phase invariants, allocation failures, parser checks and set-mode comparisons against ``WeightedQuotientSolver``. Instrumented phase hooks are compiled into a separate test-only library, never the production target. Benchmark workflow ------------------ .. code-block:: bash cmake --build build --target lotus-cfl-dynamic-dyck dynamic_dyck_test build/bin/lotus-cfl-dynamic-dyck 1 initial.dot updates.seq build/bin/lotus-cfl-dynamic-dyck 0 initial.dot updates.seq ctest --test-dir build -R dynamic_dyck --output-on-failure ``0`` selects recomputation after every input record, including no-ops; ``1`` selects dynamic updates. The CLI accepts original ``SOURCE->TARGET[label="op--TYPE"]`` / ``cp--TYPE`` graph records and ``A|D SOURCE TARGET LABEL`` sequence records, interning names and suffixes as strings. Default stdout is one elapsed-seconds value and a trailing space, with no newline, matching the table scripts. Timing measures update calls only, excluding parsing and initial saturation; ``--stats`` and ``--print-components`` add diagnostics. Run the table scripts directly; paths are resolved relative to the repository, with ``DYCK_REACH_BINARY`` and ``DYCK_BENCHMARK_ROOT`` overrides: .. code-block:: bash bash scripts/cfl/dynamic-dyck/gen_table3.sh bash scripts/cfl/dynamic-dyck/gen_table4.sh The C++ benchmark inputs live in ``benchmarks/real-world/CFL/DynamicDyck`` and the scripts in ``scripts/cfl/dynamic-dyck``. The optional ``run_benchmarks.py`` runner in ``benchmarks/real-world/CFL/DynamicDyck/`` supports case selection, dry-run input validation, and partition comparison without changing the table ordering; ``--binary`` selects another build. The DDlog encoding is not accepted by this CLI.