Replaced merc_ldd by the LDD implementation using oxidd

[mlaveaux]

I have implemented a prototype in the ldd-nodes branch of oxidd that contains the recursive algorithms that are currently being used, and have replaced all references to merc_ldd by their corresponding oxidd implementation. Preliminary results show that the sequential version is about 40 percent faster for the WMS.lps example (from 22 to 15 seconds). The oxidd side still needs to be documentation and made nicer, and the parallel variants should be implemented in the near future.

Furthermore, this should be extensively tested before accepting the pull request.

[Copilot]

Pull request overview

This PR migrates MERC’s symbolic LDD-based functionality away from the in-repo merc_ldd crate to the oxidd LDD implementation, updating tools and the merc_symbolic crate accordingly and removing merc_ldd from the workspace.

Changes:

• Replaced merc_ldd::{Storage, Ldd, ...} usage with oxidd::ldd::{LDDManagerRef, LDDFunction, ...} across tools and crates/symbolic.
• Added new LDD utilities in crates/symbolic (LDD iterators, display, Sylvan/BLF I/O, helper functions like height / element_of) implemented on top of oxidd.
• Removed the merc_ldd crate from the workspace and pinned a fork of oxidd via [patch.crates-io] to access the prototype LDD branch.

Reviewed changes

Copilot reviewed 38 out of 40 changed files in this pull request and generated 5 comments.

Show a summary per file

File	Description
tools/sym/src/main.rs	Switch tool’s LDD manager initialization + state counting to oxidd LDD.
tools/sym/Cargo.toml	Drops merc_ldd dependency (keeps direct oxidd dependency).
tools/mcrl2/lps/src/main.rs	Adds oxidd LDD manager CLI knobs and uses oxidd in symbolic exploration path.
tools/mcrl2/lps/src/explore_symbolic.rs	Ports LPS symbolic exploration from merc_ldd to oxidd LDD operations/iterators.
tools/mcrl2/lps/Cargo.toml	Replaces merc_ldd with oxidd.
tools/mcrl2/Cargo.toml	Pins oxidd fork + adds [patch.crates-io] overrides in the mcrl2 tools workspace.
tools/mcrl2/Cargo.lock	Lockfile updates for oxidd fork and dependency graph changes.
tools/lts/Cargo.toml	Removes merc_ldd dependency.
crates/symbolic/src/util.rs	Adds oxidd-LDD versions of height and element_of; adapts BDD node creation signature.
crates/symbolic/src/symbolic_quotient.rs	Switches Value import to oxidd LDD Value.
crates/symbolic/src/symbolic_lts.rs	Migrates SymbolicLts and SummandGroup to LDDFunction + oxidd meta construction.
crates/symbolic/src/symbolic_lts_bdd.rs	Updates LDD→BDD conversion pipeline to accept LDDManagerRef + oxidd LDD ops.
crates/symbolic/src/sigref.rs	Updates tests/utilities to use oxidd LDD manager instead of merc_ldd::Storage.
crates/symbolic/src/reachability.rs	Ports reachability algorithm to oxidd LDD operations (union/minus/relprod).
crates/symbolic/src/reachability_bdd.rs	Updates tests to use oxidd LDD manager and LDDFunction::len().
crates/symbolic/src/random_vector_set.rs	Reimplements random LDD construction/printing on oxidd LDD.
crates/symbolic/src/random_symbolic_lts.rs	Updates random symbolic LTS generation to use oxidd LDD manager + new helpers.
crates/symbolic/src/lib.rs	Exposes new modules (LDD cube iterator, display, I/O, test helpers) after migration.
crates/symbolic/src/ldd_to_bdd.rs	Ports LDD↔BDD conversion internals to oxidd LDD node access and operations.
crates/symbolic/src/io_symbolic_lts.rs	Switches symbolic .sym reading to oxidd-backed BinaryLddReader.
crates/symbolic/src/io_sylvan.rs	Ports Sylvan .ldd reading and adds new oxidd-backed SylvanReader.
crates/symbolic/src/io_ldd.rs	Ports BLF (binary LDD) read/write to oxidd LDD functions and new iterators.
crates/symbolic/src/display.rs	Ports LDD DOT/text display to oxidd LDD iterators and IDs.
crates/symbolic/src/cube_iter_ldd.rs	Adds oxidd-LDD cube/node iterators (iter, iter_right, iter_nodes).
crates/symbolic/Cargo.toml	Removes merc_ldd, adds needed oxidd-* + merc_number / delegate.
Cargo.toml	Removes crates/ldd members/deps and pins oxidd fork via [patch.crates-io].
Cargo.lock	Lockfile updates reflecting removal of merc_ldd and use of the oxidd fork.
crates/ldd/src/storage/ldd.rs	Deleted (part of removing merc_ldd).
crates/ldd/src/storage/cache.rs	Deleted (part of removing merc_ldd).
crates/ldd/src/storage.rs	Deleted (part of removing merc_ldd).
crates/ldd/src/operations.rs	Deleted (part of removing merc_ldd).
crates/ldd/src/lib.rs	Deleted (part of removing merc_ldd).
crates/ldd/src/iterators.rs	Deleted (part of removing merc_ldd).
crates/ldd/src/io_sylvan.rs	Deleted (part of removing merc_ldd).
crates/ldd/README.md	Deleted (part of removing merc_ldd).
crates/ldd/Cargo.toml	Deleted (part of removing merc_ldd).
crates/ldd/benchmarks/Cargo.toml	Deleted (part of removing merc_ldd benchmarks).
crates/ldd/benchmarks/benches/benchmarks_ldd.rs	Deleted (part of removing merc_ldd benchmarks).

Comments suppressed due to low confidence (2)

crates/symbolic/src/display.rs:84

• print_node never inserts the current node into marked, so the duplicate-detection guard is ineffective. For shared subgraphs this can cause repeated output (and can get extremely large), defeating the purpose of marked.
  crates/symbolic/src/ldd_to_bdd.rs:91
• ldd_to_bdd_edge panics when bit_variables is shorter than needed_bits. Since this is a library function returning Result, prefer returning an error (or at least debug_assert!) so callers can't crash the process with a mismatched input configuration.

    // Ensure we have enough variables for this layer
    let needed_bits = bits_value as usize;
    if bit_variables.len() < needed_bits {
        panic!(
            "Insufficient variables: need {needed_bits}, have {} for current layer",
            bit_variables.len()
        );
    }

---

💡 Add Copilot custom instructions for smarter, more guided reviews. Learn how to get started.