diff --git a/Cargo.lock b/Cargo.lock index df83e7441..b4bee37a6 100644 --- a/Cargo.lock +++ b/Cargo.lock @@ -125,8 +125,7 @@ checksum = "7f202df86484c868dbad7eaa557ef785d5c66295e41b460ef922eca0723b842c" [[package]] name = "arcslab" version = "0.1.2" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "67d525761a6913dc2115b17c9c72379de20e9fd7b12ad479bbadbb544b20b32b" +source = "git+https://github.com/mlaveaux/oxidd?rev=4ed048be1f064f6dc4497a396204de35e4c1568b#4ed048be1f064f6dc4497a396204de35e4c1568b" dependencies = [ "crossbeam-utils", "derive-where", @@ -165,15 +164,6 @@ dependencies = [ "merc_aterm", ] -[[package]] -name = "benchmarks_ldd" -version = "2.0.0" -dependencies = [ - "criterion", - "merc_ldd", - "rand", -] - [[package]] name = "benchmarks_sabre" version = "2.0.0" @@ -623,9 +613,9 @@ checksum = "1d674e81391d1e1ab681a28d99df07927c6d4aa5b027d7da16ba32d1d21ecd99" [[package]] name = "flume" -version = "0.11.1" +version = "0.12.0" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "da0e4dd2a88388a1f4ccc7c9ce104604dab68d9f408dc34cd45823d5a9069095" +checksum = "5e139bc46ca777eb5efaf62df0ab8cc5fd400866427e56c68b22e414e53bd3be" dependencies = [ "spin", ] @@ -760,8 +750,7 @@ dependencies = [ [[package]] name = "hugealloc" version = "0.1.1" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "542733215a252c27c674e5d875a910d7de509cb74123d0bdbaa050f871ec84c2" +source = "git+https://github.com/mlaveaux/oxidd?rev=4ed048be1f064f6dc4497a396204de35e4c1568b#4ed048be1f064f6dc4497a396204de35e4c1568b" dependencies = [ "allocator-api2 0.2.21", "libc", @@ -905,8 +894,7 @@ dependencies = [ [[package]] name = "linear-hashtbl" version = "0.1.4" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "b11269ceb6867559e0fce487ff8148933040c7ac091ee4ecc904821f1db1e0fa" +source = "git+https://github.com/mlaveaux/oxidd?rev=4ed048be1f064f6dc4497a396204de35e4c1568b#4ed048be1f064f6dc4497a396204de35e4c1568b" [[package]] name = "linux-raw-sys" @@ -975,7 +963,6 @@ dependencies = [ "merc_collections", "merc_explore", "merc_io", - "merc_ldd", "merc_lts", "merc_reduction", "merc_refinement", @@ -1013,7 +1000,6 @@ dependencies = [ "itertools 0.14.0", "log", "merc_io", - "merc_ldd", "merc_lts", "merc_symbolic", "merc_tools", @@ -1131,25 +1117,6 @@ dependencies = [ "thiserror", ] -[[package]] -name = "merc_ldd" -version = "3.0.0" -dependencies = [ - "ahash", - "delegate", - "itertools 0.14.0", - "log", - "merc_aterm", - "merc_collections", - "merc_io", - "merc_number", - "merc_unsafety", - "merc_utilities", - "rand", - "rustc-hash 2.1.2", - "streaming-iterator", -] - [[package]] name = "merc_lts" version = "2.0.0" @@ -1309,6 +1276,7 @@ name = "merc_symbolic" version = "3.0.0" dependencies = [ "clap", + "delegate", "duct", "itertools 0.14.0", "log", @@ -1316,8 +1284,8 @@ dependencies = [ "merc_collections", "merc_data", "merc_io", - "merc_ldd", "merc_lts", + "merc_number", "merc_reduction", "merc_utilities", "oxidd", @@ -1325,6 +1293,7 @@ dependencies = [ "oxidd-dump", "oxidd-reorder", "oxidd-rules-bdd", + "oxidd-rules-ldd", "rand", "rustc-hash 2.1.2", "streaming-iterator", @@ -1588,8 +1557,7 @@ dependencies = [ [[package]] name = "oxidd" version = "0.11.0" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "c984e2c820ff1306f7bd10ac166a542c69cce2d87331eb4caa1b78ca381e5c0b" +source = "git+https://github.com/mlaveaux/oxidd?rev=4ed048be1f064f6dc4497a396204de35e4c1568b#4ed048be1f064f6dc4497a396204de35e4c1568b" dependencies = [ "cfg-if", "derive-where", @@ -1602,6 +1570,7 @@ dependencies = [ "oxidd-manager-pointer", "oxidd-reorder", "oxidd-rules-bdd", + "oxidd-rules-ldd", "oxidd-rules-mtbdd", "oxidd-rules-tdd", "oxidd-rules-zbdd", @@ -1611,8 +1580,7 @@ dependencies = [ [[package]] name = "oxidd-cache" version = "0.11.1" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "ea87b04767bd71ec9a0f0f1b95b3e1be822365d611ae692734bf84dffdc1aae9" +source = "git+https://github.com/mlaveaux/oxidd?rev=4ed048be1f064f6dc4497a396204de35e4c1568b#4ed048be1f064f6dc4497a396204de35e4c1568b" dependencies = [ "allocator-api2 0.2.21", "document-features", @@ -1624,8 +1592,7 @@ dependencies = [ [[package]] name = "oxidd-core" version = "0.11.0" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "c4ce8a17e276f5df5a9a2aabdc0fd1ccf2b3b73bc3b5ef7627f26f6ecc9afee3" +source = "git+https://github.com/mlaveaux/oxidd?rev=4ed048be1f064f6dc4497a396204de35e4c1568b#4ed048be1f064f6dc4497a396204de35e4c1568b" dependencies = [ "nanorand", ] @@ -1633,8 +1600,7 @@ dependencies = [ [[package]] name = "oxidd-derive" version = "0.11.0" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "96cb7e36aee287b5ad1921fb98050a1b9e5771bf5d34381f24b0548083aefeb3" +source = "git+https://github.com/mlaveaux/oxidd?rev=4ed048be1f064f6dc4497a396204de35e4c1568b#4ed048be1f064f6dc4497a396204de35e4c1568b" dependencies = [ "proc-macro-error", "proc-macro2", @@ -1645,8 +1611,7 @@ dependencies = [ [[package]] name = "oxidd-dump" version = "0.6.0" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "675fcc8144350309a3b94a4a3522d953472c29df06b783fe0dfafbc6b1d39b4b" +source = "git+https://github.com/mlaveaux/oxidd?rev=4ed048be1f064f6dc4497a396204de35e4c1568b#4ed048be1f064f6dc4497a396204de35e4c1568b" dependencies = [ "document-features", "fixedbitset 0.5.7", @@ -1660,8 +1625,7 @@ dependencies = [ [[package]] name = "oxidd-manager-index" version = "0.11.0" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "e1339eb2952e23d62d3421f444fdf36d7f36b6a63707ae3d4fef1d1bfb007a47" +source = "git+https://github.com/mlaveaux/oxidd?rev=4ed048be1f064f6dc4497a396204de35e4c1568b#4ed048be1f064f6dc4497a396204de35e4c1568b" dependencies = [ "crossbeam-utils", "derive-where", @@ -1676,8 +1640,7 @@ dependencies = [ [[package]] name = "oxidd-manager-pointer" version = "0.6.0" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "ad78ecc8d113d3e3a2d06a47299d8a557088f016323f0f22f363622ff239ebb8" +source = "git+https://github.com/mlaveaux/oxidd?rev=4ed048be1f064f6dc4497a396204de35e4c1568b#4ed048be1f064f6dc4497a396204de35e4c1568b" dependencies = [ "arcslab", "derive-where", @@ -1693,8 +1656,7 @@ dependencies = [ [[package]] name = "oxidd-reorder" version = "0.6.1" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "6863dd156fb2713ad1f6b7528d08da3cc675ae27e24b6e9a0df9d0fea8d9a839" +source = "git+https://github.com/mlaveaux/oxidd?rev=4ed048be1f064f6dc4497a396204de35e4c1568b#4ed048be1f064f6dc4497a396204de35e4c1568b" dependencies = [ "flume", "is_sorted", @@ -1706,8 +1668,7 @@ dependencies = [ [[package]] name = "oxidd-rules-bdd" version = "0.11.0" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "c56b5465552bdc2c1f38c433f8751703d1561396f4be16315999cc47eed6e2ce" +source = "git+https://github.com/mlaveaux/oxidd?rev=4ed048be1f064f6dc4497a396204de35e4c1568b#4ed048be1f064f6dc4497a396204de35e4c1568b" dependencies = [ "document-features", "fixedbitset 0.5.7", @@ -1716,11 +1677,19 @@ dependencies = [ "oxidd-dump", ] +[[package]] +name = "oxidd-rules-ldd" +version = "0.11.0" +source = "git+https://github.com/mlaveaux/oxidd?rev=4ed048be1f064f6dc4497a396204de35e4c1568b#4ed048be1f064f6dc4497a396204de35e4c1568b" +dependencies = [ + "oxidd-core", + "oxidd-derive", +] + [[package]] name = "oxidd-rules-mtbdd" version = "0.6.0" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "49740035de417b58fad2fe420b5539081604e601c266841f3092ca8bb5db1da7" +source = "git+https://github.com/mlaveaux/oxidd?rev=4ed048be1f064f6dc4497a396204de35e4c1568b#4ed048be1f064f6dc4497a396204de35e4c1568b" dependencies = [ "document-features", "fixedbitset 0.5.7", @@ -1732,8 +1701,7 @@ dependencies = [ [[package]] name = "oxidd-rules-tdd" version = "0.6.0" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "eb13c585037127f6066e3ca928e96bdc21df19a41b0242dfcb9e95faf723558c" +source = "git+https://github.com/mlaveaux/oxidd?rev=4ed048be1f064f6dc4497a396204de35e4c1568b#4ed048be1f064f6dc4497a396204de35e4c1568b" dependencies = [ "document-features", "oxidd-core", @@ -1744,8 +1712,7 @@ dependencies = [ [[package]] name = "oxidd-rules-zbdd" version = "0.11.0" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "917c941a721e884817a5b510ff818cb6d7033216817c0fd1e0b154f4cc7cfe5b" +source = "git+https://github.com/mlaveaux/oxidd?rev=4ed048be1f064f6dc4497a396204de35e4c1568b#4ed048be1f064f6dc4497a396204de35e4c1568b" dependencies = [ "document-features", "fixedbitset 0.5.7", diff --git a/Cargo.toml b/Cargo.toml index a4d8efbeb..ede114d94 100644 --- a/Cargo.toml +++ b/Cargo.toml @@ -25,8 +25,6 @@ members = [ "crates/data", "crates/explore", "crates/io", - "crates/ldd", - "crates/ldd/benchmarks", "crates/lts", "crates/macros", "crates/number", @@ -66,10 +64,11 @@ itertools = "0.14" log = { version = "0.4", features = ["kv"] } num = "0.4" oxidd = { version = "0.11", features = ["manager-pointer"] } -oxidd-core = "0.11" oxidd-dump = "0.6" +oxidd-core = "0.11" oxidd-reorder = "0.6" oxidd-rules-bdd = "0.11" +oxidd-rules-ldd = "0.11" parking_lot = "0.12" pest = "2.8" pest_derive = "2.8" @@ -123,7 +122,6 @@ merc_collections = { version = "2.0", path = "crates/collections" } merc_data = { version = "2.0", path = "crates/data" } merc_explore = { version = "0.1.0", path = "crates/explore" } merc_io = { version = "2.0", path = "crates/io" } -merc_ldd = { version = "3.0", path = "crates/ldd" } merc_lts = { version = "2.0", path = "crates/lts" } merc_macros = { version = "2.0", path = "crates/macros" } merc_number = { version = "2.0", path = "crates/number" } @@ -145,4 +143,14 @@ merc_pest_consume_macros = { version = "2.0", git = "https://github.com/MERCorg/ [workspace.metadata.cargo-semver-checks.lints] enum_no_repr_variant_discriminant_changed = "allow" -partial_ord_enum_variants_reordered = "allow" \ No newline at end of file +partial_ord_enum_variants_reordered = "allow" + + +# Use a fork of oxidd until the LDD branch is integrated. +[patch.crates-io] +oxidd = { git = "https://github.com/mlaveaux/oxidd", rev = "4ed048be1f064f6dc4497a396204de35e4c1568b" } +oxidd-core = { git = "https://github.com/mlaveaux/oxidd", rev = "4ed048be1f064f6dc4497a396204de35e4c1568b" } +oxidd-dump = { git = "https://github.com/mlaveaux/oxidd", rev = "4ed048be1f064f6dc4497a396204de35e4c1568b" } +oxidd-reorder = { git = "https://github.com/mlaveaux/oxidd", rev = "4ed048be1f064f6dc4497a396204de35e4c1568b" } +oxidd-rules-bdd = { git = "https://github.com/mlaveaux/oxidd", rev = "4ed048be1f064f6dc4497a396204de35e4c1568b" } +oxidd-rules-ldd = { git = "https://github.com/mlaveaux/oxidd", rev = "4ed048be1f064f6dc4497a396204de35e4c1568b" } \ No newline at end of file diff --git a/crates/ldd/Cargo.toml b/crates/ldd/Cargo.toml deleted file mode 100644 index 2b8adcebd..000000000 --- a/crates/ldd/Cargo.toml +++ /dev/null @@ -1,30 +0,0 @@ -[package] -name = "merc_ldd" -description = "Implements algorithms and I/O for list decision diagrams." -keywords = ["automata", "transition-systems"] -categories = ["data-structures", "science"] -readme = "README.md" -version = "3.0.0" - -edition.workspace = true -homepage.workspace = true -license.workspace = true -repository.workspace = true -rust-version.workspace = true - - -[dependencies] -merc_aterm.workspace = true -merc_collections.workspace = true -merc_io.workspace = true -merc_number.workspace = true -merc_unsafety.workspace = true -merc_utilities.workspace = true - -ahash.workspace = true -delegate.workspace = true -itertools.workspace = true -log.workspace = true -rand.workspace = true -rustc-hash.workspace = true -streaming-iterator.workspace = true \ No newline at end of file diff --git a/crates/ldd/README.md b/crates/ldd/README.md deleted file mode 100644 index 9a22806b3..000000000 --- a/crates/ldd/README.md +++ /dev/null @@ -1,47 +0,0 @@ - # Overview - -A library to create and manipulate so called list decision diagrams, -abbreviated as LDDs. List decision diagrams are data structures that can -efficiently represent sets of vectors containing natural numbers \[Dijk18\]. - -An LDD is inductively defined as follows. First of all, constants 'true' and -'false' are two distinct LDDs. Given LDDs x and y, then node(value, x, y) is -an LDD; where value is a natural number. As such, we observe that node(5, -true, node(4, true, false)) is an LDD and in general we obtain a tree-like -data structure. - -Next, we should explain how LDDs represent a set of vectors. Given an LDD n -then \[n\] is inductively defined as: - -```plain - [false] = ∅ - [true] = { <> } - [node(value, down, right)] = { value x | x in [down] } ∪ [right]\ -``` - -Note that since 'true' and 'false' are not very insightful and clash with -Rust keywords we use 'empty vector' and 'empty set' for the constants 'true' -and 'false' respectively. - -## Changelog - -### 3.0.0 - -Added caching for the projection operation, which is used for state space -exploration. - -## Citations - -> \[Dijk18\] --- Tom van Dijk, Jaco van de Pol. Sylvan: multi-core framework for decision diagrams. International Journal on Software Tools for Technology Transfer. 19(6):675-696, 2017. - -## Safety - -This crate contains no `unsafe` code. - -## Minimum Supported Rust Version - -We do not maintain an official minimum supported rust version (MSRV), and it may be upgraded at any time when necessary. - -## License - -All MERC crates are licensed under the `BSL-1.0` license. See the [LICENSE](https://raw.githubusercontent.com/MERCorg/merc/refs/heads/main/LICENSE) file in the repository root for more information. \ No newline at end of file diff --git a/crates/ldd/benchmarks/Cargo.toml b/crates/ldd/benchmarks/Cargo.toml deleted file mode 100644 index 3d46ad2ae..000000000 --- a/crates/ldd/benchmarks/Cargo.toml +++ /dev/null @@ -1,18 +0,0 @@ -[package] -name = "benchmarks_ldd" -version.workspace = true -edition.workspace = true -license.workspace = true -rust-version.workspace = true - -# See more keys and their definitions at https://doc.rust-lang.org/cargo/reference/manifest.html - -[dependencies] -merc_ldd.workspace = true - -criterion.workspace = true -rand.workspace = true - -[[bench]] -name = "benchmarks_ldd" -harness = false \ No newline at end of file diff --git a/crates/ldd/benchmarks/benches/benchmarks_ldd.rs b/crates/ldd/benchmarks/benches/benchmarks_ldd.rs deleted file mode 100644 index 9e85b5b18..000000000 --- a/crates/ldd/benchmarks/benches/benchmarks_ldd.rs +++ /dev/null @@ -1,117 +0,0 @@ -use std::collections::HashSet; -use std::hint::black_box; - -use criterion::Criterion; -use criterion::criterion_group; -use criterion::criterion_main; -use rand::Rng; -use rand::RngExt; -use rand::prelude::IteratorRandom; - -use merc_ldd::Ldd; -use merc_ldd::Storage; -use merc_ldd::Value; -use merc_ldd::compute_meta; -use merc_ldd::minus; -use merc_ldd::relational_product; -use merc_ldd::singleton; -use merc_ldd::union; - -/// Returns a vector of the given length with random u64 values (from 0..max_value). -pub fn random_vector(rng: &mut R, length: usize, max_value: Value) -> Vec { - let mut vector: Vec = Vec::new(); - for _ in 0..length { - vector.push(rng.random_range(0..max_value)); - } - - vector -} - -/// Returns a sorted vector of the given length with unique u64 values (from 0..max_value). -pub fn random_sorted_vector(rng: &mut R, length: usize, max_value: Value) -> Vec { - let mut result = (0..max_value).sample(rng, length); - result.sort(); - result -} - -/// Returns a set of 'amount' vectors where every vector has the given length. -pub fn random_vector_set(rng: &mut R, amount: usize, length: usize, max_value: Value) -> HashSet> { - let mut result: HashSet> = HashSet::new(); - - // Insert 'amount' number of vectors into the result. - for _ in 0..amount { - result.insert(random_vector(rng, length, max_value)); - } - - result -} - -/// Returns an LDD containing all elements of the given iterator over vectors. -pub fn from_iter<'a, I>(storage: &mut Storage, iter: I) -> Ldd -where - I: Iterator>, -{ - let mut result = storage.empty_set().clone(); - - for vector in iter { - let single = singleton(storage, vector); - result = union(storage, &result, &single); - } - - result -} - -pub fn criterion_benchmark(c: &mut Criterion) { - let mut rng = rand::rng(); - - c.bench_function("union 1000", |bencher| { - let mut storage = Storage::new(); - - bencher.iter(|| { - let set_a = random_vector_set(&mut rng, 1000, 10, 10); - let set_b = random_vector_set(&mut rng, 1000, 10, 10); - - let a = from_iter(&mut storage, set_a.iter()); - let b = from_iter(&mut storage, set_b.iter()); - - black_box(union(&mut storage, &a, &b)); - }) - }); - - c.bench_function("minus 1000", |bencher| { - let mut storage = Storage::new(); - - bencher.iter(|| { - let set_a = random_vector_set(&mut rng, 1000, 10, 10); - let set_b = random_vector_set(&mut rng, 1000, 10, 10); - - let a = from_iter(&mut storage, set_a.iter()); - let b = from_iter(&mut storage, set_b.iter()); - - black_box(minus(&mut storage, &a, &b)); - }) - }); - - c.bench_function("relational_product 1000", |bencher| { - let mut storage = Storage::new(); - - bencher.iter(|| { - let set = random_vector_set(&mut rng, 1000, 10, 10); - let relation = random_vector_set(&mut rng, 32, 4, 10); - - // Pick arbitrary read and write parameters in order. - let read_proj = random_sorted_vector(&mut rng, 2, 9); - let write_proj = random_sorted_vector(&mut rng, 2, 9); - - // Compute LDD result. - let ldd = from_iter(&mut storage, set.iter()); - let rel = from_iter(&mut storage, relation.iter()); - - let meta = compute_meta(&mut storage, &read_proj, &write_proj).0; - black_box(relational_product(&mut storage, &ldd, &rel, &meta)); - }) - }); -} - -criterion_group!(benches, criterion_benchmark); -criterion_main!(benches); diff --git a/crates/ldd/src/io_sylvan.rs b/crates/ldd/src/io_sylvan.rs deleted file mode 100644 index 5664dc784..000000000 --- a/crates/ldd/src/io_sylvan.rs +++ /dev/null @@ -1,95 +0,0 @@ -use std::collections::HashMap; -use std::io::Read; - -use merc_utilities::MercError; - -use crate::Ldd; -use crate::Storage; -use crate::Value; - -/// A reader for LDDs in the Sylvan .ldd format. -pub struct SylvanReader { - indexed_set: HashMap, // Assigns LDDs to every index. - last_index: u64, // The index of the last LDD read from file. -} - -impl SylvanReader { - pub fn new() -> Self { - Self { - indexed_set: HashMap::new(), - last_index: 2, - } - } - - /// Returns an LDD read from the given stream in the Sylvan format. - pub fn read_ldd(&mut self, storage: &mut Storage, stream: &mut R) -> Result { - let count = read_u64(stream)?; - //println!("node count = {}", count); - - for _ in 0..count { - // Read a single MDD node. It has the following structure: u64 | u64 - // RmRR RRRR RRRR VVVV | VVVV DcDD DDDD DDDD (little endian) - // Every character is 4 bits, V = value, D = down, R = right, m = marked, c = copy. - let a = read_u64(stream)?; - let b = read_u64(stream)?; - //println!("{:064b} | {:064b}", a, b); - - let right = (a & 0x0000ffffffffffff) >> 1; - let down = b >> 17; - - let mut bytes: [u8; 4] = Default::default(); - bytes[0..2].copy_from_slice(&a.to_le_bytes()[6..8]); - bytes[2..4].copy_from_slice(&b.to_le_bytes()[0..2]); - let value = u32::from_le_bytes(bytes); - - let copy = right & 0x10000; - if copy != 0 { - panic!("We do not yet deal with copy nodes."); - } - - let down = self.node_from_index(storage, down); - let right = self.node_from_index(storage, right); - - let ldd = storage.insert(value as Value, &down, &right); - self.indexed_set.insert(self.last_index, ldd); - - self.last_index += 1; - } - - let result = read_u64(stream)?; - Ok(self.node_from_index(storage, result)) - } - - /// Returns the LDD belonging to the given index. - fn node_from_index(&self, storage: &mut Storage, index: u64) -> Ldd { - if index == 0 { - storage.empty_set().clone() - } else if index == 1 { - storage.empty_vector().clone() - } else { - self.indexed_set.get(&index).unwrap().clone() - } - } -} - -impl Default for SylvanReader { - fn default() -> Self { - Self::new() - } -} - -/// Returns a single u32 read from the given stream. -pub fn read_u32(stream: &mut R) -> Result { - let mut buffer: [u8; 4] = Default::default(); - stream.read_exact(&mut buffer)?; - - Ok(u32::from_le_bytes(buffer)) -} - -/// Returns a single u64 read from the given stream. -pub fn read_u64(stream: &mut R) -> Result { - let mut buffer: [u8; 8] = Default::default(); - stream.read_exact(&mut buffer)?; - - Ok(u64::from_le_bytes(buffer)) -} diff --git a/crates/ldd/src/iterators.rs b/crates/ldd/src/iterators.rs deleted file mode 100644 index d782ea32d..000000000 --- a/crates/ldd/src/iterators.rs +++ /dev/null @@ -1,306 +0,0 @@ -use streaming_iterator::StreamingIterator; - -use crate::Data; -use crate::DataRef; -use crate::Ldd; -use crate::Storage; -use crate::Value; - -// Returns an iterator over all right siblings of the given LDD. -pub fn iter_right<'a>(storage: &'a Storage, ldd: &Ldd) -> IterRight<'a> { - IterRight { - storage, - current: ldd.clone(), - } -} - -// Returns an iterator over all vectors contained in the given LDD. -pub fn iter<'a>(storage: &'a Storage, ldd: &Ldd) -> Iter<'a> { - if ldd == storage.empty_vector() || ldd == storage.empty_set() { - Iter { - storage, - vector: Vec::new(), - current: Vec::new(), - stack: Vec::new(), - finished: false, - } - } else { - Iter { - storage, - vector: Vec::new(), - current: Vec::new(), - stack: vec![ldd.clone()], - finished: false, - } - } -} - -// Calls `f` with `&mut storage` and each vector in the LDD. Unlike `iter`, the closure receives a -// mutable storage reference so it can insert nodes without a separate collection step. -pub fn for_each_mut(storage: &mut Storage, ldd: &Ldd, mut f: F) -where - F: FnMut(&mut Storage, &[Value]), -{ - if ldd == storage.empty_vector() || ldd == storage.empty_set() { - return; - } - - let mut vector: Vec = Vec::new(); - let mut stack: Vec = vec![ldd.clone()]; - - loop { - // Descend to the next leaf (node whose down == empty_vector). - loop { - let (value, down) = { - let DataRef(value, down, _) = storage.get_ref(stack.last().unwrap()); - let is_leaf = down == *storage.empty_vector(); - let down_protected = (!is_leaf).then(|| storage.protect(&down)); - (value, down_protected) - }; - vector.push(value); - match down { - Some(down_ldd) => stack.push(down_ldd), - None => break, // reached leaf - } - } - - // Storage is no longer borrowed — the closure may mutate it freely. - f(storage, &vector); - - // Ascend to find the next right sibling. - while let Some(current) = stack.pop() { - vector.pop(); - let right = { - let DataRef(_, _, right) = storage.get_ref(¤t); - if right != *storage.empty_set() { - Some(storage.protect(&right)) - } else { - None - } - }; - if let Some(right_ldd) = right { - stack.push(right_ldd); - break; - } - } - - if stack.is_empty() { - break; - } - } -} - -// Returns an iterator over all nodes in the given LDD. Visits each node only if the predicate holds. -pub fn iter_nodes<'a, P>(storage: &'a Storage, ldd: &Ldd, filter: P) -> IterNode<'a, P> -where - P: Fn(&Ldd) -> bool, -{ - let mut stack = Vec::new(); - - if ldd != storage.empty_set() { - stack.push((ldd.clone(), false)); - } - - IterNode { - storage, - stack, - predicate: filter, - } -} - -pub struct IterNode<'a, P> -where - P: Fn(&Ldd) -> bool, -{ - storage: &'a Storage, - stack: Vec<(Ldd, bool)>, - predicate: P, -} - -impl

Iterator for IterNode<'_, P> -where - P: Fn(&Ldd) -> bool, -{ - type Item = (Ldd, Data); - - fn next(&mut self) -> Option { - while let Some((current, visited)) = self.stack.pop() { - let data = self.storage.get(¤t); - - if visited { - return Some((current, data)); - } - - let Data(_, down, right) = &data; - - // Next time we can actually process the current node. - self.stack.push((current.clone(), true)); - - // Add unvisited children to stack - if (self.predicate)(down) { - self.stack.push((down.clone(), false)); - } - - if (self.predicate)(right) { - self.stack.push((right.clone(), false)); - } - } - - None - } -} - -pub struct IterRight<'a> { - storage: &'a Storage, - current: Ldd, -} - -impl Iterator for IterRight<'_> { - type Item = Data; - - fn next(&mut self) -> Option { - if self.current == *self.storage.empty_set() { - None - } else { - // Progress to the right LDD. - let Data(value, down, right) = self.storage.get(&self.current); - self.current = right.clone(); - Some(Data(value, down, right)) - } - } -} - -pub struct Iter<'a> { - storage: &'a Storage, - /// Stores the values of the returned vector. - vector: Vec, - /// Stores the current path in the LDD. - current: Vec, - /// Stores the stack for the depth-first search (only non 'true' or 'false' nodes) - stack: Vec, - /// Indicates whether the iteration is finished. - finished: bool, -} - -impl StreamingIterator for Iter<'_> { - type Item = Vec; - - fn advance(&mut self) { - // Find the next vector by going down the chain. - loop { - if let Some(current) = self.stack.last() { - let DataRef(value, down, _) = self.storage.get_ref(current); - self.vector.push(value); - if down == *self.storage.empty_vector() { - // Reserve sufficient space in current - if self.current.len() < self.vector.len() { - self.current.resize(self.vector.len(), Value::default()); - } - - self.current.copy_from_slice(&self.vector); - break; // Stop iteration. - } else { - self.stack.push(self.storage.protect(&down)); - } - } else { - // No more elements to iterate. - self.finished = true; - return; - } - } - - // Go up the chain to find the next right sibling that is not 'false'. - while let Some(current) = self.stack.pop() { - self.vector.pop(); - let DataRef(_, _, right) = self.storage.get_ref(¤t); - - if right != *self.storage.empty_set() { - self.stack.push(self.storage.protect(&right)); // This is the first right sibling. - break; - } - } - } - - fn get(&self) -> Option<&Self::Item> { - if self.finished { None } else { Some(&self.current) } - } -} - -#[cfg(test)] -mod tests { - - use super::*; - - use merc_utilities::random_test; - - use crate::test_utility::from_iter; - use crate::test_utility::random_vector_set; - - // Test that iter and for_each_mut yield the same set of cubes. - #[test] - #[cfg_attr(miri, ignore)] - fn test_random_iter_for_each_mut() { - random_test(100, |rng| { - let mut storage = Storage::new(); - - let set = random_vector_set(rng, 32, 10, 10); - let ldd = from_iter(&mut storage, set.iter()); - - // Collect via iter. - let mut iter_result: Vec> = Vec::new(); - let mut it = iter(&storage, &ldd); - while let Some(vector) = it.next() { - iter_result.push(vector.to_vec()); - } - - // Collect via for_each_mut. - let mut for_each_result: Vec> = Vec::new(); - for_each_mut(&mut storage, &ldd, |_storage, vector| { - for_each_result.push(vector.to_vec()); - }); - - for_each_result.sort(); - let original_len = for_each_result.len(); - for_each_result.dedup(); - assert_eq!( - original_len, - for_each_result.len(), - "for_each_mut returned duplicate vectors." - ); - - assert_eq!( - iter_result, for_each_result, - "iter and for_each_mut yielded different sequences of cubes." - ); - }) - } - - // Test the iterator implementation. - #[test] - #[cfg_attr(miri, ignore)] - fn test_random_iter() { - random_test(100, |rng| { - let mut storage = Storage::new(); - - let set = random_vector_set(rng, 32, 10, 10); - let ldd = from_iter(&mut storage, set.iter()); - - assert!( - iter(&storage, &ldd).count() == set.len(), - "Number of iterations does not match the number of elements in the set." - ); - - let mut results: Vec> = Vec::new(); - let mut it = iter(&storage, &ldd); - while let Some(vector) = it.next() { - assert!(set.contains(vector), "Found element not in the set."); - results.push(vector.to_vec()); - } - - results.sort(); - let original_len = results.len(); - results.dedup(); - assert_eq!(original_len, results.len(), "iter returned duplicate vectors."); - }) - } -} diff --git a/crates/ldd/src/lib.rs b/crates/ldd/src/lib.rs deleted file mode 100644 index 3ed4066a1..000000000 --- a/crates/ldd/src/lib.rs +++ /dev/null @@ -1,16 +0,0 @@ -#![doc = include_str!("../README.md")] -#[forbid(unsafe_code)] -mod format; -mod io_ldd; -mod io_sylvan; -pub mod iterators; -mod operations; -mod storage; -mod test_utility; - -pub use format::*; -pub use io_ldd::*; -pub use io_sylvan::*; -pub use operations::*; -pub use storage::*; -pub use test_utility::*; diff --git a/crates/ldd/src/operations.rs b/crates/ldd/src/operations.rs deleted file mode 100644 index b739f9a21..000000000 --- a/crates/ldd/src/operations.rs +++ /dev/null @@ -1,820 +0,0 @@ -use crate::BinaryOperator; -use crate::Data; -use crate::DataRef; -use crate::Ldd; -use crate::LddRef; -use crate::Storage; -use crate::TernaryOperator; -use crate::UnaryFunction; -use crate::Value; -use crate::cache_binary_op; -use crate::cache_comm_binary_op; -use crate::cache_terniary_op; -use crate::cache_unary_function; -use crate::iterators::*; - -use std::cmp::Ordering; -use std::cmp::{self}; - -/// Returns an LDD containing only the given vector, i.e., { vector }. -pub fn singleton(storage: &mut Storage, vector: &[Value]) -> Ldd { - let mut root = storage.empty_vector().clone(); - let empty_set = storage.empty_set().clone(); - for val in vector.iter().rev() { - root = storage.insert(*val, &root, &empty_set); - } - - root -} - -/// Computes a meta LDD that is suitable for the [project] function from the -/// given projection indices. -/// -/// This function is useful to be able to cache the projection LDD instead of -/// computing it from the projection array every time. -pub fn compute_proj(storage: &mut Storage, proj: &[Value]) -> Ldd { - // Compute length of proj. - let length = match proj.iter().max() { - Some(x) => *x + 1, - None => 0, - }; - - // Convert projection vectors to meta information. - let mut result: Vec = Vec::new(); - for i in 0..length { - let included = proj.contains(&i); - - if included { - result.push(1); - } else { - result.push(0); - } - } - - singleton(storage, &result) -} - -/// Computes the set of vectors projected onto the given indices, where proj is equal to compute_proj([i_0, ..., i_k]). -/// -/// Formally, for a single vector we have that: -/// - project(, i_0 < ... < i_k) = -/// - project(X, i_0 < ... < i_k) = { project(x, i_0 < ... < i_k) | x in X }. -/// -/// Note that the indices are sorted in the definition, but compute_proj -/// can take any array and ignores both duplicates and order. Also, it -/// follows that i_k must be smaller than or equal to n as x_(i_k) is not -/// defined otherwise. -pub fn project(storage: &mut Storage, set: &LddRef, proj: &LddRef) -> Ldd { - debug_assert_ne!(proj, storage.empty_set(), "proj must be a singleton"); - - if proj == storage.empty_vector() { - // If meta is not defined then the rest is not in the projection (proj is always zero) - storage.empty_vector().clone() - } else if set == storage.empty_set() { - storage.empty_set().clone() - } else { - debug_assert_ne!(set, storage.empty_vector(), "proj can be at most as high as set"); - - cache_binary_op(storage, BinaryOperator::Project, set, proj, |storage, set, proj| { - let DataRef(proj_value, proj_down, _) = storage.get_ref(proj); - let DataRef(value, down, right) = storage.get_ref(set); - - match proj_value { - 0 => { - let right_result = project(storage, &right, proj); - let down_result = project(storage, &down, &proj_down); - union(storage, &right_result, &down_result) - } - 1 => { - let right_result = project(storage, &right, proj); - let down_result = project(storage, &down, &proj_down); - if down_result == *storage.empty_set() { - right_result - } else { - storage.insert(value, &down_result, &right_result) - } - } - x => { - panic!("proj has unexpected value {x}"); - } - } - }) - } -} - -/// Computes a meta LDD from the given read and write projections that is -/// suitable for [relational_product]. -/// -/// The read and write projections are arrays of indices that are read, -/// respectively written, by the corresponding sparse relation. -pub fn compute_meta(storage: &mut Storage, read_proj: &[Value], write_proj: &[Value]) -> (Ldd, Vec, Vec) { - // Compute length of meta. - let length = cmp::max( - match read_proj.iter().max() { - Some(x) => *x + 1, - None => 0, - }, - match write_proj.iter().max() { - Some(x) => *x + 1, - None => 0, - }, - ); - - // Convert projection vectors to meta. - let mut read_positions = Vec::new(); - let mut write_positions = Vec::new(); - - let mut meta: Vec = Vec::new(); - - let mut offset = 0; - for i in 0..length { - let read = read_proj.contains(&i); - let write = write_proj.contains(&i); - if read && write { - meta.push(3); - meta.push(4); - read_positions.push(offset); - write_positions.push(offset + 1); - offset += 2; - } else if read { - meta.push(1); - read_positions.push(offset); - offset += 1; - } else if write { - meta.push(2); - write_positions.push(offset); - offset += 1; - } else { - meta.push(0); - } - } - - (singleton(storage, &meta), read_positions, write_positions) -} - -/// Computes the set of vectors reachable in one step from the given set as defined by the sparse relation rel. Requires that meta = compute_meta(read_proj, write_proj). -/// -/// # Details -/// -/// Formal definition of the function. relational_product(R, S, read_proj, write_proj) = { x[write_proj := y'] | project(x, read_proj) = x' and (x', y') in R and x in S } -/// where R is the relation and S the set. -/// -/// meta is a singleton vector where the value indicates the following: -/// - 0 = not part the relation. -/// - 1 = only in read_proj. -/// - 2 = only in write_proj. -/// - 3 = in both read_proj and write_proj (read phase). -/// - 4 = in both read_proj and write_proj (write phase). -pub fn relational_product(storage: &mut Storage, set: &LddRef, rel: &LddRef, meta: &LddRef) -> Ldd { - debug_assert_ne!(meta, storage.empty_set(), "proj must be a singleton"); - - if meta == storage.empty_vector() { - // If meta is not defined then the rest is not in the relation (meta is always zero) - storage.protect(set) - } else if set == storage.empty_set() || rel == storage.empty_set() { - storage.empty_set().clone() - } else { - cache_terniary_op( - storage, - TernaryOperator::RelationalProduct, - set, - rel, - meta, - |storage, set, rel, meta| { - let DataRef(meta_value, meta_down, _) = storage.get_ref(meta); - - match meta_value { - 0 => { - // Consider all values on this level part of the output and continue with rest. - let DataRef(value, down, right) = storage.get_ref(set); - - let right_result = relational_product(storage, &right, rel, meta); - let down_result = relational_product(storage, &down, rel, &meta_down); - if down_result == *storage.empty_set() { - right_result - } else { - storage.insert(value, &down_result, &right_result) - } - } - 1 => { - // Read the values present in the relation and continue with these values in the set. - let DataRef(set_value, set_down, set_right) = storage.get_ref(set); - let DataRef(rel_value, rel_down, rel_right) = storage.get_ref(rel); - - match set_value.cmp(&rel_value) { - Ordering::Less => relational_product(storage, &set_right, rel, meta), - Ordering::Equal => { - let down_result = relational_product(storage, &set_down, &rel_down, &meta_down); - let right_result = relational_product(storage, &set_right, &rel_right, meta); - if down_result == *storage.empty_set() { - right_result - } else { - storage.insert(set_value, &down_result, &right_result) - } - } - Ordering::Greater => relational_product(storage, set, &rel_right, meta), - } - } - 2 => { - // All values in set should be considered. - let mut combined = storage.empty_set().clone(); - let mut current = storage.protect(set); - loop { - let DataRef(_, set_down, set_right) = storage.get_ref(¤t); - combined = union(storage, &combined, &set_down); - - if set_right == *storage.empty_set() { - break; - } - current = storage.protect(&set_right); - } - - // Write the values present in the relation. - let DataRef(rel_value, rel_down, rel_right) = storage.get_ref(rel); - - let down_result = relational_product(storage, &combined, &rel_down, &meta_down); - let right_result = relational_product(storage, set, &rel_right, meta); - if down_result == *storage.empty_set() { - right_result - } else { - storage.insert(rel_value, &down_result, &right_result) - } - } - 3 => { - let DataRef(set_value, set_down, set_right) = storage.get_ref(set); - let DataRef(rel_value, rel_down, rel_right) = storage.get_ref(rel); - - match set_value.cmp(&rel_value) { - Ordering::Less => relational_product(storage, &set_right, rel, meta), - Ordering::Equal => { - let down_result = relational_product(storage, &set_down, &rel_down, &meta_down); - let right_result = relational_product(storage, &set_right, &rel_right, meta); - union(storage, &down_result, &right_result) - } - Ordering::Greater => relational_product(storage, set, &rel_right, meta), - } - } - 4 => { - // Write the values present in the relation. - let DataRef(rel_value, rel_down, rel_right) = storage.get_ref(rel); - - let down_result = relational_product(storage, set, &rel_down, &meta_down); - let right_result = relational_product(storage, set, &rel_right, meta); - if down_result == *storage.empty_set() { - right_result - } else { - storage.insert(rel_value, &down_result, &right_result) - } - } - x => { - panic!("meta has unexpected value: {x}"); - } - } - }, - ) - } -} - -/// Returns the largest subset of 'a' that does not contains elements of 'b', i.e., set difference. -pub fn minus(storage: &mut Storage, a: &LddRef, b: &LddRef) -> Ldd { - if a == b || a == storage.empty_set() { - storage.empty_set().clone() - } else if b == storage.empty_set() { - storage.protect(a) - } else { - cache_binary_op(storage, BinaryOperator::Minus, a, b, |storage, a, b| { - let DataRef(a_value, a_down, a_right) = storage.get_ref(a); - let DataRef(b_value, b_down, b_right) = storage.get_ref(b); - - match a_value.cmp(&b_value) { - Ordering::Less => { - let right_result = minus(storage, &a_right, b); - storage.insert(a_value, &a_down, &right_result) - } - Ordering::Equal => { - let down_result = minus(storage, &a_down, &b_down); - let right_result = minus(storage, &a_right, &b_right); - if down_result == *storage.empty_set() { - right_result - } else { - storage.insert(a_value, &down_result, &right_result) - } - } - Ordering::Greater => minus(storage, a, &b_right), - } - }) - } -} - -/// Returns the union of the given LDDs, i.e., a ∪ b. -pub fn union(storage: &mut Storage, a: &LddRef, b: &LddRef) -> Ldd { - if a == b { - storage.protect(a) - } else if a == storage.empty_set() { - storage.protect(b) - } else if b == storage.empty_set() { - storage.protect(a) - } else { - cache_comm_binary_op(storage, BinaryOperator::Union, a, b, |storage, a, b| { - let DataRef(a_value, a_down, a_right) = storage.get_ref(a); - let DataRef(b_value, b_down, b_right) = storage.get_ref(b); - - match a_value.cmp(&b_value) { - Ordering::Less => { - let result = union(storage, &a_right, b); - storage.insert(a_value, &a_down, &result) - } - Ordering::Equal => { - let down_result = union(storage, &a_down, &b_down); - let right_result = union(storage, &a_right, &b_right); - storage.insert(a_value, &down_result, &right_result) - } - Ordering::Greater => { - let result = union(storage, a, &b_right); - storage.insert(b_value, &b_down, &result) - } - } - }) - } -} - -/// Interleave the vectors of two equal height ldds. -pub fn merge(storage: &mut Storage, a: &LddRef, b: &LddRef) -> Ldd { - if a == storage.empty_vector() { - storage.protect(b) - } else if b == storage.empty_vector() { - storage.protect(a) - } else if a == storage.empty_set() || b == storage.empty_set() { - storage.empty_set().clone() - } else { - cache_binary_op(storage, BinaryOperator::Merge, a, b, |storage, a, b| { - let DataRef(value, down, right) = storage.get_ref(a); - - let down_result = merge(storage, b, &down); - let right_result = merge(storage, &right, b); - - storage.insert(value, &down_result, &right_result) - }) - } -} - -/// Appends the given value to every vector in the set represented by the given ldd. -pub fn append(storage: &mut Storage, ldd: &LddRef, value: Value) -> Ldd { - if ldd == storage.empty_set() { - storage.empty_set().clone() - } else if ldd == storage.empty_vector() { - singleton(storage, &[value]) - } else { - // Traverse the ldd. - let DataRef(val, down, right) = storage.get_ref(ldd); - - let down_result = append(storage, &down, value); - let right_result = append(storage, &right, value); - - storage.insert(val, &down_result, &right_result) - } -} - -/// Returns true iff the set contains the vector. -pub fn element_of(storage: &Storage, vector: &[Value], ldd: &Ldd) -> bool { - if vector.is_empty() { - ldd == storage.empty_vector() - } else if ldd == storage.empty_vector() { - false - } else { - for Data(value, down, _) in iter_right(storage, ldd) { - match value.cmp(&vector[0]) { - Ordering::Less => { - continue; - } - Ordering::Equal => { - return element_of(storage, &vector[1..], &down); - } - Ordering::Greater => { - return false; - } - } - } - - false - } -} - -/// Returns the number of elements in the set. -pub fn len(storage: &mut Storage, set: &LddRef) -> usize { - if set == storage.empty_set() { - 0 - } else if set == storage.empty_vector() { - 1 - } else { - cache_unary_function(storage, UnaryFunction::Len, set, |storage, a| { - let mut result: usize = 0; - - let mut current = storage.protect(a); - while current != *storage.empty_set() { - // Progress to the right LDD. - let DataRef(_, down, right) = storage.get_ref(¤t); - result += len(storage, &down); - current = storage.protect(&right); - } - - result - }) - } -} - -/// Returns the height of the LDD tree. -pub fn height(storage: &Storage, ldd: &LddRef) -> usize { - if ldd == storage.empty_set() || ldd == storage.empty_vector() { - 0 - } else { - // Since all children have the same height we only have to look at the down node. - let DataRef(_, down, _) = storage.get_ref(ldd); - - height(storage, &down) + 1 - } -} - -#[cfg(test)] -mod tests { - use super::*; - - use std::collections::HashSet; - use std::ops::Sub; - - use rand::RngExt; - use streaming_iterator::StreamingIterator; - - use merc_utilities::random_test; - - use crate::LddDisplay; - use crate::test_utility::*; - - // Compare the LDD element_of implementation for random inputs. - #[test] - #[cfg_attr(miri, ignore)] - fn test_random_element_of() { - random_test(100, |rng| { - let mut storage = Storage::new(); - - let length = 10; - let set = random_vector_set(rng, 32, length, 10); - let ldd = from_iter(&mut storage, set.iter()); - - // All elements in the set should be contained in the ldd. - for expected in &set { - assert!( - element_of(&storage, expected, &ldd), - "Did not find expected vector in ldd" - ); - } - - // No shorter vectors should be contained in the ldd (try several times). - for _ in 0..10 { - let len = rng.random_range(0..length); - let short_vector = random_vector(rng, len, 10); - assert!( - !element_of(&storage, &short_vector, &ldd), - "Found shorter vector in ldd." - ); - } - - // No longer vectors should be contained in the ldd. - for _ in 0..10 { - let len = rng.random_range(length + 1..20); - let short_vector = random_vector(rng, len, 10); - assert!(!element_of(&storage, &short_vector, &ldd), "Found longer vector in ldd"); - } - - // Try vectors of correct size with both the set and ldd. - for _ in 0..10 { - let vector = random_vector(rng, length, 10); - assert_eq!( - set.contains(&vector), - element_of(&storage, &vector, &ldd), - "Set contains did not match ldd element_of" - ); - } - }); - } - - // Compare the HashSet implementation of union with the LDD union implementation for random inputs. - #[test] - #[cfg_attr(miri, ignore)] - fn test_random_union() { - random_test(100, |rng| { - let mut storage = Storage::new(); - - let set_a = random_vector_set(rng, 32, 10, 10); - let set_b = random_vector_set(rng, 32, 10, 10); - let expected = from_iter(&mut storage, set_a.union(&set_b)); - - let a = from_iter(&mut storage, set_a.iter()); - let b = from_iter(&mut storage, set_b.iter()); - let result = union(&mut storage, &a, &b); - - assert_eq!(result, expected); - }); - } - - #[test] - #[cfg_attr(miri, ignore)] - fn test_random_merge() { - random_test(100, |rng| { - let mut storage = Storage::new(); - - let set_a = random_vector_set(rng, 32, 10, 10); - let set_b = random_vector_set(rng, 32, 10, 10); - - // Compute the interleave explicitly. - fn interleave(a: &[u32], b: &[u32]) -> Vec { - let mut result = vec![]; - - let mut iter = b.iter(); - for value in a { - result.push(*value); - result.push(*iter.next().unwrap()); - } - - result - } - - let mut set_result = HashSet::>::new(); - for a in &set_a { - for b in &set_b { - set_result.insert(interleave(a, b)); - } - } - - let expected = from_iter(&mut storage, set_result.iter()); - - let a = from_iter(&mut storage, set_a.iter()); - let b = from_iter(&mut storage, set_b.iter()); - let result: Ldd = merge(&mut storage, &a, &b); - - assert_eq!(result, expected); - }); - } - - // Compare the singleton implementation with a random vector used as input. - #[test] - #[cfg_attr(miri, ignore)] - fn test_random_singleton() { - random_test(100, |rng| { - let mut storage = Storage::new(); - let vector = random_vector(rng, 10, 10); - - let ldd = singleton(&mut storage, &vector[..]); - - // Check that ldd contains exactly one vector that is equal to the initial vector. - let mut it = iter(&storage, &ldd); - let result = it.next().unwrap(); - assert_eq!(vector, *result, "Contained vector did not match expected"); - assert_eq!(it.next(), None, "The ldd should not contain any other vector"); - }); - } - - // Test the len function with random inputs. - #[test] - #[cfg_attr(miri, ignore)] - fn test_random_len() { - random_test(100, |rng| { - let mut storage = Storage::new(); - - let set = random_vector_set(rng, 32, 10, 10); - let ldd = from_iter(&mut storage, set.iter()); - - assert_eq!(set.len(), len(&mut storage, &ldd), "Length did not match expected set"); - }); - } - - // Test the minus function with random inputs. - #[test] - #[cfg_attr(miri, ignore)] - fn test_random_minus() { - random_test(100, |rng| { - let mut storage = Storage::new(); - - let set_a = random_vector_set(rng, 32, 10, 10); - let set_b = { - let mut result = random_vector_set(rng, 32, 10, 10); - - // To ensure some overlap (which is unlikely) we insert some elements of a into b. - let mut it = set_a.iter(); - for _ in 0..16 { - result.insert(it.next().unwrap().clone()); - } - - result - }; - - let expected_result = set_a.sub(&set_b); - - let a = from_iter(&mut storage, set_a.iter()); - let b = from_iter(&mut storage, set_b.iter()); - let result = minus(&mut storage, &a, &b); - - let expected = from_iter(&mut storage, expected_result.iter()); - - println!("{}", LddDisplay::new(&storage, &result)); - println!("{}", LddDisplay::new(&storage, &expected)); - - assert_eq!(result, expected); - }); - } - - // Test the relational product function with read-only inputs. - #[test] - #[cfg_attr(miri, ignore)] - fn test_random_readonly_relational_product() { - random_test(100, |rng| { - let mut storage = Storage::new(); - let set = random_vector_set(rng, 32, 10, 10); - - let ldd = from_iter(&mut storage, set.iter()); - - let read_proj = random_sorted_vector(rng, 4, 9); - let meta = compute_meta(&mut storage, &read_proj, &[]).0; - - let proj_ldd = compute_proj(&mut storage, &read_proj); - let relation = project(&mut storage, &ldd, &proj_ldd); - - let result = relational_product(&mut storage, &ldd, &relation, &meta); - let read_project = project(&mut storage, &result, &proj_ldd); - - // relational_product(R, S, read_proj, []) = { x | project(x, read_proj) = x' and (x', <>) in R and x in S } - assert_eq!(read_project, relation); - }); - } - - // Test the relational product function with write-only inputs. - #[test] - #[cfg_attr(miri, ignore)] - fn test_random_writeonly_relational_product() { - random_test(100, |rng| { - let mut storage = Storage::new(); - let set = random_vector_set(rng, 32, 10, 10); - - let ldd = from_iter(&mut storage, set.iter()); - - let write_proj = random_sorted_vector(rng, 4, 9); - let meta = compute_meta(&mut storage, &[], &write_proj).0; - - let proj_ldd = compute_proj(&mut storage, &write_proj); - let relation = project(&mut storage, &ldd, &proj_ldd); - - let result = relational_product(&mut storage, &ldd, &relation, &meta); - let write_project = project(&mut storage, &result, &proj_ldd); - - // relational_product(R, S, [], write_proj) = { x[write_proj := y'] | (<>, y') in R and x in S } - assert_eq!(write_project, relation); - }); - } - - #[test] - #[cfg_attr(miri, ignore)] - fn test_random_relational_product() { - random_test(100, |rng| { - let mut storage = Storage::new(); - - let set = random_vector_set(rng, 32, 10, 10); - let relation = random_vector_set(rng, 32, 4, 10); - - // Pick arbitrary read and write parameters in order. - let read_proj = random_sorted_vector(rng, 2, 9); - let write_proj = random_sorted_vector(rng, 2, 9); - - // The indices of the input vectors do not match the indices in the relation. The input vector is defined for all values, but the relation only - // for relevant positions. - let (read_rel_proj, write_rel_proj) = { - let mut read_rel_proj: Vec = Vec::new(); - let mut write_rel_proj: Vec = Vec::new(); - - let mut current = 0; - for i in 0..10 { - if read_proj.contains(&i) { - read_rel_proj.push(current); - current += 1; - } - - if write_proj.contains(&i) { - write_rel_proj.push(current); - current += 1; - } - } - - (read_rel_proj, write_rel_proj) - }; - - // Compute LDD result. - let ldd = from_iter(&mut storage, set.iter()); - let rel = from_iter(&mut storage, relation.iter()); - - let meta = compute_meta(&mut storage, &read_proj, &write_proj).0; - let result = relational_product(&mut storage, &ldd, &rel, &meta); - - eprintln!("set = {}", LddDisplay::new(&storage, &ldd)); - eprintln!("relation = {}", LddDisplay::new(&storage, &rel)); - eprintln!("result = {}", LddDisplay::new(&storage, &result)); - eprintln!("========"); - - eprintln!("meta = {}", LddDisplay::new(&storage, &meta)); - eprintln!( - "read {:?}, write {:?}, read_rel {:?} and write_rel {:?}", - read_proj, write_proj, read_rel_proj, write_rel_proj - ); - - let expected = { - let mut expected: HashSet> = HashSet::new(); - - // Compute relational_product(R, S, read_proj, write_proj) = { x[write_proj := y'] | project(x, read_proj) = x' and (x', y') in R and x in S } - for x in set.iter() { - 'next: for rel in relation.iter() { - let mut value = x.clone(); // The resulting vector. - let x_prime = project_vector(rel, &read_rel_proj); - let y_prime = project_vector(rel, &write_rel_proj); - - // Ensure that project(x, read_proj) = x' - for (i, r) in read_proj.iter().enumerate() { - if value[*r as usize] != x_prime[i] { - continue 'next; - } - } - - // Compute x[write_proj := y'] - for (i, w) in write_proj.iter().enumerate() { - value[*w as usize] = y_prime[i]; - } - - // Print information about the value that we are testing. - eprintln!("value = {:?}, rel = {:?}", &value, &rel); - eprintln!("x_prime = {:?}, y_prime = {:?}", &x_prime, &y_prime); - - assert!( - element_of(&storage, &value, &result), - "Result does not contain vector {:?}.", - &value - ); - expected.insert(value); - } - } - - expected - }; - - // Check the other way around - let mut iter = iter(&storage, &result); - while let Some(res) = iter.next() { - assert!(expected.contains(res), "Result unexpectedly contains vector {:?}.", res); - } - }); - } - - // Test the project function with random inputs. - #[test] - #[cfg_attr(miri, ignore)] - fn test_random_project() { - random_test(100, |rng| { - let mut storage = Storage::new(); - - let set = random_vector_set(rng, 32, 10, 10); - let proj = random_sorted_vector(rng, 4, 9); - - let ldd = from_iter(&mut storage, set.iter()); - let proj_ldd = compute_proj(&mut storage, &proj); - let result = project(&mut storage, &ldd, &proj_ldd); - - // Compute a naive projection on the vector set. - let mut expected_result: HashSet> = HashSet::new(); - for element in &set { - expected_result.insert(project_vector(element, &proj)); - } - let expected = from_iter(&mut storage, expected_result.iter()); - assert_eq!(result, expected, "projected result does not match vector projection."); - }); - } - - // Test the append function with random inputs. - #[test] - #[cfg_attr(miri, ignore)] - fn test_random_append() { - random_test(100, |rng| { - let mut storage = Storage::new(); - - let set = random_vector_set(rng, 32, 10, 10); - let ldd = from_iter(&mut storage, set.iter()); - let result = append(&mut storage, &ldd, 0); - - let mut expected_result: HashSet> = HashSet::new(); - for element in &set { - let mut appended = element.to_vec(); - appended.push(0 as Value); - expected_result.insert(appended); - } - let expected = from_iter(&mut storage, expected_result.iter()); - - print_differences(&storage, &result, &expected); - assert_eq!(result, expected, "appended result does not match vector append"); - }); - } -} diff --git a/crates/ldd/src/storage.rs b/crates/ldd/src/storage.rs deleted file mode 100644 index 8bf427a00..000000000 --- a/crates/ldd/src/storage.rs +++ /dev/null @@ -1,377 +0,0 @@ -use std::cell::RefCell; -use std::hash::Hash; -use std::hash::Hasher; -use std::rc::Rc; - -use ldd::LddIndex; -use ldd::SharedProtectionSet; -use merc_collections::IndexedSet; -use merc_unsafety::ProtectionSet; - -use crate::operations::height; - -mod cache; -mod ldd; - -pub use self::cache::*; -pub use self::ldd::Ldd; -pub use self::ldd::LddRef; - -pub type Value = u32; - -/// This is the LDD node(value, down, right) with some additional meta data. -#[derive(Clone)] -pub struct Node { - value: Value, - down: LddIndex, - right: LddIndex, - - marked: bool, -} - -/// Check that the node size has the expected size. -#[cfg(not(debug_assertions))] -const _: () = assert!(std::mem::size_of::() == std::mem::size_of::<(usize, usize, usize)>()); - -impl Node { - fn new(value: Value, down: LddIndex, right: LddIndex) -> Node { - Node { - value, - down, - right, - marked: false, - } - } - - /// Returns false if the node has been garbage collected. - pub fn is_valid(&self) -> bool { - true - } -} - -impl PartialEq for Node { - fn eq(&self, other: &Self) -> bool { - self.value == other.value && self.down == other.down && self.right == other.right - } -} - -impl Eq for Node {} - -impl Hash for Node { - fn hash(&self, state: &mut H) { - self.value.hash(state); - self.down.hash(state); - self.right.hash(state); - } -} - -/// This is the user facing data of a [Node]. -pub struct Data(pub Value, pub Ldd, pub Ldd); - -/// This is the user facing data of a [Node] as references. -pub struct DataRef<'a>(pub Value, pub LddRef<'a>, pub LddRef<'a>); - -/// The storage that implements the maximal sharing behaviour. Meaning that -/// identical nodes (same value, down and right) have a unique index in the node -/// table. Therefore guaranteeing that Ldds n and m are identical iff their -/// indices in the node table match. -pub struct Storage { - protection_set: SharedProtectionSet, // Every Ldd points to the underlying protection set. - nodes: IndexedSet, - cache: OperationCache, - - count_until_collection: u64, // Count down until the next garbage collection. - enable_garbage_collection: bool, // Whether to enable automatic garbage collection based on heuristics. - enable_performance_metrics: bool, - empty_set: Ldd, - empty_vector: Ldd, -} - -impl Default for Storage { - fn default() -> Self { - Self::new() - } -} - -impl Storage { - pub fn new() -> Self { - let shared = Rc::new(RefCell::new(ProtectionSet::new())); - // Add two nodes representing 'false' and 'true' respectively; these cannot be created using insert. - let mut nodes = IndexedSet::new(); - let empty_set = nodes.insert(Node::new(0, LddIndex::default(), LddIndex::default())).0; - let empty_vector = nodes.insert(Node::new(1, LddIndex::default(), LddIndex::default())).0; - - Self { - protection_set: shared.clone(), - nodes, - cache: OperationCache::new(Rc::clone(&shared)), - - count_until_collection: 10000, - enable_garbage_collection: true, - enable_performance_metrics: false, - empty_set: Ldd::new(&shared, empty_set), - empty_vector: Ldd::new(&shared, empty_vector), - } - } - - /// Provides access to the underlying operation cache. - pub fn operation_cache(&mut self) -> &mut OperationCache { - &mut self.cache - } - - /// Create a new LDD singleton(value) - pub fn insert_singleton(&mut self, value: Value) -> Ldd { - if self.count_until_collection == 0 { - if self.enable_garbage_collection { - self.garbage_collect(); - } - self.count_until_collection = self.nodes.len() as u64; - } - - let (index, _inserted) = - self.nodes - .insert(Node::new(value, self.empty_vector().index(), self.empty_set().index())); - - Ldd::new(&self.protection_set, index) - } - - /// Create a new LDD node(value, down, right) - pub fn insert(&mut self, value: Value, down: &LddRef, right: &LddRef) -> Ldd { - // These invariants ensure that the result is a valid LDD. - debug_assert_ne!(down, self.empty_set(), "down node can never be the empty set."); - debug_assert_ne!(right, self.empty_vector(), "right node can never be the empty vector."); - debug_assert!(*down.index() < self.nodes.len(), "down node not in table."); - debug_assert!(*right.index() < self.nodes.len(), "right not not in table."); - - if right != self.empty_set() { - debug_assert_eq!( - height(self, down) + 1, - height(self, right), - "height of node {} should match the right node {} height.", - down.index(), - right.index() - ); - debug_assert!(value < self.value(right), "value should be less than right node value."); - } - - if self.count_until_collection == 0 { - if self.enable_garbage_collection { - self.garbage_collect(); - } - self.count_until_collection = self.nodes.len() as u64; - } - - let (index, _inserted) = self.nodes.insert(Node::new(value, down.index(), right.index())); - - Ldd::new(&self.protection_set, index) - } - - /// Upgrade an [LddRef] to a protected [Ldd] instance. - pub fn protect(&self, ldd: &LddRef) -> Ldd { - Ldd::new(&self.protection_set, ldd.index()) - } - - /// Cleans up all LDDs that are unreachable from the root LDDs. - pub fn garbage_collect(&mut self) { - // Clear the cache since it contains unprotected LDDs, and keep track of size before clearing. - let size_of_cache = self.cache.len(); - self.cache.clear(); - self.cache.limit(self.nodes.len()); - - // Mark all nodes that are (indirect) children of nodes with positive reference count. - let mut stack: Vec = Vec::new(); - for (_root, index) in self.protection_set.borrow().iter() { - mark_node(&mut self.nodes, &mut stack, *index); - } - - // Collect all garbage nodes. - let mut number_of_collections: usize = 0; - self.nodes.retain_mut(|_, node| { - if node.marked { - debug_assert!(node.is_valid(), "Should never mark a node that is not valid."); - node.marked = false; - true - } else { - number_of_collections += 1; - false - } - }); - - // Check whether the direct children of a valid node are valid (this implies that the whole tree is valid if the root is valid). - for (_, node) in &self.nodes { - // Special cases for the empty set and empty vector. - debug_assert!( - *node.down == 0 || self.nodes.get(node.down).is_some(), - "The down node of a valid node must be valid." - ); - debug_assert!( - *node.right == 0 || self.nodes.get(node.right).is_some(), - "The right node of a valid node must be valid." - ); - } - - if self.enable_performance_metrics { - println!( - "Collected {number_of_collections} elements and {} elements remaining", - self.nodes.len() - ); - println!("Operation cache contains {size_of_cache} elements"); - } - } - - /// Enables automatic garbage collection, which is enabled by default. - pub fn enable_garbage_collection(&mut self, enabled: bool) { - self.enable_garbage_collection = enabled; - } - - pub fn enable_performance_metrics(&mut self, enabled: bool) { - self.enable_performance_metrics = enabled; - } - - /// The 'false' LDD. - pub fn empty_set(&self) -> &Ldd { - &self.empty_set - } - - /// The 'true' LDD. - pub fn empty_vector(&self) -> &Ldd { - &self.empty_vector - } - - /// The value of an LDD node(value, down, right). Note, ldd cannot be 'true' or 'false. - pub fn value(&self, ldd: &LddRef) -> Value { - self.verify_ldd(ldd); - let node = &self.nodes[ldd.index()]; - node.value - } - - /// The down of an LDD node(value, down, right). Note, ldd cannot be 'true' or 'false. - pub fn down(&self, ldd: &LddRef) -> Ldd { - self.verify_ldd(ldd); - let node = &self.nodes[ldd.index()]; - Ldd::new(&self.protection_set, node.down) - } - - /// The right of an LDD node(value, down, right). Note, ldd cannot be 'true' or 'false. - pub fn right(&self, ldd: &LddRef) -> Ldd { - self.verify_ldd(ldd); - let node = &self.nodes[ldd.index()]; - Ldd::new(&self.protection_set, node.right) - } - - /// Returns a Data tuple for the given LDD node(value, down, right). Note, ldd cannot be 'true' or 'false. - pub fn get(&self, ldd: &LddRef) -> Data { - self.verify_ldd(ldd); - let node = &self.nodes[ldd.index()]; - Data( - node.value, - Ldd::new(&self.protection_set, node.down), - Ldd::new(&self.protection_set, node.right), - ) - } - - /// Returns a DataRef tuple for the given LDD node(value, down, right). Note, ldd cannot be 'true' or 'false. - pub fn get_ref<'a>(&self, ldd: &'a LddRef) -> DataRef<'a> { - self.verify_ldd(ldd); - let node = &self.nodes[ldd.index()]; - DataRef(node.value, LddRef::new(node.down), LddRef::new(node.right)) - } - - // Asserts whether the given ldd is valid. - fn verify_ldd(&self, ldd: &LddRef) { - debug_assert_ne!(ldd, self.empty_set(), "Cannot inspect empty set."); - debug_assert_ne!(ldd, self.empty_vector(), "Cannot inspect empty vector."); - debug_assert!( - self.nodes.get(ldd.index()).is_some(), - "Node {} should not have been garbage collected", - ldd.index() - ); - } -} - -impl Drop for Storage { - fn drop(&mut self) { - if self.enable_performance_metrics { - println!( - "There were {} insertions into the protection set.", - self.protection_set.borrow().number_of_insertions() - ); - println!( - "There were at most {} root variables.", - self.protection_set.borrow().maximum_size() - ); - println!("There were at most {} nodes.", self.nodes.capacity()); - } - } -} - -/// Mark all LDDs reachable from the given root index. -/// -/// Reuses the stack for the depth-first exploration. -fn mark_node(nodes: &mut IndexedSet, stack: &mut Vec, root: LddIndex) { - stack.push(root); - while let Some(current) = stack.pop() { - let node = &mut nodes[current]; - debug_assert!(node.is_valid(), "Should never mark a node that is not valid."); - if node.marked { - continue; - } else { - node.marked = true; - if *current != 0 && *current != 1 { - stack.push(node.down); - stack.push(node.right); - } - } - } - - debug_assert!(stack.is_empty(), "When marking finishes the stack should be empty."); -} - -#[cfg(test)] -mod tests { - - use super::*; - use crate::operations::singleton; - use crate::test_utility::*; - - use merc_utilities::random_test; - - #[test] - fn test_random_garbage_collection_small() { - random_test(100, |rng| { - let mut storage = Storage::new(); - - let _child: Ldd; - { - // Make sure that this set goes out of scope, but keep a reference to some child ldd. - let vector = random_vector(rng, 10, 10); - let ldd = singleton(&mut storage, &vector); - - _child = storage.get(&ldd).1; - storage.garbage_collect(); - } - - storage.garbage_collect(); - }); - } - - #[test] - #[cfg_attr(miri, ignore)] - fn test_random_garbage_collection() { - random_test(20, |rng| { - let mut storage = Storage::new(); - - let _child: Ldd; - { - // Make sure that this set goes out of scope, but keep a reference to some child ldd. - let vector = random_vector_set(rng, 2000, 10, 2); - let ldd = from_iter(&mut storage, vector.iter()); - - _child = storage.get(&storage.get(&ldd).1).1; - storage.garbage_collect(); - } - - storage.garbage_collect(); - }); - } -} diff --git a/crates/ldd/src/storage/cache.rs b/crates/ldd/src/storage/cache.rs deleted file mode 100644 index 9273e55f1..000000000 --- a/crates/ldd/src/storage/cache.rs +++ /dev/null @@ -1,295 +0,0 @@ -use ahash::RandomState; -use core::hash::Hash; -use std::hash::BuildHasher; - -use crate::Ldd; -use crate::LddRef; -use crate::Storage; - -use super::ldd::LddIndex; -use super::ldd::SharedProtectionSet; - -/// The operation cache can significantly speed up operations by caching -/// intermediate results. This is necessary since the maximal sharing means that -/// the same inputs can be encountered many times while evaluating the -/// operation. -/// -/// For all operations defined in `operations.rs` where caching helps we -/// introduce a cache. The cache that belongs to one operation is identified by -/// the value of [UnaryFunction], [BinaryOperator] or [TernaryOperator]. -pub struct OperationCache { - protection_set: SharedProtectionSet, - caches1: Vec>, - caches2: Vec>, - caches3: Vec>, -} - -impl OperationCache { - pub fn new(protection_set: SharedProtectionSet) -> OperationCache { - OperationCache { - protection_set, - caches1: vec![Cache::new()], - caches2: vec![Cache::new(); 4], - caches3: vec![Cache::new()], - } - } - - /// Clear all existing caches. This must be done during garbage collection - /// since caches have references to elements in the node table that are not - /// protected. - pub fn clear(&mut self) { - for cache in self.caches1.iter_mut() { - cache.clear(); - } - - for cache in self.caches2.iter_mut() { - cache.clear(); - } - - for cache in self.caches3.iter_mut() { - cache.clear(); - } - } - - /// Returns the number of elements in the operation cache. - pub fn len(&self) -> usize { - let mut result: usize = 0; - - for cache in self.caches1.iter() { - result += cache.len(); - } - - for cache in self.caches2.iter() { - result += cache.len(); - } - - for cache in self.caches3.iter() { - result += cache.len(); - } - - result - } - - /// Returns true iff the operation cache is empty. - pub fn is_empty(&self) -> bool { - self.len() == 0 - } - - /// Puts a limit on the operation cache size. This will ensure that - /// self.len() <= n if self.limit(n) has been set. - pub fn limit(&mut self, size: usize) { - for cache in self.caches1.iter_mut() { - cache.limit(size / 4); - } - - for cache in self.caches2.iter_mut() { - cache.limit(size / 4); - } - - for cache in self.caches3.iter_mut() { - cache.limit(size / 4); - } - } - - fn get_cache1(&mut self, operator: &UnaryFunction) -> &mut Cache { - match operator { - UnaryFunction::Len => &mut self.caches1[0], - } - } - - fn get_cache2(&mut self, operator: &BinaryOperator) -> &mut Cache<(LddIndex, LddIndex), LddIndex> { - match operator { - BinaryOperator::Union => &mut self.caches2[0], - BinaryOperator::Merge => &mut self.caches2[1], - BinaryOperator::Minus => &mut self.caches2[2], - BinaryOperator::Project => &mut self.caches2[3], - } - } - - fn get_cache3(&mut self, operator: &TernaryOperator) -> &mut Cache<(LddIndex, LddIndex, LddIndex), LddIndex> { - match operator { - TernaryOperator::RelationalProduct => &mut self.caches3[0], - } - } - - /// Create an Ldd from the given index. Only safe because this is a private function. - fn create(&mut self, index: LddIndex) -> Ldd { - Ldd::new(&self.protection_set, index) - } -} - -/// Implements an associative mapping between key value pairs, but has a limit -/// on the maximum amount of elements stored. The cache requires that default -/// values of K are never used in calls to get and insert, because these are -/// used to indicate empty cache entries. -pub struct Cache { - table: Vec<(K, V)>, - hash_builder: S, -} - -impl Cache { - pub fn new() -> Cache { - Cache { - table: vec![Default::default(); 1024], - hash_builder: RandomState::default(), - } - } -} - -impl Default for Cache { - fn default() -> Self { - Self::new() - } -} - -impl Cache { - /// Removes all elements stored in the cache. - pub fn clear(&mut self) { - let capacity = self.table.len(); - - self.table.clear(); - self.table.resize(capacity, Default::default()); - } - - /// Puts a limit on the maximum self.len() of this cache. - pub fn limit(&mut self, size: usize) { - let power_of_two = size.next_power_of_two(); - - self.table.clear(); - self.table.resize(power_of_two, Default::default()); - } - - /// Returns the amount of elements in the cache. - pub fn len(&self) -> usize { - self.table.len() - } - - /// Returns true iff the cache is empty. - pub fn is_empty(&self) -> bool { - self.len() == 0 - } -} - -impl Cache { - /// Check whether key is in the storage, if so returns Some(value) and None otherwise. - pub fn get(&mut self, key: &K) -> Option<&V> { - debug_assert!(*key != K::default(), "The key may never be equal to its default value."); - - // Compute the index in the table. - let index = self.hash_builder.hash_one(key) % (self.table.len() as u64); - - let entry = &self.table[index as usize]; - if entry.0 == *key { Some(&entry.1) } else { None } - } - - /// Inserts the given key value pair into the cache. Might evict other pairs in the cache. - pub fn insert(&mut self, key: K, value: V) { - debug_assert!(key != K::default(), "The key may never be equal to its default value."); - - // Compute the index in the table. - - let index = self.hash_builder.hash_one(&key) % (self.table.len() as u64); - self.table[index as usize] = (key, value); - } -} - -impl Clone for Cache { - fn clone(&self) -> Self { - Cache { - table: self.table.clone(), - hash_builder: self.hash_builder.clone(), - } - } -} - -/// Any function from LDD -> usize. -pub enum UnaryFunction { - Len, -} - -/// Any operator from LDD x LDD -> LDD. -pub enum BinaryOperator { - Union, - Merge, - Minus, - Project, -} - -/// Any operator from LDD x LDD x LDD -> LDD. -pub enum TernaryOperator { - RelationalProduct, -} - -/// Implements an operation cache for a unary LDD operator. -pub fn cache_unary_function(storage: &mut Storage, operator: UnaryFunction, a: &LddRef, f: F) -> usize -where - F: Fn(&mut Storage, &LddRef<'_>) -> usize, -{ - let key = a.index(); - if let Some(result) = storage.operation_cache().get_cache1(&operator).get(&key) { - *result - } else { - let result = f(storage, a); - storage.operation_cache().get_cache1(&operator).insert(key, result); - result - } -} - -/// Implements an operation cache for a binary LDD operator. -pub fn cache_binary_op(storage: &mut Storage, operator: BinaryOperator, a: &LddRef, b: &LddRef, f: F) -> Ldd -where - F: Fn(&mut Storage, &LddRef<'_>, &LddRef<'_>) -> Ldd, -{ - let key = (a.index(), b.index()); - if let Some(result) = storage.operation_cache().get_cache2(&operator).get(&key) { - let result = *result; // Necessary to decouple borrow from storage and the call to create. - storage.operation_cache().create(result) - } else { - let result = f(storage, a, b); - storage - .operation_cache() - .get_cache2(&operator) - .insert(key, result.index()); - result - } -} - -/// Implements an operation cache for a commutative binary LDD operator, i.e., -/// an operator f such that f(a,b) = f(b,a) for all LDD a and b. -pub fn cache_comm_binary_op(storage: &mut Storage, operator: BinaryOperator, a: &LddRef, b: &LddRef, f: F) -> Ldd -where - F: Fn(&mut Storage, &LddRef<'_>, &LddRef<'_>) -> Ldd, -{ - // Reorder the inputs to improve caching behaviour (can potentially half the cache size) - if a.index() < b.index() { - cache_binary_op(storage, operator, a, b, f) - } else { - cache_binary_op(storage, operator, b, a, f) - } -} - -/// Implements an operation cache for a terniary LDD operator. -pub fn cache_terniary_op( - storage: &mut Storage, - operator: TernaryOperator, - a: &LddRef, - b: &LddRef, - c: &LddRef, - f: F, -) -> Ldd -where - F: Fn(&mut Storage, &LddRef<'_>, &LddRef<'_>, &LddRef<'_>) -> Ldd, -{ - let key = (a.index(), b.index(), c.index()); - if let Some(result) = storage.operation_cache().get_cache3(&operator).get(&key) { - let result = *result; // Necessary to decouple borrow from storage and the call to create. - storage.operation_cache().create(result) - } else { - let result = f(storage, a, b, c); - storage - .operation_cache() - .get_cache3(&operator) - .insert(key, result.index()); - result - } -} diff --git a/crates/ldd/src/storage/ldd.rs b/crates/ldd/src/storage/ldd.rs deleted file mode 100644 index 10345ac85..000000000 --- a/crates/ldd/src/storage/ldd.rs +++ /dev/null @@ -1,154 +0,0 @@ -use std::borrow::Borrow; -use std::cell::RefCell; -use std::fmt::Debug; -use std::fmt::Formatter; -use std::fmt::{self}; -use std::hash::Hash; -use std::hash::Hasher; -use std::marker::PhantomData; -use std::ops::Deref; -use std::rc::Rc; - -use merc_collections::SetIndex; -use merc_unsafety::ProtectionIndex; -use merc_unsafety::ProtectionSet; - -/// An alias for the ldd index type. -pub type LddIndex = SetIndex; - -/// The shared protection set is used to keep track of the nodes that are reachable. -pub type SharedProtectionSet = Rc>>; - -/// Every Ldd points to its root node in the Storage instance for maximal -/// sharing. These Ldd instances can only be created from the storage. -/// -/// # Details -/// -/// Note that the Ldd actually has an interior mutable reference to the protection set. -/// However, this has no influence on the PartialEq and Hash implementations. As such -/// we can use the Ldd as a key in hash maps and sets. Use the following clippy lint -/// to disable the warning about mutable key types: -/// -/// #[allow(clippy::mutable_key_type)] -pub struct Ldd { - ldd: LddRef<'static>, // Reference in the node table. - root: ProtectionIndex, // Index in the root set. - protection_set: SharedProtectionSet, -} - -impl Ldd { - /// Creates a new Ldd instance. This should only be called from the storage. - pub fn new(protection_set: &SharedProtectionSet, index: LddIndex) -> Ldd { - let root = protection_set.borrow_mut().protect(index); - Ldd { - protection_set: Rc::clone(protection_set), - ldd: LddRef::new(index), - root, - } - } - - /// Returns the index of the Ldd. - pub fn index(&self) -> LddIndex { - self.ldd.index - } -} - -impl Deref for Ldd { - type Target = LddRef<'static>; - - fn deref(&self) -> &Self::Target { - &self.ldd - } -} - -impl<'a> Borrow> for Ldd { - fn borrow(&self) -> &LddRef<'a> { - &self.ldd - } -} - -impl Clone for Ldd { - fn clone(&self) -> Self { - Ldd::new(&self.protection_set, self.index()) - } -} - -impl Drop for Ldd { - fn drop(&mut self) { - self.protection_set.borrow_mut().unprotect(self.root); - } -} - -impl PartialEq for Ldd { - fn eq(&self, other: &Self) -> bool { - debug_assert!( - Rc::ptr_eq(&self.protection_set, &other.protection_set), - "Both LDDs should refer to the same storage." - ); - self.index() == other.index() - } -} - -impl Debug for Ldd { - fn fmt(&self, f: &mut Formatter<'_>) -> fmt::Result { - write!(f, "index: {}", self.index()) - } -} - -impl Hash for Ldd { - fn hash(&self, state: &mut H) { - self.index().hash(state); - } -} - -impl Eq for Ldd {} - -/// The LddRef is a reference to an existing [Ldd] instance. This can be used to -/// avoid explicit protections that are performed when creating an [Ldd] -/// instance. -/// -/// # Implementation notes -/// -/// It is important to note that the lifetime carried by an LddRef is only used -/// to enforce lifetime constraints in several places, in a similar way as used -/// for mutex guards or iterators. The lifetime should *not* be used to derive -/// lifetimes of return values and instead these should be derived from `self`. -/// If this is implemented correctly in the internal implementation then the -/// LddRef can never be misused. -#[derive(Hash, PartialEq, Eq)] -pub struct LddRef<'a> { - index: LddIndex, // Index in the node table. - marker: PhantomData<&'a ()>, -} - -impl<'a> LddRef<'a> { - /// TODO: This function should only be called by Storage and [Ldd] - pub fn new(index: LddIndex) -> LddRef<'a> { - LddRef { - index, - marker: PhantomData, - } - } - - /// Returns the index of the LddRef in the node table. - pub fn index(&self) -> LddIndex { - self.index - } - - /// Returns an LddRef with the same lifetime as itself. - pub fn borrow(&self) -> LddRef<'_> { - LddRef::new(self.index()) - } -} - -impl fmt::Debug for LddRef<'_> { - fn fmt(&self, f: &mut Formatter<'_>) -> fmt::Result { - write!(f, "index: {}", self.index()) - } -} - -impl PartialEq for LddRef<'_> { - fn eq(&self, other: &Ldd) -> bool { - self.index == other.index() - } -} diff --git a/crates/symbolic/Cargo.toml b/crates/symbolic/Cargo.toml index ab5860398..30519df67 100644 --- a/crates/symbolic/Cargo.toml +++ b/crates/symbolic/Cargo.toml @@ -21,18 +21,20 @@ merc_aterm.workspace = true merc_collections.workspace = true merc_data.workspace = true merc_io.workspace = true -merc_ldd.workspace = true merc_lts.workspace = true +merc_number.workspace = true merc_utilities.workspace = true clap = { workspace = true, optional = true } duct.workspace = true +delegate.workspace = true itertools.workspace = true log.workspace = true oxidd-core.workspace = true oxidd-dump.workspace = true oxidd-reorder.workspace = true oxidd-rules-bdd.workspace = true +oxidd-rules-ldd.workspace = true oxidd.workspace = true rand.workspace = true rustc-hash.workspace = true diff --git a/crates/symbolic/src/convert_bdd.rs b/crates/symbolic/src/convert_bdd.rs index 6e0a49fa4..6219d57fe 100644 --- a/crates/symbolic/src/convert_bdd.rs +++ b/crates/symbolic/src/convert_bdd.rs @@ -297,7 +297,6 @@ fn compute_positions( #[cfg(test)] mod tests { - use merc_ldd::Storage; use merc_lts::LTS; use merc_lts::LtsBuilderMem; use merc_reduction::Equivalence; @@ -319,13 +318,13 @@ mod tests { let input = include_bytes!("../../../examples/lts/abp.sym"); - let mut storage = Storage::new(); - let manager_ref = oxidd::bdd::new_manager(2048, 1024, 1); - let symbolic_lts = read_symbolic_lts(&mut storage, &input[..]).unwrap(); - let symbolic_lts_bdd = SymbolicLtsBdd::from_symbolic_lts(&mut storage, &manager_ref, &symbolic_lts).unwrap(); + let ldd_manager = oxidd::ldd::new_manager(2048, 1024, 1); + let bdd_manager = oxidd::bdd::new_manager(2048, 1024, 1); + let symbolic_lts = read_symbolic_lts(&ldd_manager, &input[..]).unwrap(); + let symbolic_lts_bdd = SymbolicLtsBdd::from_symbolic_lts(&ldd_manager, &bdd_manager, &symbolic_lts).unwrap(); let mut builder = LtsBuilderMem::new(Vec::new(), Vec::new()); - let lts = convert_symbolic_lts_bdd(&manager_ref, &mut builder, &symbolic_lts_bdd).unwrap(); + let lts = convert_symbolic_lts_bdd(&bdd_manager, &mut builder, &symbolic_lts_bdd).unwrap(); assert_eq!(lts.num_of_states(), 74); assert_eq!(lts.num_of_transitions(), 92); @@ -335,17 +334,17 @@ mod tests { #[cfg_attr(miri, ignore)] // Oxidd does not work with miri fn test_random_convert_symbolic_lts_bdd() { random_test(100, |rng| { - let mut storage = Storage::new(); + let ldd_manager = oxidd::ldd::new_manager(2048, 1024, 1); - let lts = random_symbolic_lts(rng, &mut storage, 10, 5).unwrap(); + let lts = random_symbolic_lts(rng, &ldd_manager, 10, 5).unwrap(); let mut builder = LtsBuilderMem::new(Vec::new(), Vec::new()); - let explicit_lts = convert_symbolic_lts(&mut storage, &mut builder, <s).unwrap(); + let explicit_lts = convert_symbolic_lts(&ldd_manager, &mut builder, <s).unwrap(); - let manager_ref = oxidd::bdd::new_manager(2028, 2028, 1); - let lts_bdd = SymbolicLtsBdd::from_symbolic_lts(&mut storage, &manager_ref, <s).unwrap(); + let bdd_manager = oxidd::bdd::new_manager(2028, 2028, 1); + let lts_bdd = SymbolicLtsBdd::from_symbolic_lts(&ldd_manager, &bdd_manager, <s).unwrap(); let mut builder = LtsBuilderMem::new(Vec::new(), Vec::new()); - let explicit_lts_bdd = convert_symbolic_lts_bdd(&manager_ref, &mut builder, <s_bdd).unwrap(); + let explicit_lts_bdd = convert_symbolic_lts_bdd(&bdd_manager, &mut builder, <s_bdd).unwrap(); assert!( compare_lts( diff --git a/crates/symbolic/src/convert_ldd.rs b/crates/symbolic/src/convert_ldd.rs index c086aca89..49175b998 100644 --- a/crates/symbolic/src/convert_ldd.rs +++ b/crates/symbolic/src/convert_ldd.rs @@ -1,6 +1,7 @@ use log::debug; use log::info; use log::trace; +use oxidd::ldd::LDDManagerRef; use rustc_hash::FxBuildHasher; use rustc_hash::FxHashSet; use streaming_iterator::StreamingIterator; @@ -8,16 +9,14 @@ use streaming_iterator::StreamingIterator; use merc_collections::IndexedSet; use merc_io::LargeFormatter; use merc_io::TimeProgress; -use merc_ldd::Storage; -use merc_ldd::height; -use merc_ldd::iterators::iter; -use merc_ldd::len; use merc_lts::LtsBuilder; use merc_lts::StateIndex; use merc_utilities::MercError; use crate::SymbolicLTS; use crate::TransitionGroup; +use crate::height; +use crate::iter; /// Converts a symbolic BDD LTS to an explicit LTS. /// @@ -26,7 +25,7 @@ use crate::TransitionGroup; /// This basically applies the symbolic transitions to every state in the state /// space, and constructs the explicit LTS. pub fn convert_symbolic_lts, L: SymbolicLTS>( - storage: &mut Storage, + manager: &LDDManagerRef, output: &mut B, lts: &L, ) -> Result { @@ -49,7 +48,7 @@ pub fn convert_symbolic_lts, L: SymbolicLTS>( } // Total number of states for progress reporting. - let total_number_of_states = len(storage, lts.states()); + let total_number_of_states = lts.states().len(); info!( "Converting symbolic LTS to explicit LTS with {} states", LargeFormatter(total_number_of_states) @@ -68,8 +67,8 @@ pub fn convert_symbolic_lts, L: SymbolicLTS>( // All states have been explored, so add them to the discovered set immediately. let mut discovered: IndexedSet, FxBuildHasher> = IndexedSet::new(); - let mut state_iter = iter(storage, lts.states()); - while let Some(state) = state_iter.next() { + let mut all_states_iter = iter(lts.states()); + while let Some(state) = all_states_iter.next() { let (_, inserted) = discovered.insert(state.clone()); debug_assert!(inserted, "State space contains duplicate states"); state_progress.print(discovered.len()) @@ -92,9 +91,9 @@ pub fn convert_symbolic_lts, L: SymbolicLTS>( let mut outgoing = FxHashSet::default(); // Avoid reallocations. - let mut target = vec![0u32; height(storage, lts.states())]; + let mut target = vec![0u32; height(manager, lts.states())]; - let mut state_iter = iter(storage, lts.states()); + let mut state_iter = iter(lts.states()); let mut index: usize = 0; while let Some(state) = state_iter.next() { @@ -105,7 +104,7 @@ pub fn convert_symbolic_lts, L: SymbolicLTS>( // Apply every transition group to this state. for (group_index, group) in lts.transition_groups().iter().enumerate() { - let mut iter_transitions = iter(storage, group.relation()); + let mut iter_transitions = iter(group.relation()); 'skip: while let Some(transition) = iter_transitions.next() { // Try to match the read parameters of this vector. for (index, i) in group.read_indices().iter().enumerate() { @@ -154,7 +153,7 @@ pub fn convert_symbolic_lts, L: SymbolicLTS>( } // Find the initial state. - let mut state_iter = iter(storage, lts.initial_state()); + let mut state_iter = iter(lts.initial_state()); let initial_state = state_iter.next().ok_or("Symbolic LTS has no initial state")?; let initial_state_index = discovered @@ -204,7 +203,6 @@ fn compute_positions(group: &G) -> (Vec, Vec) #[cfg(test)] mod tests { - use merc_ldd::Storage; use merc_lts::LTS; use merc_lts::LtsBuilderMem; use merc_utilities::test_logger; @@ -219,11 +217,11 @@ mod tests { let input = include_bytes!("../../../examples/lts/abp.sym"); - let mut storage = Storage::new(); - let symbolic_lts = read_symbolic_lts(&mut storage, &input[..]).unwrap(); + let manager = oxidd::ldd::new_manager(2048, 1024, 1); + let symbolic_lts = read_symbolic_lts(&manager, &input[..]).unwrap(); let mut builder = LtsBuilderMem::new(Vec::new(), Vec::new()); - let lts = convert_symbolic_lts(&mut storage, &mut builder, &symbolic_lts).unwrap(); + let lts = convert_symbolic_lts(&manager, &mut builder, &symbolic_lts).unwrap(); debug_assert_eq!(lts.num_of_states(), 74); debug_assert_eq!(lts.num_of_transitions(), 92); diff --git a/crates/symbolic/src/cube_iter_ldd.rs b/crates/symbolic/src/cube_iter_ldd.rs new file mode 100644 index 000000000..35486933d --- /dev/null +++ b/crates/symbolic/src/cube_iter_ldd.rs @@ -0,0 +1,200 @@ +use oxidd::ldd::LDDFunction; +use oxidd::ldd::Value; +use streaming_iterator::StreamingIterator; + +/// Owned `(value, down, right)` triple of an LDD node. +pub struct Data(pub Value, pub LDDFunction, pub LDDFunction); + +// Returns an iterator over all right siblings of the given LDD. +pub fn iter_right(ldd: &LDDFunction) -> IterRight { + IterRight { current: ldd.clone() } +} + +// Returns an iterator over all vectors contained in the given LDD. +pub fn iter(ldd: &LDDFunction) -> Iter { + if ldd.node().is_none() { + // Either the empty set or the empty vector, both contain no + // non-trivial vectors to iterate. + Iter { + vector: Vec::new(), + current: Vec::new(), + stack: Vec::new(), + finished: false, + } + } else { + Iter { + vector: Vec::new(), + current: Vec::new(), + stack: vec![ldd.clone()], + finished: false, + } + } +} + +// Returns an iterator over all nodes in the given LDD. Visits each node only if the predicate holds. +pub fn iter_nodes

(ldd: &LDDFunction, filter: P) -> IterNode

+where + P: Fn(&LDDFunction) -> bool, +{ + let mut stack = Vec::new(); + + // Skip terminals (empty set / empty vector); they have no node data. + if ldd.node().is_some() { + stack.push((ldd.clone(), false)); + } + + IterNode { + stack, + predicate: filter, + } +} + +pub struct IterNode

+where + P: Fn(&LDDFunction) -> bool, +{ + stack: Vec<(LDDFunction, bool)>, + predicate: P, +} + +impl

Iterator for IterNode

+where + P: Fn(&LDDFunction) -> bool, +{ + type Item = (LDDFunction, Data); + + fn next(&mut self) -> Option { + while let Some((current, visited)) = self.stack.pop() { + let (value, down, right) = current.node().expect("only inner nodes are pushed onto the stack"); + + if visited { + return Some((current, Data(value, down, right))); + } + + // Next time we can actually process the current node. + self.stack.push((current.clone(), true)); + + // Add unvisited children to stack + if (self.predicate)(&down) { + self.stack.push((down, false)); + } + + if (self.predicate)(&right) { + self.stack.push((right, false)); + } + } + + None + } +} + +pub struct IterRight { + current: LDDFunction, +} + +impl Iterator for IterRight { + type Item = Data; + + fn next(&mut self) -> Option { + match self.current.node() { + // Reached the empty set (or empty vector), so iteration stops. + None => None, + Some((value, down, right)) => { + // Progress to the right LDD. + self.current = right.clone(); + Some(Data(value, down, right)) + } + } + } +} + +pub struct Iter { + /// Stores the values of the returned vector. + vector: Vec, + /// Stores the current path in the LDD. + current: Vec, + /// Stores the stack for the depth-first search (only non 'true' or 'false' nodes) + stack: Vec, + /// Indicates whether the iteration is finished. + finished: bool, +} + +impl StreamingIterator for Iter { + type Item = Vec; + + fn advance(&mut self) { + // Find the next vector by going down the chain. + loop { + if let Some(current) = self.stack.last() { + let (value, down, _) = current.node().expect("only inner nodes are pushed onto the stack"); + self.vector.push(value); + if down.is_empty_vector() { + self.current.clear(); + self.current.extend_from_slice(&self.vector); + break; // Stop iteration. + } else { + self.stack.push(down); + } + } else { + // No more elements to iterate. + self.finished = true; + return; + } + } + + // Go up the chain to find the next right sibling that is not 'false'. + while let Some(current) = self.stack.pop() { + self.vector.pop(); + let (_, _, right) = current.node().expect("only inner nodes are pushed onto the stack"); + + if !right.is_empty() { + self.stack.push(right); // This is the first right sibling. + break; + } + } + } + + fn get(&self) -> Option<&Self::Item> { + if self.finished { None } else { Some(&self.current) } + } +} + +#[cfg(test)] +mod tests { + + use super::*; + + use merc_utilities::random_test; + + use crate::from_iter; + use crate::random_vector_set; + + // Test the iterator implementation. + #[test] + #[cfg_attr(miri, ignore)] + fn test_random_iter() { + random_test(100, |rng| { + let manager = oxidd::ldd::new_manager(2048, 1024, 1); + + let set = random_vector_set(rng, 32, 10, 10); + let ldd = from_iter(&manager, set.iter()); + + assert!( + iter(&ldd).count() == set.len(), + "Number of iterations does not match the number of elements in the set." + ); + + let mut results: Vec> = Vec::new(); + let mut it = iter(&ldd); + while let Some(vector) = it.next() { + assert!(set.contains(vector), "Found element not in the set."); + results.push(vector.to_vec()); + } + + results.sort(); + let original_len = results.len(); + results.dedup(); + assert_eq!(original_len, results.len(), "iter returned duplicate vectors."); + }) + } +} diff --git a/crates/ldd/src/format.rs b/crates/symbolic/src/display.rs similarity index 60% rename from crates/ldd/src/format.rs rename to crates/symbolic/src/display.rs index a6bccf4d0..1cf2d69f5 100644 --- a/crates/ldd/src/format.rs +++ b/crates/symbolic/src/display.rs @@ -1,22 +1,22 @@ -use itertools::Itertools; use std::collections::HashSet; use std::fmt; + +use itertools::Itertools; +use oxidd::ldd::LDDFunction; use streaming_iterator::StreamingIterator; use crate::Data; -use crate::Ldd; -use crate::Storage; -use crate::iterators::*; +use crate::iter; +use crate::iter_right; /// Helper struct for displaying LDDs in DOT format. pub struct LddDot<'a> { - storage: &'a Storage, - ldd: &'a Ldd, + ldd: &'a LDDFunction, } impl<'a> LddDot<'a> { - pub fn new(storage: &'a Storage, ldd: &'a Ldd) -> LddDot<'a> { - LddDot { storage, ldd } + pub fn new(ldd: &'a LDDFunction) -> LddDot<'a> { + LddDot { ldd } } } @@ -35,17 +35,17 @@ impl fmt::Display for LddDot<'_> { // Every node must be printed once, so keep track of already printed ones. #[allow(clippy::mutable_key_type)] - let mut marked: HashSet = HashSet::new(); + let mut marked: HashSet = HashSet::new(); // We don't show these nodes in the output since every right most node is 'false' and every bottom node is 'true'. // or in our terms empty_set and empty_vector. However, if the LDD itself is 'false' or 'true' we just show the single // node for clarity. - if self.ldd == self.storage.empty_set() { + if self.ldd.is_empty() { writeln!(f, "0 [shape=record, label=\"False\"];")?; - } else if self.ldd == self.storage.empty_vector() { + } else if self.ldd.is_empty_vector() { writeln!(f, "1 [shape=record, label=\"True\"];")?; } else { - print_node(self.storage, f, &mut marked, self.ldd)?; + print_node(f, &mut marked, self.ldd)?; } writeln!(f, "}}") @@ -54,13 +54,12 @@ impl fmt::Display for LddDot<'_> { /// Helper struct for displaying LDDs. pub struct LddDisplay<'a> { - storage: &'a Storage, - ldd: &'a Ldd, + ldd: &'a LDDFunction, } impl<'a> LddDisplay<'a> { - pub fn new(storage: &'a Storage, ldd: &'a Ldd) -> LddDisplay<'a> { - LddDisplay { storage, ldd } + pub fn new(ldd: &'a LDDFunction) -> LddDisplay<'a> { + LddDisplay { ldd } } } @@ -68,7 +67,7 @@ impl fmt::Display for LddDisplay<'_> { fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result { writeln!(f, "{{")?; - let mut iter = iter(self.storage, self.ldd); + let mut iter = iter(self.ldd); while let Some(vector) = iter.next() { writeln!(f, "\t[{}]", vector.iter().format(" "))?; } @@ -77,15 +76,15 @@ impl fmt::Display for LddDisplay<'_> { } #[allow(clippy::mutable_key_type)] -fn print_node(storage: &Storage, f: &mut fmt::Formatter<'_>, marked: &mut HashSet, ldd: &Ldd) -> fmt::Result { - if marked.contains(ldd) || ldd == storage.empty_set() || ldd == storage.empty_vector() { +fn print_node(f: &mut fmt::Formatter<'_>, marked: &mut HashSet, ldd: &LDDFunction) -> fmt::Result { + if marked.contains(ldd) || ldd.is_empty() || ldd.is_empty_vector() { Ok(()) } else { // Print the node values - write!(f, "{} [shape=record, label=\"", ldd.index())?; + write!(f, "{} [shape=record, label=\"", ldd.id())?; let mut first = true; - for Data(value, _, _) in iter_right(storage, ldd) { + for Data(value, _, _) in iter_right(ldd) { if !first { write!(f, "|")?; } @@ -96,22 +95,22 @@ fn print_node(storage: &Storage, f: &mut fmt::Formatter<'_>, marked: &mut HashSe writeln!(f, "\"];")?; // Print the edges. - for Data(value, down, _) in iter_right(storage, ldd) { - if down != *storage.empty_set() && down != *storage.empty_vector() { + for Data(value, down, _) in iter_right(ldd) { + if !down.is_empty() && !down.is_empty_vector() { writeln!( f, "{}:{} -> {}:{};", - ldd.index(), + ldd.id(), value, - down.index(), - storage.get_ref(&down).0 + down.id(), + down.node().expect("down is an inner node").0 )?; } } // Print all nodes. - for Data(_, down, _) in iter_right(storage, ldd) { - print_node(storage, f, marked, &down)?; + for Data(_, down, _) in iter_right(ldd) { + print_node(f, marked, &down)?; } Ok(()) diff --git a/crates/ldd/src/io_ldd.rs b/crates/symbolic/src/io_ldd.rs similarity index 77% rename from crates/ldd/src/io_ldd.rs rename to crates/symbolic/src/io_ldd.rs index cbe71c111..4b301ac44 100644 --- a/crates/ldd/src/io_ldd.rs +++ b/crates/symbolic/src/io_ldd.rs @@ -9,6 +9,9 @@ use std::cell::RefCell; +use oxidd::ldd::LDDFunction; +use oxidd::ldd::LDDManagerRef; + use merc_aterm::ATerm; use merc_aterm::ATermRead; use merc_collections::IndexedSet; @@ -18,9 +21,7 @@ use merc_number::bits_for_value; use merc_utilities::MercError; use crate::Data; -use crate::Ldd; -use crate::Storage; -use crate::iterators::iter_nodes; +use crate::iter_nodes; /// The magic value for a binary LDD format stream. const BLF_MAGIC: u64 = 0x8baf; @@ -29,19 +30,19 @@ const BLF_VERSION: u64 = 0x8306; /// \brief Writes ldds in a streamable binary format to an output stream. pub struct BinaryLddWriter { writer: W, - nodes: RefCell>, + nodes: RefCell>, } impl BinaryLddWriter { - pub fn new(storage: &mut Storage, mut writer: W) -> Result { + pub fn new(manager: &LDDManagerRef, mut writer: W) -> Result { // Write the header of the binary LDD format. writer.write_bits(BLF_MAGIC, 16)?; writer.write_bits(BLF_VERSION, 16)?; // Add the true and false constants let mut nodes = IndexedSet::new(); - nodes.insert(storage.empty_set().clone()); - nodes.insert(storage.empty_vector().clone()); + nodes.insert(LDDFunction::empty_set(manager)?); + nodes.insert(LDDFunction::empty_vector(manager)?); Ok(Self { writer, @@ -50,8 +51,8 @@ impl BinaryLddWriter { } /// Writes an LDD to the stream. - pub fn write_ldd(&mut self, ldd: &Ldd, storage: &Storage) -> Result<(), MercError> { - for (node, Data(value, down, right)) in iter_nodes(storage, ldd, |node| { + pub fn write_ldd(&mut self, ldd: &LDDFunction, _manager: &LDDManagerRef) -> Result<(), MercError> { + for (node, Data(value, down, right)) in iter_nodes(ldd, |node| { // Skip any LDD that we have already inserted in the stream !self.nodes.borrow().contains(node) }) { @@ -88,19 +89,19 @@ impl BinaryLddWriter { /// Returns the number of bits required to represent an LDD index. /// This matches the reader: when writing a node definition we've already /// inserted the current node, so we use the current number of nodes. - fn ldd_index_width(nodes: &IndexedSet) -> u8 { + fn ldd_index_width(nodes: &IndexedSet) -> u8 { bits_for_value(nodes.len()) } } pub struct BinaryLddReader { reader: R, - nodes: Vec, + nodes: Vec, } impl BinaryLddReader { /// Inserts the header into the stream and initializes the reader. - pub fn new(storage: &mut Storage, mut reader: R) -> Result { + pub fn new(storage: &LDDManagerRef, mut reader: R) -> Result { // Read and verify the header of the binary LDD format. let magic = reader.read_bits(16)?; if magic != BLF_MAGIC { @@ -113,12 +114,12 @@ impl BinaryLddReader { } // Add the true and false constants - let nodes = vec![storage.empty_set().clone(), storage.empty_vector().clone()]; + let nodes = vec![LDDFunction::empty_set(storage)?, LDDFunction::empty_vector(storage)?]; Ok(Self { reader, nodes }) } /// Reads an LDD from the stream. - pub fn read_ldd(&mut self, storage: &mut Storage) -> Result { + pub fn read_ldd(&mut self, storage: &LDDManagerRef) -> Result { loop { let is_output = self.reader.read_bits(1)? == 1; @@ -135,17 +136,23 @@ impl BinaryLddReader { let value = self.reader.read_integer()?; let down_index = self.reader.read_bits(self.ldd_index_width(true))? as usize; let right_index = self.reader.read_bits(self.ldd_index_width(true))? as usize; - let ldd = storage.insert( - value as u32, - self.nodes.get(down_index).ok_or(format!( + let down = self + .nodes + .get(down_index) + .ok_or(format!( "Read invalid down ldd index {down_index}, length {}", self.nodes.len() - ))?, - self.nodes.get(right_index).ok_or(format!( + ))? + .clone(); + let right = self + .nodes + .get(right_index) + .ok_or(format!( "Read invalid right ldd index {right_index}, length {}", self.nodes.len() - ))?, - ); + ))? + .clone(); + let ldd = LDDFunction::make_node(storage, value as u32, &down, &right)?; self.nodes.push(ldd); } } @@ -181,8 +188,8 @@ mod tests { use merc_io::BitStreamWriter; use merc_utilities::random_test; - use crate::test_utility::from_iter; - use crate::test_utility::random_vector_set; + use crate::from_iter; + use crate::random_vector_set; use super::*; @@ -190,29 +197,28 @@ mod tests { #[cfg_attr(miri, ignore)] fn test_binary_ldd_stream() { random_test(100, |rng| { - let mut storage = Storage::new(); + let manager = oxidd::ldd::new_manager(2048, 1024, 1); let input: Vec<_> = (0..20) .map(|_| { let input = random_vector_set(rng, 32, 10, 10); - from_iter(&mut storage, input.iter()) + from_iter(&manager, input.iter()) }) .collect(); let mut vector: Vec = Vec::new(); let stream = BitStreamWriter::new(&mut vector); - let mut output_stream = BinaryLddWriter::new(&mut storage, stream).unwrap(); + let mut output_stream = BinaryLddWriter::new(&manager, stream).unwrap(); for term in &input { - output_stream.write_ldd(term, &storage).unwrap(); + output_stream.write_ldd(term, &manager).unwrap(); } drop(output_stream); // Explicitly drop to release the mutable borrow - let mut input_stream = BinaryLddReader::new(&mut storage, BitStreamReader::new(&vector[..])).unwrap(); + let mut input_stream = BinaryLddReader::new(&manager, BitStreamReader::new(&vector[..])).unwrap(); for term in &input { - debug_assert_eq!( - *term, - input_stream.read_ldd(&mut storage).unwrap(), + assert!( + *term == input_stream.read_ldd(&manager).unwrap(), "The read LDD must match the LDD that we have written" ); } diff --git a/crates/symbolic/src/io_sylvan.rs b/crates/symbolic/src/io_sylvan.rs index 265bab43d..dc31e492d 100644 --- a/crates/symbolic/src/io_sylvan.rs +++ b/crates/symbolic/src/io_sylvan.rs @@ -1,47 +1,47 @@ +use std::collections::HashMap; use std::fmt; use std::io::Read; use log::info; use merc_data::DataExpression; -use merc_ldd::Ldd; -use merc_ldd::Storage; -use merc_ldd::SylvanReader; -use merc_ldd::Value; -use merc_ldd::compute_meta; -use merc_ldd::read_u32; use merc_utilities::MercError; +use oxidd::ldd::LDDFunction; +use oxidd::ldd::LDDManagerRef; +use oxidd::ldd::Value; use crate::SymbolicLTS; use crate::TransitionGroup; /// Returns the (initial state, transitions) read from the file in Sylvan's format. -pub fn read_sylvan(storage: &mut Storage, stream: &mut R) -> Result { +pub fn read_sylvan(manager: &LDDManagerRef, stream: &mut R) -> Result { info!("Reading symbolic LTS in Sylvan format..."); let mut reader = SylvanReader::new(); let _vector_length = read_u32(stream)?; let _unused = read_u32(stream)?; // This is called 'k' in Sylvan's ldd2bdd.c, but unused. - let initial_state = reader.read_ldd(storage, stream)?; + let initial_state = reader.read_ldd(manager, stream)?; let num_transitions: usize = read_u32(stream)? as usize; let mut groups: Vec = Vec::new(); // Read all the transition groups. for _ in 0..num_transitions { let (read_proj, write_proj) = read_projection(stream)?; + + let meta = LDDFunction::relation_product_meta(manager, &read_proj, &write_proj)?.0; groups.push(SylvanTransitionGroup::new( - storage.empty_set().clone(), - compute_meta(storage, &read_proj, &write_proj).0, + LDDFunction::empty_set(manager)?, + meta, read_proj, write_proj, )); } for transition in groups.iter_mut().take(num_transitions) { - transition.relation = reader.read_ldd(storage, stream)?; + transition.relation = reader.read_ldd(manager, stream)?; } - Ok(SylvanLts::new(storage.empty_set().clone(), initial_state, groups)) + Ok(SylvanLts::new(LDDFunction::empty_set(manager)?, initial_state, groups)) } /// Reads the read and write projections from the given stream. @@ -68,16 +68,20 @@ pub fn read_projection(file: &mut R) -> Result<(Vec, Vec) /// A symbolic labelled transition system read from a Sylvan file. pub struct SylvanLts { - initial_state: merc_ldd::Ldd, + initial_state: LDDFunction, transition_groups: Vec, // (relation, meta) - empty_set: Ldd, + empty_set: LDDFunction, } impl SylvanLts { /// Creates a new Sylvan LTS. - pub fn new(empty_set: Ldd, initial_state: Ldd, transition_groups: Vec) -> Self { + pub fn new( + empty_set: LDDFunction, + initial_state: LDDFunction, + transition_groups: Vec, + ) -> Self { Self { initial_state, transition_groups, @@ -87,11 +91,11 @@ impl SylvanLts { } impl SymbolicLTS for SylvanLts { - fn states(&self) -> &Ldd { + fn states(&self) -> &LDDFunction { &self.empty_set } - fn initial_state(&self) -> &Ldd { + fn initial_state(&self) -> &LDDFunction { &self.initial_state } @@ -116,15 +120,15 @@ impl SymbolicLTS for SylvanLts { /// A transition group read from a Sylvan file. pub struct SylvanTransitionGroup { - relation: Ldd, - meta: Ldd, + relation: LDDFunction, + meta: LDDFunction, read_proj: Vec, write_proj: Vec, } impl SylvanTransitionGroup { /// Creates a new Sylvan transition group. - pub fn new(relation: Ldd, meta: Ldd, read_proj: Vec, write_proj: Vec) -> Self { + pub fn new(relation: LDDFunction, meta: LDDFunction, read_proj: Vec, write_proj: Vec) -> Self { Self { relation, meta, @@ -135,7 +139,7 @@ impl SylvanTransitionGroup { } impl TransitionGroup for SylvanTransitionGroup { - fn relation(&self) -> &Ldd { + fn relation(&self) -> &LDDFunction { &self.relation } @@ -151,11 +155,11 @@ impl TransitionGroup for SylvanTransitionGroup { None } - fn meta(&self) -> &Ldd { + fn meta(&self) -> &LDDFunction { &self.meta } - fn learn_successors(&mut self, _storage: &mut Storage, _todo: &Ldd) -> Result<(), MercError> { + fn learn_successors(&mut self, _manager: &LDDManagerRef, _todo: &LDDFunction) -> Result<(), MercError> { // All states are already explored. Ok(()) } @@ -170,31 +174,117 @@ impl fmt::Debug for SylvanTransitionGroup { } } +/// A reader for LDDs in the Sylvan .ldd format. +pub struct SylvanReader { + indexed_set: HashMap, // Assigns LDDs to every index. + last_index: u64, // The index of the last LDD read from file. +} + +impl SylvanReader { + pub fn new() -> Self { + Self { + indexed_set: HashMap::new(), + last_index: 2, + } + } + + /// Returns an LDD read from the given stream in the Sylvan format. + pub fn read_ldd(&mut self, manager: &LDDManagerRef, stream: &mut R) -> Result { + let count = read_u64(stream)?; + //println!("node count = {}", count); + + for _ in 0..count { + // Read a single MDD node. It has the following structure: u64 | u64 + // RmRR RRRR RRRR VVVV | VVVV DcDD DDDD DDDD (little endian) + // Every character is 4 bits, V = value, D = down, R = right, m = marked, c = copy. + let a = read_u64(stream)?; + let b = read_u64(stream)?; + //println!("{:064b} | {:064b}", a, b); + + let right = (a & 0x0000ffffffffffff) >> 1; + let down = b >> 17; + + let mut bytes: [u8; 4] = Default::default(); + bytes[0..2].copy_from_slice(&a.to_le_bytes()[6..8]); + bytes[2..4].copy_from_slice(&b.to_le_bytes()[0..2]); + let value = u32::from_le_bytes(bytes); + + let copy = right & 0x10000; + if copy != 0 { + panic!("We do not yet deal with copy nodes."); + } + + let down = self.node_from_index(manager, down)?; + let right = self.node_from_index(manager, right)?; + + let ldd = LDDFunction::make_node(manager, value as Value, &down, &right)?; + self.indexed_set.insert(self.last_index, ldd); + + self.last_index += 1; + } + + let result = read_u64(stream)?; + self.node_from_index(manager, result) + } + + /// Returns the LDD belonging to the given index. + fn node_from_index(&self, manager: &LDDManagerRef, index: u64) -> Result { + if index == 0 { + Ok(LDDFunction::empty_set(manager)?) + } else if index == 1 { + Ok(LDDFunction::empty_vector(manager)?) + } else { + Ok(self.indexed_set.get(&index).unwrap().clone()) + } + } +} + +impl Default for SylvanReader { + fn default() -> Self { + Self::new() + } +} + +/// Returns a single u32 read from the given stream. +pub fn read_u32(stream: &mut R) -> Result { + let mut buffer: [u8; 4] = Default::default(); + stream.read_exact(&mut buffer)?; + + Ok(u32::from_le_bytes(buffer)) +} + +/// Returns a single u64 read from the given stream. +pub fn read_u64(stream: &mut R) -> Result { + let mut buffer: [u8; 8] = Default::default(); + stream.read_exact(&mut buffer)?; + + Ok(u64::from_le_bytes(buffer)) +} + #[cfg(test)] mod test { use merc_utilities::Timing; use crate::reachability; - use super::Storage; use super::read_sylvan; #[test] #[cfg_attr(miri, ignore)] // Miri is too slow fn test_load_anderson_4() { - let mut storage = Storage::new(); + let ldd_manager = oxidd::ldd::new_manager(2048, 1024, 1); let bytes = include_bytes!("../../../examples/ldd/anderson.4.ldd"); - let mut lts = read_sylvan(&mut storage, &mut &bytes[..]).expect("Loading should work correctly"); - reachability(&mut storage, &mut lts, &Timing::new()).expect("Reachability should work correctly"); + let mut lts = read_sylvan(&ldd_manager, &mut &bytes[..]).expect("Loading should work correctly"); + reachability(&ldd_manager, &mut lts, &Timing::new()).expect("Reachability should work correctly"); } #[test] #[cfg_attr(miri, ignore)] // Miri is too slow #[cfg(not(debug_assertions))] fn test_load_collision_4() { - let mut storage = Storage::new(); + let ldd_manager = oxidd::ldd::new_manager(2048, 1024, 1); let bytes = include_bytes!("../../../examples/ldd/collision.4.ldd"); - let mut lts = read_sylvan(&mut storage, &mut &bytes[..]).expect("Loading should work correctly"); - reachability(&mut storage, &mut lts, &Timing::new()).expect("Reachability should work correctly"); + let mut lts = read_sylvan(&ldd_manager, &mut &bytes[..]).expect("Loading should work correctly"); + reachability(&ldd_manager, &mut lts, &Timing::new()).expect("Reachability should work correctly"); } } diff --git a/crates/symbolic/src/io_symbolic_lts.rs b/crates/symbolic/src/io_symbolic_lts.rs index 073680cd9..518796b44 100644 --- a/crates/symbolic/src/io_symbolic_lts.rs +++ b/crates/symbolic/src/io_symbolic_lts.rs @@ -13,11 +13,11 @@ use merc_data::DataExpression; use merc_data::DataSpecification; use merc_data::DataVariable; use merc_io::BitStreamRead; -use merc_ldd::BinaryLddReader; -use merc_ldd::Storage; use merc_lts::LtsMultiAction; use merc_utilities::MercError; +use oxidd::ldd::LDDManagerRef; +use crate::BinaryLddReader; use crate::SummandGroup; use crate::SymbolicLts; @@ -54,11 +54,11 @@ use crate::SymbolicLts; /// For each write parameter: /// : ATerm /// ``` -pub fn read_symbolic_lts(storage: &mut Storage, reader: R) -> Result { +pub fn read_symbolic_lts(manager: &LDDManagerRef, reader: R) -> Result { info!("Reading symbolic LTS in the mCRL2 symbolic format..."); let aterm_stream = BinaryATermReader::new(BufReader::new(reader))?; - let mut stream = BinaryLddReader::new(storage, aterm_stream)?; + let mut stream = BinaryLddReader::new(manager, aterm_stream)?; if ATermRead::read_aterm(&mut stream)? != Some(symbolic_labelled_transition_system_mark()) { return Err("Expected symbolic labelled transition system stream".into()); @@ -68,8 +68,8 @@ pub fn read_symbolic_lts(storage: &mut Storage, reader: R) -> Result = stream.read_aterm()?.ok_or("Expected process parameters")?.into(); let process_parameters: Vec = process_parameters.to_vec(); - let initial_state = stream.read_ldd(storage)?; - let states = stream.read_ldd(storage)?; + let initial_state = stream.read_ldd(manager)?; + let states = stream.read_ldd(manager)?; // Read the values for the process parameters. let mut parameter_values: Vec> = Vec::with_capacity(process_parameters.len()); @@ -122,10 +122,10 @@ pub fn read_symbolic_lts(storage: &mut Storage, reader: R) -> Result, - bits_per_layer: &LddRef<'_>, + _ldd_manager_ref: &LDDManagerRef, + bdd_manager_ref: &BDDManagerRef, + ldd: &LDDFunction, + bits_per_layer: &LDDFunction, bit_variables: &[VarNo], ) -> Result { // For LDDs we can assume that nodes in one layer are unique, so we don't // need the bits_per_layer and bit_variables in the cache. let mut cache = FxHashMap::default(); - manager_ref.with_manager_shared(|manager| -> Result { + bdd_manager_ref.with_manager_shared(|bdd_manager| -> Result { Ok(BDDFunction::from_edge( - manager, - ldd_to_bdd_edge(storage, manager, &mut cache, ldd, bits_per_layer, bit_variables)?, + bdd_manager, + ldd_to_bdd_edge(bdd_manager, &mut cache, ldd, bits_per_layer, bit_variables)?, )) }) } @@ -59,32 +54,31 @@ pub fn ldd_to_bdd( /// Recursive implementation of [ldd_to_bdd]. #[allow(clippy::mutable_key_type)] pub fn ldd_to_bdd_edge<'id>( - storage: &mut Storage, - manager: &::Manager<'id>, - cache: &mut FxHashMap, - ldd: &LddRef<'_>, - bits_per_layer: &LddRef<'_>, + bdd_manager: &::Manager<'id>, + cache: &mut FxHashMap, + ldd: &LDDFunction, + bits_per_layer: &LDDFunction, bit_variables: &[VarNo], ) -> Result, OutOfMemory> { // Base cases - if **storage.empty_set() == *ldd { - return manager.get_terminal(BDDTerminal::False); + if ldd.is_empty() { + return bdd_manager.get_terminal(BDDTerminal::False); } - if **storage.empty_vector() == *ldd { - return manager.get_terminal(BDDTerminal::True); + if ldd.is_empty_vector() { + return bdd_manager.get_terminal(BDDTerminal::True); } if let Some(cached) = cache.get(ldd) { - return Ok(manager.clone_edge(cached.as_edge(manager))); + return Ok(bdd_manager.clone_edge(cached.as_edge(bdd_manager))); } - let DataRef(value, down, right) = storage.get_ref(ldd); - let DataRef(bits_value, bits_down, _bits_right) = storage.get_ref(bits_per_layer); + let (value, down, right) = ldd.node().expect("ldd is an inner node"); + let (bits_value, bits_down, _bits_right) = bits_per_layer.node().expect("bits_per_layer is an inner node"); // Right branch does not consume variables at this layer let right_bdd = EdgeDropGuard::new( - manager, - ldd_to_bdd_edge(storage, manager, cache, &right, bits_per_layer, bit_variables)?, + bdd_manager, + ldd_to_bdd_edge(bdd_manager, cache, &right, bits_per_layer, bit_variables)?, ); // Ensure we have enough variables for this layer @@ -98,54 +92,53 @@ pub fn ldd_to_bdd_edge<'id>( // Recurse on down with the remaining variables after consuming this layer let mut down_bdd = EdgeDropGuard::new( - manager, - ldd_to_bdd_edge( - storage, - manager, - cache, - &down, - &bits_down, - &bit_variables[needed_bits..], - )?, + bdd_manager, + ldd_to_bdd_edge(bdd_manager, cache, &down, &bits_down, &bit_variables[needed_bits..])?, ); // Encode current value using the variables for this layer (MSB to LSB) // Current layer variables: vars[0..bits_value] // The `ite` is necessary since the variables are not in sorted order. - let f_edge = EdgeDropGuard::new(manager, manager.get_terminal(BDDTerminal::False)?); + let f_edge = EdgeDropGuard::new(bdd_manager, bdd_manager.get_terminal(BDDTerminal::False)?); for i in 0..bits_value { let bit = bits_value - i - 1; // MSB first let var_no = bit_variables[bit as usize]; - let var = EdgeDropGuard::new(manager, BDDFunction::var_edge(manager, var_no)?); + let var = EdgeDropGuard::new(bdd_manager, BDDFunction::var_edge(bdd_manager, var_no)?); if value & (1 << i) != 0 { // bit is 1 - down_bdd = EdgeDropGuard::new(manager, BDDFunction::ite_edge(manager, &var, &down_bdd, &f_edge)?); + down_bdd = EdgeDropGuard::new( + bdd_manager, + BDDFunction::ite_edge(bdd_manager, &var, &down_bdd, &f_edge)?, + ); } else { // bit is 0 - down_bdd = EdgeDropGuard::new(manager, BDDFunction::ite_edge(manager, &var, &f_edge, &down_bdd)?); + down_bdd = EdgeDropGuard::new( + bdd_manager, + BDDFunction::ite_edge(bdd_manager, &var, &f_edge, &down_bdd)?, + ); } } - let result = BDDFunction::or_edge(manager, &down_bdd, &right_bdd)?; - cache.insert(storage.protect(ldd), BDDFunction::from_edge_ref(manager, &result)); + let result = BDDFunction::or_edge(bdd_manager, &down_bdd, &right_bdd)?; + cache.insert(ldd.clone(), BDDFunction::from_edge_ref(bdd_manager, &result)); Ok(result) } /// Converts a BDD representing a set of bitblasted vectors back into an LDD /// representing the same set, i.e., the inverse of [ldd_to_bdd]. pub fn bdd_to_ldd( - storage: &mut Storage, + ldd_manager: &LDDManagerRef, manager_ref: &BDDManagerRef, bdd: &BDDFunction, variables: &[VarNo], bits_per_layer: &[Value], current_bit: Value, current_value: Value, -) -> Result { +) -> Result { manager_ref.with_manager_shared(|manager| { let edge = bdd.as_edge(manager); bdd_to_ldd_edge( - storage, + ldd_manager, manager, edge.borrowed(), variables, @@ -158,21 +151,21 @@ pub fn bdd_to_ldd( /// Recursive implementation of [bdd_to_ldd]. pub fn bdd_to_ldd_edge<'id>( - storage: &mut Storage, + ldd_manager: &LDDManagerRef, manager: &::Manager<'id>, bdd: Borrowed>, variables: &[VarNo], bits_per_layer: &[Value], current_bit: Value, current_value: Value, -) -> Result { +) -> Result { let bdd_node = match manager.get_node(&bdd) { oxidd::Node::Inner(node) => node, oxidd::Node::Terminal(terminal) => { // Base cases match terminal { BDDTerminal::False => { - return Ok(storage.empty_set().clone()); + return LDDFunction::empty_set(ldd_manager); } BDDTerminal::True => { if !variables.is_empty() { @@ -185,14 +178,15 @@ pub fn bdd_to_ldd_edge<'id>( // There are don't care variables in this BDD that have been skipped, so generate both branches. if num_bits == current_bit { // We reached the last bit for this layer, variable still belongs to next layer. - let down = bdd_to_ldd_edge(storage, manager, bdd, variables, &bits_per_layer[1..], 0, 0)?; - let right = storage.empty_set().clone(); - return Ok(storage.insert(current_value, &down, &right)); + let down = + bdd_to_ldd_edge(ldd_manager, manager, bdd, variables, &bits_per_layer[1..], 0, 0)?; + let right = LDDFunction::empty_set(ldd_manager)?; + return LDDFunction::make_node(ldd_manager, current_value, &down, &right); } debug_assert!(current_bit < num_bits, "Current bit exceeds number of bits for layer"); let high = bdd_to_ldd_edge( - storage, + ldd_manager, manager, bdd.borrowed(), &variables[1..], @@ -201,7 +195,7 @@ pub fn bdd_to_ldd_edge<'id>( current_value | (1 << (num_bits - current_bit - 1)), )?; let low = bdd_to_ldd_edge( - storage, + ldd_manager, manager, bdd, &variables[1..], @@ -209,10 +203,10 @@ pub fn bdd_to_ldd_edge<'id>( current_bit + 1, current_value, )?; - return Ok(union(storage, &high, &low)); + return high.union(&low); } - return Ok(storage.insert_singleton(current_value)); + return LDDFunction::singleton(ldd_manager, &[current_value]); } } } @@ -231,14 +225,14 @@ pub fn bdd_to_ldd_edge<'id>( // There are don't care variables in this BDD that have been skipped, so generate both branches without cofactors. if num_bits == current_bit { // We reached the last bit for this layer, variable still belongs to next layer. - let down = bdd_to_ldd_edge(storage, manager, bdd, variables, &bits_per_layer[1..], 0, 0)?; - let right = storage.empty_set().clone(); - return Ok(storage.insert(current_value, &down, &right)); + let down = bdd_to_ldd_edge(ldd_manager, manager, bdd, variables, &bits_per_layer[1..], 0, 0)?; + let right = LDDFunction::empty_set(ldd_manager)?; + return LDDFunction::make_node(ldd_manager, current_value, &down, &right); } debug_assert!(current_bit < num_bits, "Current bit exceeds number of bits for layer"); let high = bdd_to_ldd_edge( - storage, + ldd_manager, manager, bdd.borrowed(), &variables[1..], @@ -247,7 +241,7 @@ pub fn bdd_to_ldd_edge<'id>( current_value | (1 << (num_bits - current_bit - 1)), )?; let low = bdd_to_ldd_edge( - storage, + ldd_manager, manager, bdd, &variables[1..], @@ -255,23 +249,22 @@ pub fn bdd_to_ldd_edge<'id>( current_bit + 1, current_value, )?; - return Ok(union(storage, &high, &low)); + return high.union(&low); } debug_assert_eq!(*variable_level, bdd_node.level(), "Levels do not match"); if num_bits == current_bit { // We reached the last bit for this layer - let down = bdd_to_ldd_edge(storage, manager, bdd, variables, &bits_per_layer[1..], 0, 0)?; - let right = storage.empty_set().clone(); - Ok(storage.insert(current_value, &down, &right)) + let down = bdd_to_ldd_edge(ldd_manager, manager, bdd, variables, &bits_per_layer[1..], 0, 0)?; + let right = LDDFunction::empty_set(ldd_manager)?; + LDDFunction::make_node(ldd_manager, current_value, &down, &right) } else { - debug_assert!(current_bit < num_bits, "Current bit exceeds number of bits for layer"); debug_assert!(current_bit < num_bits, "Current bit exceeds number of bits for layer"); let (bdd_high, bdd_low) = collect_children(bdd_node); // Recurse for high and low cofactors let high = bdd_to_ldd_edge( - storage, + ldd_manager, manager, bdd_high, &variables[1..], @@ -280,7 +273,7 @@ pub fn bdd_to_ldd_edge<'id>( current_value | (1 << (num_bits - current_bit - 1)), )?; let low = bdd_to_ldd_edge( - storage, + ldd_manager, manager, bdd_low, &variables[1..], @@ -289,14 +282,14 @@ pub fn bdd_to_ldd_edge<'id>( current_value, )?; - Ok(union(storage, &high, &low)) + high.union(&low) } } /// Computes the highest value for every layer in the LDD -pub fn compute_highest(storage: &mut Storage, ldd: &LddRef<'_>) -> Vec { +pub fn compute_highest(storage: &LDDManagerRef, ldd: &LDDFunction) -> Vec { let mut result = vec![0; height(storage, ldd)]; - compute_highest_rec(storage, &mut result, ldd, 0); + compute_highest_rec(&mut result, ldd, 0); result } @@ -362,14 +355,15 @@ pub fn to_value(bits: &[OptBool]) -> u64 { } /// Helper function for compute_highest -fn compute_highest_rec(storage: &mut Storage, result: &mut [u32], set: &LddRef<'_>, depth: usize) { - if set == storage.empty_set() || set == storage.empty_vector() { - return; - } +fn compute_highest_rec(result: &mut [u32], set: &LDDFunction, depth: usize) { + let (value, down, right) = match set.node() { + // Terminals (empty set / empty vector) have no contribution. + None => return, + Some(node) => node, + }; - let DataRef(value, down, right) = storage.get_ref(set); - compute_highest_rec(storage, result, &right, depth); - compute_highest_rec(storage, result, &down, depth + 1); + compute_highest_rec(result, &right, depth); + compute_highest_rec(result, &down, depth + 1); result[depth] = result[depth].max(value); } @@ -394,30 +388,30 @@ pub fn compute_bits(highest: &[u32]) -> Vec { mod tests { use oxidd::Manager; use oxidd::ManagerRef; + use oxidd::ldd::LDDFunction; - use merc_ldd::LddDisplay; - use merc_ldd::Storage; - use merc_ldd::from_iter; - use merc_ldd::random_vector_set; - use merc_ldd::singleton; use merc_utilities::random_test; use crate::FormatConfigSet; + use crate::LddDisplay; use crate::bdd_to_ldd; use crate::compute_bits; use crate::compute_highest; + use crate::from_iter; use crate::ldd_to_bdd; + use crate::random_vector_set; use crate::required_bits; #[test] + #[cfg_attr(miri, ignore)] // Oxidd does not work with miri fn test_random_compute_highest() { random_test(100, |rng| { + let manager = oxidd::ldd::new_manager(2048, 1024, 1); let set = random_vector_set(rng, 4, 3, 5); - let mut storage = Storage::new(); - let ldd = from_iter(&mut storage, set.iter()); - println!("LDD: {}", LddDisplay::new(&storage, &ldd)); + let ldd = from_iter(&manager, set.iter()); + println!("LDD: {}", LddDisplay::new(&ldd)); - let highest = compute_highest(&mut storage, &ldd); + let highest = compute_highest(&manager, &ldd); println!("Highest: {:?}", highest); for (i, h) in highest.iter().enumerate() { // Determine the highest value for every vector @@ -450,15 +444,15 @@ mod tests { #[cfg_attr(miri, ignore)] // Oxidd does not work with miri fn test_random_ldd_to_bdd() { random_test(100, |rng| { + let manager = oxidd::ldd::new_manager(2048, 1024, 1); let set = random_vector_set(rng, 50, 3, 5); - let mut storage = Storage::new(); - let ldd = from_iter(&mut storage, set.iter()); - println!("LDD: {}", LddDisplay::new(&storage, &ldd)); + let ldd = from_iter(&manager, set.iter()); + println!("LDD: {}", LddDisplay::new(&ldd)); - let highest = compute_highest(&mut storage, &ldd); + let highest = compute_highest(&manager, &ldd); let bits = compute_bits(&highest); - let bits_dd = singleton(&mut storage, &bits); + let bits_dd = LDDFunction::singleton(&manager, &bits).unwrap(); let manager_ref = oxidd::bdd::new_manager(2048, 1024, 1); @@ -466,12 +460,12 @@ mod tests { println!("Total bits: {}", total_bits); println!("Bits per layer: {:?}", bits); let vars = manager_ref.with_manager_exclusive(|manager| manager.add_vars(total_bits).collect::>()); - let bdd = ldd_to_bdd(&mut storage, &manager_ref, &ldd, &bits_dd, &vars).unwrap(); + let bdd = ldd_to_bdd(&manager, &manager_ref, &ldd, &bits_dd, &vars).unwrap(); println!("resulting BDD: {}", FormatConfigSet(&bdd)); - let resulting_ldd = bdd_to_ldd(&mut storage, &manager_ref, &bdd, &vars, &bits, 0, 0).unwrap(); + let resulting_ldd = bdd_to_ldd(&manager, &manager_ref, &bdd, &vars, &bits, 0, 0).unwrap(); - println!("resulting LDD: {}", LddDisplay::new(&storage, &resulting_ldd)); - assert_eq!(ldd, resulting_ldd, "Converted LDD does not match original"); + println!("resulting LDD: {}", LddDisplay::new(&resulting_ldd)); + assert!(ldd == resulting_ldd, "Converted LDD does not match original"); }); } } diff --git a/crates/symbolic/src/lib.rs b/crates/symbolic/src/lib.rs index e39680060..ba73d8e06 100644 --- a/crates/symbolic/src/lib.rs +++ b/crates/symbolic/src/lib.rs @@ -3,15 +3,19 @@ mod convert_bdd; mod convert_ldd; mod cube_iter; +mod cube_iter_ldd; mod dependency_graph; +mod display; mod format; mod io; +mod io_ldd; mod io_sylvan; mod io_symbolic_lts; mod ldd_to_bdd; mod mince_variable_order; mod random_bdd; mod random_symbolic_lts; +mod random_vector_set; mod reachability; mod reachability_bdd; mod refine; @@ -24,15 +28,19 @@ mod util; pub use convert_bdd::*; pub use convert_ldd::*; pub use cube_iter::*; +pub use cube_iter_ldd::*; pub use dependency_graph::*; +pub use display::*; pub use format::*; pub use io::*; +pub use io_ldd::*; pub use io_sylvan::*; pub use io_symbolic_lts::*; pub use ldd_to_bdd::*; pub use mince_variable_order::*; pub use random_bdd::*; pub use random_symbolic_lts::*; +pub use random_vector_set::*; pub use reachability::*; pub use reachability_bdd::*; pub use refine::*; diff --git a/crates/symbolic/src/random_symbolic_lts.rs b/crates/symbolic/src/random_symbolic_lts.rs index 3fad8f642..d051a229b 100644 --- a/crates/symbolic/src/random_symbolic_lts.rs +++ b/crates/symbolic/src/random_symbolic_lts.rs @@ -1,3 +1,4 @@ +use oxidd::ldd::LDDManagerRef; use rand::Rng; use rand::RngExt; use rand::seq::IndexedRandom; @@ -7,9 +8,6 @@ use merc_aterm::ATermString; use merc_data::DataExpression; use merc_data::DataSpecification; use merc_data::DataVariable; -use merc_ldd::Storage; -use merc_ldd::from_iter; -use merc_ldd::random_vector_set; use merc_lts::LtsMultiAction; use merc_lts::TransitionLabel; use merc_utilities::MercError; @@ -17,12 +15,14 @@ use merc_utilities::Timing; use crate::SummandGroup; use crate::SymbolicLts; +use crate::from_iter; +use crate::random_vector_set; use crate::reachability; /// Generates random symbolic LTSs for testing purposes. pub fn random_symbolic_lts( rng: &mut R, - storage: &mut Storage, + manager: &LDDManagerRef, num_state_variables: usize, num_action_labels: usize, ) -> Result { @@ -67,10 +67,10 @@ pub fn random_symbolic_lts( // Reserve additional space for action labels. let relation = random_vector_set(rng, 10, read_parameters.len() + write_parameters.len() + 1, 5); - let relation_bdd = from_iter(storage, relation.iter()); + let relation_bdd = from_iter(manager, relation.iter()); summand_groups.push(SummandGroup::new( - storage, + manager, ¶meters, read_parameters, write_parameters, @@ -78,7 +78,7 @@ pub fn random_symbolic_lts( )?) } - let initial_state_ldd = from_iter(storage, std::iter::once(initial_state)); + let initial_state_ldd = from_iter(manager, std::iter::once(initial_state)); // Compute the actual reachable state set, since the randomly generated transitions are not // restricted to the random state set above. @@ -91,7 +91,7 @@ pub fn random_symbolic_lts( parameter_values, ); - let reachable = reachability(storage, &mut lts, &Timing::new())?; + let reachable = reachability(manager, &mut lts, &Timing::new())?; lts.set_states(reachable); Ok(lts) diff --git a/crates/ldd/src/test_utility.rs b/crates/symbolic/src/random_vector_set.rs similarity index 72% rename from crates/ldd/src/test_utility.rs rename to crates/symbolic/src/random_vector_set.rs index 6b5e4a2dd..e9aa10f44 100644 --- a/crates/ldd/src/test_utility.rs +++ b/crates/symbolic/src/random_vector_set.rs @@ -1,16 +1,16 @@ //! Functions in this module are only relevant for testing purposes. +use oxidd::ldd::LDDFunction; +use oxidd::ldd::LDDManagerRef; +use oxidd::ldd::Value; use rand::Rng; +use rand::RngExt; use std::collections::HashSet; -use rand::RngExt; use streaming_iterator::StreamingIterator; -use crate::Ldd; -use crate::Storage; -use crate::Value; -use crate::iterators::*; -use crate::operations::*; +use crate::element_of; +use crate::iter; /// Returns a vector of the given length with random u64 values (from 0..max_value). pub fn random_vector(rng: &mut R, length: usize, max_value: Value) -> Vec { @@ -44,27 +44,27 @@ pub fn random_vector_set(rng: &mut R, amount: usize, length: usize, max_ } /// Returns an LDD containing all elements of the given iterator over vectors. -pub fn from_iter<'a, I>(storage: &mut Storage, iter: I) -> Ldd +pub fn from_iter<'a, I>(manager: &LDDManagerRef, iter: I) -> LDDFunction where I: Iterator>, { - let mut result = storage.empty_set().clone(); + let mut result = LDDFunction::empty_set(manager).expect("Failed to create the empty set"); for vector in iter { - let single = singleton(storage, vector); - result = union(storage, &result, &single); + let single = LDDFunction::singleton(manager, vector).expect("Failed to create a singleton"); + result = result.union(&single).expect("Failed to compute the union"); } result } /// Prints vectors included in left, but not in right. Returns true iff the difference is non-empty. -pub fn print_left(storage: &Storage, left: &Ldd, right: &Ldd) -> bool { +pub fn print_left(manager: &LDDManagerRef, left: &LDDFunction, right: &LDDFunction) -> bool { let mut result = true; - let mut iter = iter(storage, left); + let mut iter = iter(left); while let Some(element) = iter.next() { - if !element_of(storage, element, right) { + if !element_of(manager, element, right) { result = false; eprintln!("{:?}", element); } @@ -74,12 +74,12 @@ pub fn print_left(storage: &Storage, left: &Ldd, right: &Ldd) -> bool { } /// Prints the differences in contained vectors between two LDDs. -pub fn print_differences(storage: &Storage, left: &Ldd, right: &Ldd) { +pub fn print_differences(manager: &LDDManagerRef, left: &LDDFunction, right: &LDDFunction) { // eprintln!("Vectors contained in {:?}, but not in {:?}:", left, right); - print_left(storage, left, right); + print_left(manager, left, right); // eprintln!("Vectors contained in {}, but not in {}:", right, left); - print_left(storage, right, left); + print_left(manager, right, left); } /// Returns project(vector, proj), see [project]. Requires proj to be sorted. diff --git a/crates/symbolic/src/reachability.rs b/crates/symbolic/src/reachability.rs index f88f6331e..d08c9952b 100644 --- a/crates/symbolic/src/reachability.rs +++ b/crates/symbolic/src/reachability.rs @@ -3,28 +3,25 @@ use std::fmt; use log::debug; use log::info; use log::trace; +use oxidd::ldd::LDDFunction; +use oxidd::ldd::LDDManagerRef; + use merc_data::DataExpression; use merc_io::TimeProgress; -use merc_ldd::Ldd; -use merc_ldd::LddDisplay; -use merc_ldd::Storage; -use merc_ldd::len; -use merc_ldd::minus; -use merc_ldd::relational_product; -use merc_ldd::union; use merc_utilities::MercError; use merc_utilities::Timing; use crate::DependencyGraph; +use crate::LddDisplay; use crate::Relation; /// A generic trait representing a symbolic LTS pub trait SymbolicLTS { /// Returns the LDD representing the set of states. - fn states(&self) -> &Ldd; + fn states(&self) -> &LDDFunction; /// Returns the LDD representing the initial state. - fn initial_state(&self) -> &Ldd; + fn initial_state(&self) -> &LDDFunction; /// Returns an iterator over the summand groups. fn transition_groups(&self) -> &[impl TransitionGroup]; @@ -55,7 +52,7 @@ pub trait SymbolicLTS { pub trait TransitionGroup: fmt::Debug { /// Returns the transition relation T' -> U' for this summand group. - fn relation(&self) -> &Ldd; + fn relation(&self) -> &LDDFunction; /// Returns the read indices for this summand group. fn read_indices(&self) -> &[u32]; @@ -67,23 +64,27 @@ pub trait TransitionGroup: fmt::Debug { fn action_label_index(&self) -> Option; /// Returns the meta information for this summand group required to perform the relational product. - fn meta(&self) -> &Ldd; + fn meta(&self) -> &LDDFunction; /// Learns the successors of the given set of states. /// /// The `todo` the set of vectors for which successors should be learned. /// This function should update the [Self::relation] of the transition group /// to include the new transitions from `todo` to their successors. - fn learn_successors(&mut self, storage: &mut Storage, todo: &Ldd) -> Result<(), MercError>; + fn learn_successors(&mut self, manager: &LDDManagerRef, todo: &LDDFunction) -> Result<(), MercError>; } /// Performs reachability analysis using the given initial state and transitions from the symbolic LTS. -pub fn reachability(storage: &mut Storage, lts: &mut L, timing: &Timing) -> Result { +pub fn reachability( + storage: &LDDManagerRef, + lts: &mut L, + timing: &Timing, +) -> Result { let mut todo = lts.initial_state().clone(); let mut states = lts.initial_state().clone(); // The state space. let mut iteration = 0; - trace!("states = {}", LddDisplay::new(storage, &states)); + trace!("states = {}", LddDisplay::new(&states)); let progress = TimeProgress::new( |(iteration, num_of_states)| { info!("explored {} state(s) after {} iteration(s)", num_of_states, iteration); @@ -92,27 +93,27 @@ pub fn reachability(storage: &mut Storage, lts: &mut L, timing: ); timing.measure("reachability", || { - while todo != *storage.empty_set() { - debug!("Iteration {}: todo size = {}", iteration, len(storage, &todo)); + while !todo.is_empty() { + debug!("Iteration {}: todo size = {}", iteration, todo.len()); // Learn successors for all the transition groups and compute the next todo set. - let mut todo1 = storage.empty_set().clone(); + let mut todo1 = LDDFunction::empty_set(storage)?; for (i, transition) in lts.transition_groups_mut().iter_mut().enumerate() { trace!("Learning successors for transition group {}:", i); timing.measure(&format!("learn_successors_{}", i), || { transition.learn_successors(storage, &todo) })?; - let result = relational_product(storage, &todo, transition.relation(), transition.meta()); - todo1 = union(storage, &todo1, &result); + let result = todo.relational_product(transition.relation(), transition.meta())?; + todo1 = todo1.union(&result)?; } - trace!("todo1 = {}", LddDisplay::new(storage, &todo1)); + trace!("todo1 = {}", LddDisplay::new(&todo1)); - todo = minus(storage, &todo1, &states); - states = union(storage, &states, &todo); + todo = todo1.minus(&states)?; + states = states.union(&todo)?; if progress.is_due() { - progress.print((iteration, len(storage, &states))); + progress.print((iteration, states.len())); } iteration += 1; } diff --git a/crates/symbolic/src/reachability_bdd.rs b/crates/symbolic/src/reachability_bdd.rs index cb46925d9..3024c1b4b 100644 --- a/crates/symbolic/src/reachability_bdd.rs +++ b/crates/symbolic/src/reachability_bdd.rs @@ -85,8 +85,6 @@ pub fn reachability_bdd( // // This can be seen from the following: `exists a. (todo(s) ∧ R(s, s', a))` // is equal to `todo(s)` if `support(R) = a`, where quantifying over `s` would - // This can be seen from the following: `exists a. (todo(s) ∧ R(s, s', a))` - // is equal to `todo(s)` if `support(R) = a`, where quantifying over `s` would // result in `T`. And `todo(s)[s' <- s]` is equal to `todo(s)`. let tmp = todo.apply_exists(BooleanOperator::And, transition.relation(), relation_vars)?; @@ -121,7 +119,6 @@ mod tests { use oxidd::util::SatCountCache; use rustc_hash::FxBuildHasher; - use merc_ldd::len; use merc_utilities::Timing; use merc_utilities::random_test; @@ -134,15 +131,15 @@ mod tests { #[cfg_attr(miri, ignore)] // Oxidd does not work with miri fn test_random_reachability() { random_test(100, |rng| { - let mut storage = merc_ldd::Storage::new(); + let manager = oxidd::ldd::new_manager(2048, 1024, 1); // We don't really check anything here, just ensure that reachability runs without errors. - let mut lts = random_symbolic_lts(rng, &mut storage, 10, 5).unwrap(); - let reachable_states = reachability(&mut storage, &mut lts, &Timing::new()).unwrap(); - let num_reachable_states = len(&mut storage, &reachable_states); + let mut lts = random_symbolic_lts(rng, &manager, 10, 5).unwrap(); + let reachable_states = reachability(&manager, &mut lts, &Timing::new()).unwrap(); + let num_reachable_states = reachable_states.len(); let manager_ref = oxidd::bdd::new_manager(2028, 2028, 1); - let lts_bdd = SymbolicLtsBdd::from_symbolic_lts(&mut storage, &manager_ref, <s).unwrap(); + let lts_bdd = SymbolicLtsBdd::from_symbolic_lts(&manager, &manager_ref, <s).unwrap(); let reachable_states_bdd = reachability_bdd(&manager_ref, <s_bdd, false).unwrap(); let num_reachable_states_bdd = reachable_states_bdd diff --git a/crates/symbolic/src/sigref.rs b/crates/symbolic/src/sigref.rs index 135336139..8b10e5f39 100644 --- a/crates/symbolic/src/sigref.rs +++ b/crates/symbolic/src/sigref.rs @@ -1003,13 +1003,6 @@ fn to_block_index(bits: &[OptBool]) -> u64 { mod tests { use std::ops::Range; - use merc_ldd::Storage; - use merc_lts::LTS; - use merc_lts::LtsBuilderMem; - use merc_reduction::Equivalence; - use merc_reduction::compare_lts; - use merc_reduction::reduce_lts; - use merc_utilities::Timing; use oxidd::BooleanFunction; use oxidd::Edge; use oxidd::Function; @@ -1021,6 +1014,12 @@ mod tests { use oxidd::util::Borrowed; use rand::RngExt; + use merc_lts::LTS; + use merc_lts::LtsBuilderMem; + use merc_reduction::Equivalence; + use merc_reduction::compare_lts; + use merc_reduction::reduce_lts; + use merc_utilities::Timing; use merc_utilities::random_test; use crate::SymbolicLtsBdd; @@ -1075,21 +1074,21 @@ mod tests { #[cfg_attr(miri, ignore)] // Oxidd does not work with miri fn test_random_sigref_split_signature() { random_test(100, |rng| { - let mut storage = Storage::new(); + let ldd_manager = oxidd::ldd::new_manager(2048, 1024, 1); - let lts = random_symbolic_lts(rng, &mut storage, 10, 5).unwrap(); + let lts = random_symbolic_lts(rng, &ldd_manager, 10, 5).unwrap(); - let manager_ref = oxidd::bdd::new_manager(2028, 2028, 1); - let lts_bdd = SymbolicLtsBdd::from_symbolic_lts(&mut storage, &manager_ref, <s).unwrap(); + let bdd_manager = oxidd::bdd::new_manager(2028, 2028, 1); + let lts_bdd = SymbolicLtsBdd::from_symbolic_lts(&ldd_manager, &bdd_manager, <s).unwrap(); let (_, _, expected_num_blocks) = - sigref_symbolic(&manager_ref, <s_bdd, &Timing::new(), false, false, false, false).unwrap(); + sigref_symbolic(&bdd_manager, <s_bdd, &Timing::new(), false, false, false, false).unwrap(); // Create a separate manager since sigref_symbolic creates new block variables. - let manager_ref_split = oxidd::bdd::new_manager(2028, 2028, 1); - let lts_bdd_split = SymbolicLtsBdd::from_symbolic_lts(&mut storage, &manager_ref_split, <s).unwrap(); + let bdd_manager_split = oxidd::bdd::new_manager(2028, 2028, 1); + let lts_bdd_split = SymbolicLtsBdd::from_symbolic_lts(&ldd_manager, &bdd_manager_split, <s).unwrap(); let (_, _, split_num_blocks) = sigref_symbolic( - &manager_ref_split, + &bdd_manager_split, <s_bdd_split, &Timing::new(), true, @@ -1109,18 +1108,18 @@ mod tests { #[test] #[cfg_attr(miri, ignore)] // Oxidd does not work with miri fn test_szymanski_symbolic_refinement() { - let mut storage = Storage::new(); + let ldd_manager = oxidd::ldd::new_manager(2048, 1024, 1); let lts_bdd = read_symbolic_lts( - &mut storage, + &ldd_manager, include_bytes!("../../../examples/lts/Szymanski_3-bit_lin_wait_alt.sym") as &[u8], ) .unwrap(); - let manager_ref = oxidd::bdd::new_manager(2048, 1024, 1); - let lts_bdd = SymbolicLtsBdd::from_symbolic_lts(&mut storage, &manager_ref, <s_bdd).unwrap(); + let bdd_manager = oxidd::bdd::new_manager(2048, 1024, 1); + let lts_bdd = SymbolicLtsBdd::from_symbolic_lts(&ldd_manager, &bdd_manager, <s_bdd).unwrap(); let (_, _, num_of_blocks) = - sigref_symbolic(&manager_ref, <s_bdd, &Timing::new(), false, false, false, false).unwrap(); + sigref_symbolic(&bdd_manager, <s_bdd, &Timing::new(), false, false, false, false).unwrap(); assert_eq!( num_of_blocks, 1791, "The Szymanski example has 1791 bisimulation blocks" @@ -1130,14 +1129,14 @@ mod tests { #[test] #[cfg_attr(miri, ignore)] // Oxidd does not work with miri fn test_symbolic_signature_refinement_abp() { - let mut storage = Storage::new(); - let lts = read_symbolic_lts(&mut storage, include_bytes!("../../../examples/lts/abp.sym") as &[u8]).unwrap(); + let ldd_manager = oxidd::ldd::new_manager(2048, 1024, 1); + let lts = read_symbolic_lts(&ldd_manager, include_bytes!("../../../examples/lts/abp.sym") as &[u8]).unwrap(); - let manager_ref = oxidd::bdd::new_manager(2028, 2028, 1); - let lts_bdd = SymbolicLtsBdd::from_symbolic_lts(&mut storage, &manager_ref, <s).unwrap(); + let bdd_manager = oxidd::bdd::new_manager(2028, 2028, 1); + let lts_bdd = SymbolicLtsBdd::from_symbolic_lts(&ldd_manager, &bdd_manager, <s).unwrap(); let (_, _, num_of_blocks) = - sigref_symbolic(&manager_ref, <s_bdd, &mut Timing::new(), false, false, false, false).unwrap(); + sigref_symbolic(&bdd_manager, <s_bdd, &mut Timing::new(), false, false, false, false).unwrap(); assert_eq!(num_of_blocks, 68, "The ABP examples has 68 bisimulation blocks"); } @@ -1145,13 +1144,13 @@ mod tests { #[cfg_attr(miri, ignore)] // Oxidd does not work with miri fn test_random_is_cube() { random_test(100, |rng| { - let manager = oxidd::bdd::new_manager(2048, 1024, 1); + let ldd_manager = oxidd::bdd::new_manager(2048, 1024, 1); // Create variables in the BDD manager let vars: Vec = - manager.with_manager_exclusive(|manager| manager.add_vars(8).collect::>()); + ldd_manager.with_manager_exclusive(|manager| manager.add_vars(8).collect::>()); - let bdd_vars = manager + let bdd_vars = ldd_manager .with_manager_exclusive(|manager| { vars.iter() .map(|v| BDDFunction::var(manager, *v)) @@ -1159,9 +1158,9 @@ mod tests { }) .unwrap(); - let bdd = random_bdd(&manager, rng, &bdd_vars, 1).unwrap(); + let bdd = random_bdd(&ldd_manager, rng, &bdd_vars, 1).unwrap(); - manager.with_manager_shared(|manager| { + ldd_manager.with_manager_shared(|manager| { assert!( !bdd.satisfiable() || is_bdd_cube_edge(&manager, bdd.as_edge(manager).borrowed()).unwrap(), "The bdd was created as a cube, so it should be a cube" @@ -1174,15 +1173,15 @@ mod tests { #[cfg_attr(miri, ignore)] // Oxidd does not work with miri fn test_random_sigref() { random_test(100, |rng| { - let mut storage = Storage::new(); + let ldd_manager = oxidd::ldd::new_manager(2048, 1024, 1); - let lts = random_symbolic_lts(rng, &mut storage, 10, 5).unwrap(); + let lts = random_symbolic_lts(rng, &ldd_manager, 10, 5).unwrap(); - let manager_ref = oxidd::bdd::new_manager(2028, 2028, 1); - let lts_bdd = SymbolicLtsBdd::from_symbolic_lts(&mut storage, &manager_ref, <s).unwrap(); + let bdd_manager = oxidd::bdd::new_manager(2028, 2028, 1); + let lts_bdd = SymbolicLtsBdd::from_symbolic_lts(&ldd_manager, &bdd_manager, <s).unwrap(); let mut builder = LtsBuilderMem::new(Vec::new(), Vec::new()); - let explicit_lts = convert_symbolic_lts(&mut storage, &mut builder, <s).unwrap(); + let explicit_lts = convert_symbolic_lts(&ldd_manager, &mut builder, <s).unwrap(); let explicit_lts_reduced = reduce_lts( explicit_lts.clone(), Equivalence::StrongBisim, @@ -1191,12 +1190,12 @@ mod tests { ); let (partition, block_vars, _num_of_blocks) = - sigref_symbolic(&manager_ref, <s_bdd, &mut Timing::new(), false, false, false, false).unwrap(); + sigref_symbolic(&bdd_manager, <s_bdd, &mut Timing::new(), false, false, false, false).unwrap(); - let quotient_lts = quotient_symbolic(&manager_ref, <s_bdd, &partition, &block_vars).unwrap(); + let quotient_lts = quotient_symbolic(&bdd_manager, <s_bdd, &partition, &block_vars).unwrap(); let mut builder = LtsBuilderMem::new(Vec::new(), Vec::new()); - let symbolic_lts_reduced = convert_symbolic_lts_bdd(&manager_ref, &mut builder, "ient_lts).unwrap(); + let symbolic_lts_reduced = convert_symbolic_lts_bdd(&bdd_manager, &mut builder, "ient_lts).unwrap(); println!( "Explicit LTS has {} states and {} transitions", diff --git a/crates/symbolic/src/symbolic_lts.rs b/crates/symbolic/src/symbolic_lts.rs index 7600c17bb..e03529788 100644 --- a/crates/symbolic/src/symbolic_lts.rs +++ b/crates/symbolic/src/symbolic_lts.rs @@ -3,13 +3,12 @@ use std::fmt; use merc_data::DataExpression; use merc_data::DataSpecification; use merc_data::DataVariable; -use merc_ldd::Ldd; -use merc_ldd::Storage; -use merc_ldd::Value; -use merc_ldd::compute_meta; use merc_lts::LtsAction; use merc_lts::LtsMultiAction; use merc_utilities::MercError; +use oxidd::ldd::LDDFunction; +use oxidd::ldd::LDDManagerRef; +use oxidd::ldd::Value; use crate::SymbolicLTS; use crate::TransitionGroup; @@ -17,10 +16,10 @@ use crate::TransitionGroup; /// Represents a symbolic LTS encoded by a disjunctive transition relation and a set of states. pub struct SymbolicLts { data_specification: DataSpecification, - states: Ldd, + states: LDDFunction, /// A singleton LDD representing the initial state. - initial_state: Ldd, + initial_state: LDDFunction, summand_groups: Vec, /// The action labels of the LTS, stored as their string representation, @@ -40,8 +39,8 @@ impl SymbolicLts { /// in the LDDs. pub fn new( data_specification: DataSpecification, - states: Ldd, - initial_state: Ldd, + states: LDDFunction, + initial_state: LDDFunction, summand_groups: Vec, action_labels: Vec>, parameter_values: Vec>, @@ -72,17 +71,17 @@ impl SymbolicLts { } /// Replaces the set of states of the LTS, for example after running reachability. - pub fn set_states(&mut self, states: Ldd) { + pub fn set_states(&mut self, states: LDDFunction) { self.states = states; } } impl SymbolicLTS for SymbolicLts { - fn states(&self) -> &Ldd { + fn states(&self) -> &LDDFunction { &self.states } - fn initial_state(&self) -> &Ldd { + fn initial_state(&self) -> &LDDFunction { &self.initial_state } @@ -123,21 +122,21 @@ pub struct SummandGroup { write_parameter_indices: Vec, /// The transition relation T' -> U' for this summand group. - relation: Ldd, + relation: LDDFunction, /// The meta information for this summand group. - meta: Ldd, + meta: LDDFunction, /// The action label index for this summand group. action_label_index: usize, } impl TransitionGroup for SummandGroup { - fn relation(&self) -> &Ldd { + fn relation(&self) -> &LDDFunction { &self.relation } - fn meta(&self) -> &Ldd { + fn meta(&self) -> &LDDFunction { &self.meta } @@ -153,7 +152,7 @@ impl TransitionGroup for SummandGroup { Some(self.action_label_index) } - fn learn_successors(&mut self, _storage: &mut Storage, _todo: &Ldd) -> Result<(), MercError> { + fn learn_successors(&mut self, _storage: &LDDManagerRef, _todo: &LDDFunction) -> Result<(), MercError> { // All states are already explored. Ok(()) } @@ -164,11 +163,11 @@ impl SummandGroup { /// /// This can fail if one of the read or write parameters is not in the list of all parameters. pub fn new( - storage: &mut Storage, + manager: &LDDManagerRef, parameters: &[DataVariable], read_parameters: Vec, write_parameters: Vec, - relation: Ldd, + relation: LDDFunction, ) -> Result { // Find the position of every variable in the parameter list. let mut read_parameter_indices: Vec = read_parameters @@ -197,7 +196,7 @@ impl SummandGroup { write_parameter_indices.sort(); read_parameter_indices.sort(); - let meta = compute_meta(storage, &read_parameter_indices, &write_parameter_indices).0; + let meta = LDDFunction::relation_product_meta(manager, &read_parameter_indices, &write_parameter_indices)?.0; let action_label_index = read_parameters.len() + write_parameters.len(); // The action label is the last index Ok(Self { @@ -212,7 +211,7 @@ impl SummandGroup { } /// Returns the transition relation LDD for this summand group. - pub fn relation(&self) -> &Ldd { + pub fn relation(&self) -> &LDDFunction { &self.relation } diff --git a/crates/symbolic/src/symbolic_lts_bdd.rs b/crates/symbolic/src/symbolic_lts_bdd.rs index c37c5b46d..a81bbaefb 100644 --- a/crates/symbolic/src/symbolic_lts_bdd.rs +++ b/crates/symbolic/src/symbolic_lts_bdd.rs @@ -10,13 +10,13 @@ use oxidd::VarNo; use oxidd::bdd::BDDFunction; use oxidd::bdd::BDDManagerRef; use oxidd::error::DuplicateVarName; +use oxidd::ldd::LDDManagerRef; +use oxidd::ldd::Value; +use oxidd::util::OutOfMemory; use merc_data::DataExpression; -use merc_ldd::Storage; -use merc_ldd::Value; -use merc_ldd::singleton; use merc_utilities::MercError; -use oxidd::util::OutOfMemory; +use oxidd::ldd::LDDFunction; use crate::SymbolicLTS; use crate::TransitionGroup; @@ -67,18 +67,18 @@ impl SymbolicLtsBdd { /// of the LDD symbolic LTS, as unreachable states may not be representable /// with the number of bits assigned to each state variable. pub fn from_symbolic_lts( - storage: &mut Storage, - manager_ref: &BDDManagerRef, + manager: &LDDManagerRef, + manager_bdd: &BDDManagerRef, lts: &L, ) -> Result { info!("Converting symbolic LTS from LDD to BDD representation..."); // Determine the highest values for every state variable. - let mut state_highest = compute_highest(storage, lts.states()); + let mut state_highest = compute_highest(manager, lts.states()); let mut action_label_highest = 0u32; for group in lts.transition_groups() { - let highest = compute_highest(storage, group.relation()); + let highest = compute_highest(manager, group.relation()); // Deal with the special empty case. if highest.is_empty() { @@ -141,12 +141,12 @@ impl SymbolicLtsBdd { } // Check for existing variables. - if manager_ref.with_manager_shared(|manager| manager.num_vars()) != 0 { + if manager_bdd.with_manager_shared(|manager| manager.num_vars()) != 0 { return Err("BDD manager must not contain any variables yet".into()); } // Ensure that the BDD manager is empty. - manager_ref.with_manager_exclusive(|manager| { + manager_bdd.with_manager_exclusive(|manager| { debug_assert_eq!( manager.num_vars(), 0, @@ -156,7 +156,7 @@ impl SymbolicLtsBdd { // Create variables in the BDD manager let number_of_vars = vars.len(); - let variables = manager_ref + let variables = manager_bdd .with_manager_exclusive(|manager| -> Result, DuplicateVarName> { manager.add_named_vars(vars) }) @@ -169,12 +169,12 @@ impl SymbolicLtsBdd { ); // Convert the states to a BDD representation. - let bits_dd = singleton(storage, &state_bits); + let bits_dd = LDDFunction::singleton(manager, &state_bits)?; let all_state_variables_bits: Vec = state_variables_bits.iter().flatten().cloned().collect(); - let states = ldd_to_bdd(storage, manager_ref, lts.states(), &bits_dd, &all_state_variables_bits)?; + let states = ldd_to_bdd(manager, manager_bdd, lts.states(), &bits_dd, &all_state_variables_bits)?; let initial_state = ldd_to_bdd( - storage, - manager_ref, + manager, + manager_bdd, lts.initial_state(), &bits_dd, &all_state_variables_bits, @@ -220,8 +220,8 @@ impl SymbolicLtsBdd { index, group, relation_bits, variables ); - let bits_dd = singleton(storage, &relation_bits); - let relation_bdd = ldd_to_bdd(storage, manager_ref, group.relation(), &bits_dd, &variables)?; + let bits_dd = LDDFunction::singleton(manager, &relation_bits)?; + let relation_bdd = ldd_to_bdd(manager, manager_bdd, group.relation(), &bits_dd, &variables)?; transition_groups.push(SummandGroupBdd::new( relation_bdd, @@ -399,7 +399,6 @@ pub fn compute_vars_bdd( #[cfg(test)] mod tests { - use merc_ldd::Storage; use merc_utilities::test_logger; use crate::SymbolicLtsBdd; @@ -412,11 +411,11 @@ mod tests { let input = include_bytes!("../../../examples/lts/abp.sym"); - let mut storage = Storage::new(); - let manager_ref = oxidd::bdd::new_manager(2048, 1024, 1); - let symbolic_lts = read_symbolic_lts(&mut storage, &input[..]).unwrap(); + let ldd_manager = oxidd::ldd::new_manager(2048, 1024, 1); + let bdd_manager = oxidd::bdd::new_manager(2048, 1024, 1); + let symbolic_lts = read_symbolic_lts(&ldd_manager, &input[..]).unwrap(); // This only tests that the conversion does not panic. - SymbolicLtsBdd::from_symbolic_lts(&mut storage, &manager_ref, &symbolic_lts).unwrap(); + SymbolicLtsBdd::from_symbolic_lts(&ldd_manager, &bdd_manager, &symbolic_lts).unwrap(); } } diff --git a/crates/symbolic/src/symbolic_quotient.rs b/crates/symbolic/src/symbolic_quotient.rs index 34bb3ac6a..c7739325c 100644 --- a/crates/symbolic/src/symbolic_quotient.rs +++ b/crates/symbolic/src/symbolic_quotient.rs @@ -1,7 +1,5 @@ use std::ops::Range; -use merc_ldd::Value; -use merc_utilities::MercError; use oxidd::BooleanFunctionQuant; use oxidd::BooleanOperator; use oxidd::FunctionSubst; @@ -12,6 +10,9 @@ use oxidd::VarNo; use oxidd::bdd::BDDFunction; use oxidd::bdd::BDDManagerRef; use oxidd::error::DuplicateVarName; +use oxidd::ldd::Value; + +use merc_utilities::MercError; use crate::SummandGroupBdd; use crate::SymbolicLtsBdd; diff --git a/crates/symbolic/src/util.rs b/crates/symbolic/src/util.rs index 8a8fde33b..726ac4482 100644 --- a/crates/symbolic/src/util.rs +++ b/crates/symbolic/src/util.rs @@ -1,4 +1,6 @@ use std::collections::HashSet; + +use std::cmp::Ordering; use std::fmt; use merc_io::LargeFormatter; @@ -14,12 +16,16 @@ use oxidd::Node; use oxidd::VarNo; use oxidd::bdd::BDDFunction; use oxidd::bdd::BDDManagerRef; +use oxidd::ldd::LDDFunction; +use oxidd::ldd::LDDManagerRef; +use oxidd::ldd::Value; use oxidd::util::Borrowed; use oxidd::util::OutOfMemory; use oxidd::util::SatCountCache as OxiddSatCountCache; use oxidd_core::function::EdgeOfFunc; use oxidd_core::util::EdgeDropGuard; use oxidd_core::util::num::F64; +use oxidd_rules_ldd::LDDTerminal; use rustc_hash::FxBuildHasher; use rustc_hash::FxHashMap; @@ -387,10 +393,59 @@ pub(crate) fn reduce<'id>( } oxidd_core::LevelView::get_or_insert( &mut manager.level(level), - <::Manager<'id> as Manager>::InnerNode::new(level, [t, e]), + <::Manager<'id> as Manager>::InnerNode::new(level, [t, e], ()), ) } +/// Returns the height of the LDD tree. +pub fn height(manager: &LDDManagerRef, ldd: &LDDFunction) -> usize { + manager.with_manager_shared(|manager| height_edge(manager, ldd.as_edge(manager).borrowed())) +} + +/// The edge variant of [height]. +pub fn height_edge<'id>( + manager: &::Manager<'id>, + ldd: Borrowed>, +) -> usize { + match manager.get_node(&ldd) { + Node::Terminal(_) => 0, + Node::Inner(node) => { + // All right siblings share the same height, so only the down chain + // contributes to the height of the LDD. + let (down, _right) = collect_children(node); + 1 + height_edge(manager, down) + } + } +} + +/// Returns true iff the set contains the vector. +pub fn element_of(manager: &LDDManagerRef, vector: &[Value], ldd: &LDDFunction) -> bool { + manager.with_manager_shared(|manager| element_of_edge(manager, vector, ldd.as_edge(manager).borrowed())) +} + +fn element_of_edge<'id>( + manager: &::Manager<'id>, + vector: &[Value], + ldd: Borrowed>, +) -> bool { + match manager.get_node(&ldd) { + Node::Terminal(LDDTerminal::True) => vector.is_empty(), + Node::Terminal(LDDTerminal::Empty) => false, + Node::Inner(node) => { + let value = *node.get_value(); + let (down, right) = collect_children(node); + match vector.first() { + None => false, + Some(&first) => match value.cmp(&first) { + Ordering::Less => element_of_edge(manager, vector, right), + Ordering::Equal => element_of_edge(manager, &vector[1..], down), + Ordering::Greater => false, + }, + } + } + } +} + #[cfg(test)] mod tests { use merc_utilities::random_test; diff --git a/tools/lts/Cargo.toml b/tools/lts/Cargo.toml index d79ad5583..b1e122127 100644 --- a/tools/lts/Cargo.toml +++ b/tools/lts/Cargo.toml @@ -9,7 +9,6 @@ rust-version.workspace = true merc_collections.workspace = true merc_explore.workspace = true merc_io.workspace = true -merc_ldd.workspace = true merc_lts = { workspace = true, features = ["clap"] } merc_reduction = { workspace = true, features = ["clap"] } merc_refinement = { workspace = true, features = ["clap"] } diff --git a/tools/mcrl2/Cargo.lock b/tools/mcrl2/Cargo.lock index a43326001..f4db8a6e5 100644 --- a/tools/mcrl2/Cargo.lock +++ b/tools/mcrl2/Cargo.lock @@ -110,8 +110,7 @@ checksum = "7f202df86484c868dbad7eaa557ef785d5c66295e41b460ef922eca0723b842c" [[package]] name = "arcslab" version = "0.1.2" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "67d525761a6913dc2115b17c9c72379de20e9fd7b12ad479bbadbb544b20b32b" +source = "git+https://github.com/mlaveaux/oxidd?rev=4ed048be1f064f6dc4497a396204de35e4c1568b#4ed048be1f064f6dc4497a396204de35e4c1568b" dependencies = [ "crossbeam-utils", "derive-where", @@ -571,9 +570,9 @@ checksum = "1d674e81391d1e1ab681a28d99df07927c6d4aa5b027d7da16ba32d1d21ecd99" [[package]] name = "flume" -version = "0.11.1" +version = "0.12.0" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "da0e4dd2a88388a1f4ccc7c9ce104604dab68d9f408dc34cd45823d5a9069095" +checksum = "5e139bc46ca777eb5efaf62df0ab8cc5fd400866427e56c68b22e414e53bd3be" dependencies = [ "spin", ] @@ -688,8 +687,7 @@ checksum = "2304e00983f87ffb38b55b444b5e3b60a884b5d30c0fca7d82fe33449bbe55ea" [[package]] name = "hugealloc" version = "0.1.1" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "542733215a252c27c674e5d875a910d7de509cb74123d0bdbaa050f871ec84c2" +source = "git+https://github.com/mlaveaux/oxidd?rev=4ed048be1f064f6dc4497a396204de35e4c1568b#4ed048be1f064f6dc4497a396204de35e4c1568b" dependencies = [ "allocator-api2 0.2.21", "libc", @@ -824,8 +822,7 @@ dependencies = [ [[package]] name = "linear-hashtbl" version = "0.1.4" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "b11269ceb6867559e0fce487ff8148933040c7ac091ee4ecc904821f1db1e0fa" +source = "git+https://github.com/mlaveaux/oxidd?rev=4ed048be1f064f6dc4497a396204de35e4c1568b#4ed048be1f064f6dc4497a396204de35e4c1568b" [[package]] name = "link-cplusplus" @@ -944,12 +941,12 @@ dependencies = [ "merc_data", "merc_explore", "merc_io", - "merc_ldd", "merc_lts", "merc_symbolic", "merc_tools", "merc_unsafety", "merc_utilities", + "oxidd", "rand", "serde", "serde_json", @@ -1032,7 +1029,7 @@ dependencies = [ [[package]] name = "merc_explore" -version = "2.0.0" +version = "0.1.0" dependencies = [ "itertools 0.14.0", "log", @@ -1059,25 +1056,6 @@ dependencies = [ "thiserror", ] -[[package]] -name = "merc_ldd" -version = "3.0.0" -dependencies = [ - "ahash", - "delegate", - "itertools 0.14.0", - "log", - "merc_aterm", - "merc_collections", - "merc_io", - "merc_number", - "merc_unsafety", - "merc_utilities", - "rand", - "rustc-hash 2.1.2", - "streaming-iterator", -] - [[package]] name = "merc_lts" version = "2.0.0" @@ -1190,6 +1168,7 @@ dependencies = [ name = "merc_symbolic" version = "3.0.0" dependencies = [ + "delegate", "duct", "itertools 0.14.0", "log", @@ -1197,14 +1176,15 @@ dependencies = [ "merc_collections", "merc_data", "merc_io", - "merc_ldd", "merc_lts", + "merc_number", "merc_utilities", "oxidd", "oxidd-core", "oxidd-dump", "oxidd-reorder", "oxidd-rules-bdd", + "oxidd-rules-ldd", "rand", "rustc-hash 2.1.2", "streaming-iterator", @@ -1423,8 +1403,7 @@ dependencies = [ [[package]] name = "oxidd" version = "0.11.0" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "c984e2c820ff1306f7bd10ac166a542c69cce2d87331eb4caa1b78ca381e5c0b" +source = "git+https://github.com/mlaveaux/oxidd?rev=4ed048be1f064f6dc4497a396204de35e4c1568b#4ed048be1f064f6dc4497a396204de35e4c1568b" dependencies = [ "cfg-if", "derive-where", @@ -1437,6 +1416,7 @@ dependencies = [ "oxidd-manager-pointer", "oxidd-reorder", "oxidd-rules-bdd", + "oxidd-rules-ldd", "oxidd-rules-mtbdd", "oxidd-rules-tdd", "oxidd-rules-zbdd", @@ -1446,8 +1426,7 @@ dependencies = [ [[package]] name = "oxidd-cache" version = "0.11.1" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "ea87b04767bd71ec9a0f0f1b95b3e1be822365d611ae692734bf84dffdc1aae9" +source = "git+https://github.com/mlaveaux/oxidd?rev=4ed048be1f064f6dc4497a396204de35e4c1568b#4ed048be1f064f6dc4497a396204de35e4c1568b" dependencies = [ "allocator-api2 0.2.21", "document-features", @@ -1459,8 +1438,7 @@ dependencies = [ [[package]] name = "oxidd-core" version = "0.11.0" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "c4ce8a17e276f5df5a9a2aabdc0fd1ccf2b3b73bc3b5ef7627f26f6ecc9afee3" +source = "git+https://github.com/mlaveaux/oxidd?rev=4ed048be1f064f6dc4497a396204de35e4c1568b#4ed048be1f064f6dc4497a396204de35e4c1568b" dependencies = [ "nanorand", ] @@ -1468,8 +1446,7 @@ dependencies = [ [[package]] name = "oxidd-derive" version = "0.11.0" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "96cb7e36aee287b5ad1921fb98050a1b9e5771bf5d34381f24b0548083aefeb3" +source = "git+https://github.com/mlaveaux/oxidd?rev=4ed048be1f064f6dc4497a396204de35e4c1568b#4ed048be1f064f6dc4497a396204de35e4c1568b" dependencies = [ "proc-macro-error", "proc-macro2", @@ -1480,8 +1457,7 @@ dependencies = [ [[package]] name = "oxidd-dump" version = "0.6.0" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "675fcc8144350309a3b94a4a3522d953472c29df06b783fe0dfafbc6b1d39b4b" +source = "git+https://github.com/mlaveaux/oxidd?rev=4ed048be1f064f6dc4497a396204de35e4c1568b#4ed048be1f064f6dc4497a396204de35e4c1568b" dependencies = [ "document-features", "fixedbitset", @@ -1495,8 +1471,7 @@ dependencies = [ [[package]] name = "oxidd-manager-index" version = "0.11.0" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "e1339eb2952e23d62d3421f444fdf36d7f36b6a63707ae3d4fef1d1bfb007a47" +source = "git+https://github.com/mlaveaux/oxidd?rev=4ed048be1f064f6dc4497a396204de35e4c1568b#4ed048be1f064f6dc4497a396204de35e4c1568b" dependencies = [ "crossbeam-utils", "derive-where", @@ -1511,8 +1486,7 @@ dependencies = [ [[package]] name = "oxidd-manager-pointer" version = "0.6.0" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "ad78ecc8d113d3e3a2d06a47299d8a557088f016323f0f22f363622ff239ebb8" +source = "git+https://github.com/mlaveaux/oxidd?rev=4ed048be1f064f6dc4497a396204de35e4c1568b#4ed048be1f064f6dc4497a396204de35e4c1568b" dependencies = [ "arcslab", "derive-where", @@ -1528,8 +1502,7 @@ dependencies = [ [[package]] name = "oxidd-reorder" version = "0.6.1" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "6863dd156fb2713ad1f6b7528d08da3cc675ae27e24b6e9a0df9d0fea8d9a839" +source = "git+https://github.com/mlaveaux/oxidd?rev=4ed048be1f064f6dc4497a396204de35e4c1568b#4ed048be1f064f6dc4497a396204de35e4c1568b" dependencies = [ "flume", "is_sorted", @@ -1541,8 +1514,7 @@ dependencies = [ [[package]] name = "oxidd-rules-bdd" version = "0.11.0" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "c56b5465552bdc2c1f38c433f8751703d1561396f4be16315999cc47eed6e2ce" +source = "git+https://github.com/mlaveaux/oxidd?rev=4ed048be1f064f6dc4497a396204de35e4c1568b#4ed048be1f064f6dc4497a396204de35e4c1568b" dependencies = [ "document-features", "fixedbitset", @@ -1551,11 +1523,19 @@ dependencies = [ "oxidd-dump", ] +[[package]] +name = "oxidd-rules-ldd" +version = "0.11.0" +source = "git+https://github.com/mlaveaux/oxidd?rev=4ed048be1f064f6dc4497a396204de35e4c1568b#4ed048be1f064f6dc4497a396204de35e4c1568b" +dependencies = [ + "oxidd-core", + "oxidd-derive", +] + [[package]] name = "oxidd-rules-mtbdd" version = "0.6.0" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "49740035de417b58fad2fe420b5539081604e601c266841f3092ca8bb5db1da7" +source = "git+https://github.com/mlaveaux/oxidd?rev=4ed048be1f064f6dc4497a396204de35e4c1568b#4ed048be1f064f6dc4497a396204de35e4c1568b" dependencies = [ "document-features", "fixedbitset", @@ -1567,8 +1547,7 @@ dependencies = [ [[package]] name = "oxidd-rules-tdd" version = "0.6.0" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "eb13c585037127f6066e3ca928e96bdc21df19a41b0242dfcb9e95faf723558c" +source = "git+https://github.com/mlaveaux/oxidd?rev=4ed048be1f064f6dc4497a396204de35e4c1568b#4ed048be1f064f6dc4497a396204de35e4c1568b" dependencies = [ "document-features", "oxidd-core", @@ -1579,8 +1558,7 @@ dependencies = [ [[package]] name = "oxidd-rules-zbdd" version = "0.11.0" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "917c941a721e884817a5b510ff818cb6d7033216817c0fd1e0b154f4cc7cfe5b" +source = "git+https://github.com/mlaveaux/oxidd?rev=4ed048be1f064f6dc4497a396204de35e4c1568b#4ed048be1f064f6dc4497a396204de35e4c1568b" dependencies = [ "document-features", "fixedbitset", diff --git a/tools/mcrl2/Cargo.toml b/tools/mcrl2/Cargo.toml index f393e5e73..79b5c6e4d 100644 --- a/tools/mcrl2/Cargo.toml +++ b/tools/mcrl2/Cargo.toml @@ -49,13 +49,22 @@ merc_collections = { path = "../../crates/collections" } merc_data = { path = "../../crates/data" } merc_explore = { path = "../../crates/explore" } merc_io = { path = "../../crates/io" } -merc_ldd = { path = "../../crates/ldd" } merc_lts = { path = "../../crates/lts" } merc_symbolic = { path = "../../crates/symbolic" } merc_tools = { path = "../../crates/tools" } merc_unsafety = { path = "../../crates/unsafety" } merc_utilities = { path = "../../crates/utilities" } +oxidd = { git = "https://github.com/mlaveaux/oxidd", rev = "4ed048be1f064f6dc4497a396204de35e4c1568b", features = ["manager-pointer"] } + # Use a local version of mCRL2-sys for development. # [patch."https://github.com/MERCorg/mCRL2-sys"] -# mcrl2-sys = { path = "crates/mCRL2-sys" } \ No newline at end of file +# mcrl2-sys = { path = "crates/mCRL2-sys" } + +[patch.crates-io] +oxidd = { git = "https://github.com/mlaveaux/oxidd", rev = "4ed048be1f064f6dc4497a396204de35e4c1568b" } +oxidd-core = { git = "https://github.com/mlaveaux/oxidd", rev = "4ed048be1f064f6dc4497a396204de35e4c1568b" } +oxidd-dump = { git = "https://github.com/mlaveaux/oxidd", rev = "4ed048be1f064f6dc4497a396204de35e4c1568b" } +oxidd-reorder = { git = "https://github.com/mlaveaux/oxidd", rev = "4ed048be1f064f6dc4497a396204de35e4c1568b" } +oxidd-rules-bdd = { git = "https://github.com/mlaveaux/oxidd", rev = "4ed048be1f064f6dc4497a396204de35e4c1568b" } +oxidd-rules-ldd = { git = "https://github.com/mlaveaux/oxidd", rev = "4ed048be1f064f6dc4497a396204de35e4c1568b" } \ No newline at end of file diff --git a/tools/mcrl2/lps/Cargo.toml b/tools/mcrl2/lps/Cargo.toml index 35c2b3131..75454e7d2 100644 --- a/tools/mcrl2/lps/Cargo.toml +++ b/tools/mcrl2/lps/Cargo.toml @@ -11,12 +11,12 @@ merc_collections.workspace = true merc_data.workspace = true merc_explore.workspace = true merc_io.workspace = true -merc_ldd.workspace = true merc_lts.workspace = true merc_symbolic.workspace = true merc_tools.workspace = true merc_unsafety.workspace = true merc_utilities.workspace = true +oxidd.workspace = true clap.workspace = true env_logger.workspace = true diff --git a/tools/mcrl2/lps/src/explore_symbolic.rs b/tools/mcrl2/lps/src/explore_symbolic.rs index 94733c41c..5d4aa3d9b 100644 --- a/tools/mcrl2/lps/src/explore_symbolic.rs +++ b/tools/mcrl2/lps/src/explore_symbolic.rs @@ -19,17 +19,14 @@ use mcrl2::free_variables_data_expression; use mcrl2::preprocess; use merc_collections::IndexedSet; -use merc_ldd::Ldd; -use merc_ldd::Storage; -use merc_ldd::Value; -use merc_ldd::compute_meta; -use merc_ldd::compute_proj; -use merc_ldd::iterators::for_each_mut; -use merc_ldd::project; -use merc_ldd::singleton; -use merc_ldd::union; +use oxidd::ldd::LDDFunction; +use oxidd::ldd::LDDManagerRef; +use oxidd::ldd::Value; +use streaming_iterator::StreamingIterator; + use merc_symbolic::SymbolicLTS; use merc_symbolic::TransitionGroup; +use merc_symbolic::iter; use merc_symbolic::reachability; use merc_utilities::MercError; @@ -37,10 +34,10 @@ use merc_utilities::Timing; /// Explore the linear process specification using symbolic reachability. pub fn explore_lps_symbolic( - storage: &mut Storage, + storage: &LDDManagerRef, lps: &LinearProcessSpecification, timing: &Timing, -) -> Result { +) -> Result { let mut symbolic_lts = SymbolicLinearProcessSpecification::new(storage, lps)?; debug!("{symbolic_lts:?}"); @@ -63,11 +60,11 @@ struct SymbolicLinearProcessSpecification { _shared: Rc, /// The initial state of the LPS. - initial_state: Ldd, + initial_state: LDDFunction, } impl SymbolicLinearProcessSpecification { - pub fn new(storage: &mut Storage, lps: &LinearProcessSpecification) -> Result { + pub fn new(storage: &LDDManagerRef, lps: &LinearProcessSpecification) -> Result { let lps = preprocess(lps)?; let parameters = lps.parameters(); @@ -85,7 +82,7 @@ impl SymbolicLinearProcessSpecification { &lps.action_summand(index)?, ¶meters, Rc::clone(&shared), - )); + )?); } let initial_state_vector = lps @@ -105,7 +102,7 @@ impl SymbolicLinearProcessSpecification { "Initial state vector length must match number of parameters" ); - let initial_state = singleton(storage, &initial_state_vector); + let initial_state = LDDFunction::singleton(storage, &initial_state_vector)?; Ok(SymbolicLinearProcessSpecification { _lps: lps, @@ -131,10 +128,10 @@ struct Shared { /// Represents a symbolic summand of a [mcrl2::LinearProcessSpecification]. struct SymbolicSummand { /// The LDD encoding the projection of the state space on the read variables of this summand. - project_ldd: Ldd, + project_ldd: LDDFunction, /// The relation encoding the transition relation of this summand. - relation: Ldd, + relation: LDDFunction, /// The parameters that are read by this summand. read_parameters: Vec<*const _aterm>, @@ -144,16 +141,16 @@ struct SymbolicSummand { read_indices: Vec, /// The positions of `read_indices` in the short vector. - read_positions: Vec, + read_positions: Vec, /// The indices of the parameters that are written by this summand. write_indices: Vec, /// The positions of `write_indices` in the short vector. - write_positions: Vec, + write_positions: Vec, /// The meta information for this summand, which is required by the relational product. - meta: Ldd, + meta: LDDFunction, /// The condition of this summand. condition: DataExpression, @@ -174,11 +171,11 @@ struct SymbolicSummand { impl SymbolicSummand { /// Extract the required information from the given action summand that is required for symbolic exploration. pub fn new( - storage: &mut Storage, + storage: &LDDManagerRef, summand: &LinearSummand, parameters: &ATermList, shared: Rc, - ) -> Self { + ) -> Result { // Collect free variables from the condition. let mut read_vars = free_variables_data_expression(&summand.condition().copy()); let parameters = parameters.to_vec(); @@ -231,10 +228,11 @@ impl SymbolicSummand { let summation_variables: ATermList = summand.summation_variables(); let multi_action: ATerm = summand.multi_action(); - let relation = storage.protect(storage.empty_set()); - let project_ldd = compute_proj(storage, &read_indices); + let relation = LDDFunction::empty_set(storage)?; + let project_ldd = LDDFunction::projection_meta(storage, &read_indices)?; - let (meta, read_positions, write_positions) = compute_meta(storage, &read_indices, &write_indices); + let (meta, read_positions, write_positions) = + LDDFunction::relation_product_meta(storage, &read_indices, &write_indices)?; debug_assert_eq!( read_indices.len(), @@ -262,7 +260,7 @@ impl SymbolicSummand { "Write indices must be strictly sorted" ); - Self { + Ok(Self { project_ldd, relation, read_indices, @@ -276,16 +274,16 @@ impl SymbolicSummand { multi_action, shared, read_parameters, - } + }) } } impl SymbolicLTS for SymbolicLinearProcessSpecification { - fn states(&self) -> &Ldd { + fn states(&self) -> &LDDFunction { unreachable!("The SymbolicLTS interface can only be explored"); } - fn initial_state(&self) -> &Ldd { + fn initial_state(&self) -> &LDDFunction { &self.initial_state } @@ -307,7 +305,7 @@ impl SymbolicLTS for SymbolicLinearProcessSpecification { } impl TransitionGroup for SymbolicSummand { - fn relation(&self) -> &Ldd { + fn relation(&self) -> &LDDFunction { &self.relation } @@ -323,18 +321,19 @@ impl TransitionGroup for SymbolicSummand { None } - fn meta(&self) -> &Ldd { + fn meta(&self) -> &LDDFunction { &self.meta } - fn learn_successors(&mut self, storage: &mut Storage, todo: &Ldd) -> Result<(), MercError> { - let proj = project(storage, todo, &self.project_ldd); + fn learn_successors(&mut self, storage: &LDDManagerRef, todo: &LDDFunction) -> Result<(), MercError> { + let proj = todo.project(&self.project_ldd)?; // Reused across short states to avoid per-iteration allocation. let mut read_values: Vec<*const _aterm> = Vec::with_capacity(self.read_indices.len()); let mut interleaved_values: Vec = vec![0; self.read_indices.len() + self.write_indices.len()]; - for_each_mut(storage, &proj, |storage, short_state| { + let mut states = iter(&proj); + while let Some(short_state) = states.next() { debug_assert_eq!( short_state.len(), self.read_indices.len(), @@ -362,7 +361,7 @@ impl TransitionGroup for SymbolicSummand { ); for (offset, value) in self.read_positions.iter().zip(short_state.iter()) { - interleaved_values[*offset as usize] = *value; + interleaved_values[*offset] = *value; } self.shared.context.enumerate_raw( @@ -382,7 +381,7 @@ impl TransitionGroup for SymbolicSummand { { let mut mapping = self.shared.mapping.borrow_mut(); for (&offset, (i, value)) in self.write_positions.iter().zip(values.iter().enumerate()) { - interleaved_values[offset as usize] = *mapping[self.write_indices[i] as usize] + interleaved_values[offset] = *mapping[self.write_indices[i] as usize] .insert(DataExpression::from(ATerm::from_ptr(*value))) .0 as Value; } @@ -393,15 +392,16 @@ impl TransitionGroup for SymbolicSummand { short_state.iter().join(", "), self.write_positions .iter() - .map(|&pos| interleaved_values[pos as usize]) + .map(|&pos| interleaved_values[pos]) .join(", ") ); - let cube = singleton(storage, &interleaved_values); - self.relation = union(storage, &self.relation, &cube); + let cube = + LDDFunction::singleton(storage, &interleaved_values).expect("Failed to allocate LDD singleton"); + self.relation = self.relation.union(&cube).expect("Failed to allocate LDD union"); }, ); - }); + } Ok(()) } @@ -450,8 +450,6 @@ mod tests { use std::process::Command; use mcrl2::read_lps; - use merc_ldd::Storage; - use merc_ldd::len; use merc_utilities::Timing; use super::explore_lps_symbolic; @@ -480,11 +478,11 @@ mod tests { let lps = read_lps(lps_path.to_str().expect("LPS path is valid UTF-8")).expect("Failed to read LPS"); - let mut storage = Storage::new(); + let storage = oxidd::ldd::new_manager(1 << 20, 1 << 20, 1); let timing = Timing::new(); - let states = explore_lps_symbolic(&mut storage, &lps, &timing).expect("Failed to explore LPS"); - let num_of_states = len(&mut storage, &states); + let states = explore_lps_symbolic(&storage, &lps, &timing).expect("Failed to explore LPS"); + let num_of_states = states.len(); assert_eq!( num_of_states, 74, diff --git a/tools/mcrl2/lps/src/main.rs b/tools/mcrl2/lps/src/main.rs index aa4e26295..51816782c 100644 --- a/tools/mcrl2/lps/src/main.rs +++ b/tools/mcrl2/lps/src/main.rs @@ -6,8 +6,6 @@ use std::process::ExitCode; use clap::Parser; use clap::Subcommand; -use merc_ldd::Storage; -use merc_ldd::len; use merc_lts::LTS; use merc_lts::LtsBuilderFast; use merc_lts::StateIndex; @@ -29,6 +27,9 @@ use explore_symbolic::explore_lps_symbolic; mod explore_explicit; mod explore_symbolic; +/// Default number of nodes for the Oxidd LDD manager. +const DEFAULT_OXIDD_NODE_CAPACITY: usize = 1 << 24; + #[derive(clap::ValueEnum, Clone, Debug)] enum LpsFormat { Lps, @@ -47,10 +48,31 @@ struct Cli { #[arg(long, global = true)] timings: bool, + /// The number of worker threads for the Oxidd LDD manager. + #[arg(long, global = true, default_value_t = 1)] + oxidd_workers: u32, + + /// The number of nodes for the Oxidd LDD manager. + #[arg(long, global = true, default_value_t = DEFAULT_OXIDD_NODE_CAPACITY)] + oxidd_node_capacity: usize, + + /// The apply cache capacity for the Oxidd LDD manager, defaults to the node capacity. + #[arg(long, global = true)] + oxidd_cache_capacity: Option, + #[command(subcommand)] commands: Option, } +/// Initializes the Oxidd LDD manager based on CLI arguments. +fn init_ldd_manager(cli: &Cli) -> oxidd::ldd::LDDManagerRef { + oxidd::ldd::new_manager( + cli.oxidd_node_capacity, + cli.oxidd_cache_capacity.unwrap_or(cli.oxidd_node_capacity), + cli.oxidd_workers, + ) +} + #[derive(Debug, Subcommand)] enum Commands { /// Explores the state space of an LPS symbolically @@ -101,9 +123,9 @@ fn main() -> Result { let timing = Timing::new(); - if let Some(command) = cli.commands { + if let Some(command) = &cli.commands { match command { - Commands::Explore(args) => handle_explore(args, &timing)?, + Commands::Explore(args) => handle_explore(&cli, args, &timing)?, Commands::ExploreExplicit(args) => handle_explore_explicit(args, &timing)?, } } @@ -117,22 +139,22 @@ fn main() -> Result { Ok(ExitCode::SUCCESS) } -fn handle_explore(args: ExploreArgs, timing: &Timing) -> Result<(), MercError> { - let format = args.format.unwrap_or(LpsFormat::Lps); +fn handle_explore(cli: &Cli, args: &ExploreArgs, timing: &Timing) -> Result<(), MercError> { + let format = args.format.clone().unwrap_or(LpsFormat::Lps); let lps = match format { LpsFormat::Lps => read_lps(&args.filename)?, }; - let mut storage = Storage::new(); + let storage = init_ldd_manager(cli); - let num_of_states = explore_lps_symbolic(&mut storage, &lps, timing)?; - println!("Number of states: {}", len(&mut storage, &num_of_states)); + let states = explore_lps_symbolic(&storage, &lps, timing)?; + println!("Number of states: {}", states.len()); Ok(()) } -fn handle_explore_explicit(args: ExploreExplicitArgs, timing: &Timing) -> Result<(), MercError> { - let format = args.format.unwrap_or(LpsFormat::Lps); +fn handle_explore_explicit(args: &ExploreExplicitArgs, timing: &Timing) -> Result<(), MercError> { + let format = args.format.clone().unwrap_or(LpsFormat::Lps); let lps = match format { LpsFormat::Lps => read_lps(&args.filename)?, }; diff --git a/tools/sym/Cargo.toml b/tools/sym/Cargo.toml index d52a31b36..bdc10b261 100644 --- a/tools/sym/Cargo.toml +++ b/tools/sym/Cargo.toml @@ -7,7 +7,6 @@ rust-version.workspace = true [dependencies] merc_io.workspace = true -merc_ldd.workspace = true merc_lts = { workspace = true, features = ["clap"] } merc_symbolic = { workspace = true, features = ["clap"] } merc_tools.workspace = true diff --git a/tools/sym/src/main.rs b/tools/sym/src/main.rs index 3c8926ae0..f2bdc022b 100644 --- a/tools/sym/src/main.rs +++ b/tools/sym/src/main.rs @@ -8,8 +8,6 @@ use clap::Subcommand; use itertools::Itertools; use merc_io::LargeFormatter; -use merc_ldd::Storage; -use merc_ldd::len; use merc_lts::AutStream; use merc_lts::LtsBuilderMem; use merc_lts::LtsFormat; @@ -202,6 +200,15 @@ fn init_bdd_manager(cli: &Cli) -> oxidd::bdd::BDDManagerRef { ) } +/// Initializes the Oxidd LDD manager based on CLI arguments. +fn init_ldd_manager(cli: &Cli) -> oxidd::ldd::LDDManagerRef { + oxidd::ldd::new_manager( + cli.oxidd_node_capacity, + cli.oxidd_cache_capacity.unwrap_or(cli.oxidd_node_capacity), + cli.oxidd_workers, + ) +} + fn main() -> Result { let cli = Cli::parse(); @@ -219,10 +226,10 @@ fn main() -> Result { if let Some(command) = &cli.commands { match command { - Commands::Info(args) => handle_info(args, &timing)?, + Commands::Info(args) => handle_info(&cli, args, &timing)?, Commands::Explore(args) => handle_explore(&cli, args, &timing)?, Commands::Reorder(args) => handle_reorder(args, &timing)?, - Commands::Convert(args) => handle_convert(args, &timing)?, + Commands::Convert(args) => handle_convert(&cli, args, &timing)?, Commands::Reduce(args) => handle_reduce(&cli, args, &timing)?, } } @@ -236,8 +243,8 @@ fn main() -> Result { } /// Reads the given symbolic LTS and prints information about it. -fn handle_info(args: &InfoArgs, timing: &Timing) -> Result<(), MercError> { - let mut storage = Storage::new(); +fn handle_info(cli: &Cli, args: &InfoArgs, timing: &Timing) -> Result<(), MercError> { + let storage = init_ldd_manager(cli); let format = guess_format_from_extension(&args.filename, args.format).ok_or("Cannot determine input symbolic LTS format")?; @@ -247,13 +254,10 @@ fn handle_info(args: &InfoArgs, timing: &Timing) -> Result<(), MercError> { } let lts = timing.measure("read_symbolic_lts", || { - read_symbolic_lts(&mut storage, File::open(&args.filename)?) + read_symbolic_lts(&storage, File::open(&args.filename)?) })?; - println!( - "Number of states: {}", - LargeFormatter(merc_ldd::len(&mut storage, lts.states())) - ); + println!("Number of states: {}", LargeFormatter(lts.states().len())); println!("Number of summand groups: {}", lts.transition_groups().len()); Ok(()) @@ -261,19 +265,19 @@ fn handle_info(args: &InfoArgs, timing: &Timing) -> Result<(), MercError> { /// Explores the given symbolic LTS. fn handle_explore(cli: &Cli, args: &ExploreArgs, timing: &Timing) -> Result<(), MercError> { - let mut storage = Storage::new(); + let storage = init_ldd_manager(cli); let format = guess_format_from_extension(&args.filename, args.format).ok_or("Cannot determine input format")?; let mut file = File::open(&args.filename)?; match format { SymFormat::Sylvan => { - let mut lts = timing.measure("read_symbolic_lts", || read_sylvan(&mut storage, &mut file))?; - explore_impl(&mut storage, cli, args, &mut lts, timing)?; + let mut lts = timing.measure("read_symbolic_lts", || read_sylvan(&storage, &mut file))?; + explore_impl(&storage, cli, args, &mut lts, timing)?; } SymFormat::Sym => { - let mut lts = timing.measure("read_symbolic_lts", || read_symbolic_lts(&mut storage, &mut file))?; - explore_impl(&mut storage, cli, args, &mut lts, timing)?; + let mut lts = timing.measure("read_symbolic_lts", || read_symbolic_lts(&storage, &mut file))?; + explore_impl(&storage, cli, args, &mut lts, timing)?; } } @@ -281,7 +285,7 @@ fn handle_explore(cli: &Cli, args: &ExploreArgs, timing: &Timing) -> Result<(), } fn explore_impl( - storage: &mut Storage, + storage: &oxidd::ldd::LDDManagerRef, cli: &Cli, args: &ExploreArgs, lts: &mut L, @@ -312,7 +316,7 @@ fn explore_impl( timing.measure("explore", || -> Result<_, MercError> { let states = reachability(storage, lts, timing)?; - Ok(len(storage, &states)) + Ok(states.len()) })? ); } @@ -402,8 +406,8 @@ fn handle_reorder(args: &ReorderArgs, _timing: &Timing) -> Result<(), MercError> } /// Converts a symbolic LTS to an explicit LTS. -fn handle_convert(args: &ConvertArgs, _timing: &Timing) -> Result<(), MercError> { - let mut storage = Storage::new(); +fn handle_convert(cli: &Cli, args: &ConvertArgs, _timing: &Timing) -> Result<(), MercError> { + let storage = init_ldd_manager(cli); let format = guess_format_from_extension(&args.filename, args.format).ok_or("Cannot determine input symbolic LTS format")?; @@ -412,7 +416,7 @@ fn handle_convert(args: &ConvertArgs, _timing: &Timing) -> Result<(), MercError> } let mut file = File::open(&args.filename)?; - let lts = read_symbolic_lts(&mut storage, &mut file)?; + let lts = read_symbolic_lts(&storage, &mut file)?; if let Some(output) = &args.output { let output_format = @@ -425,16 +429,16 @@ fn handle_convert(args: &ConvertArgs, _timing: &Timing) -> Result<(), MercError> LtsFormat::Aut => { let mut output = File::create(output)?; let mut stream = AutStream::new(&mut output); - convert_symbolic_lts(&mut storage, &mut stream, <s)?; + convert_symbolic_lts(&storage, &mut stream, <s)?; } LtsFormat::AutMcrl2 => { let mut output = File::create(output)?; let mut stream = AutStream::new_mcrl2(&mut output); - convert_symbolic_lts(&mut storage, &mut stream, <s)?; + convert_symbolic_lts(&storage, &mut stream, <s)?; } LtsFormat::Bcg => { let explicit_lts = - convert_symbolic_lts(&mut storage, &mut LtsBuilderMem::new(Vec::new(), Vec::new()), <s)?; + convert_symbolic_lts(&storage, &mut LtsBuilderMem::new(Vec::new(), Vec::new()), <s)?; write_bcg(&explicit_lts, output)?; } } @@ -451,14 +455,14 @@ fn handle_reduce(cli: &Cli, args: &ReduceArgs, timing: &Timing) -> Result<(), Me return Err("Currently only the .sym format is supported for reduction".into()); } - let mut storage = Storage::new(); + let storage = init_ldd_manager(cli); let manager_ref = init_bdd_manager(cli); let mut file = File::open(&args.filename)?; - let lts = read_symbolic_lts(&mut storage, &mut file)?; + let lts = read_symbolic_lts(&storage, &mut file)?; let lts_bdd = timing.measure("convert_bdd", || { - SymbolicLtsBdd::from_symbolic_lts(&mut storage, &manager_ref, <s) + SymbolicLtsBdd::from_symbolic_lts(&storage, &manager_ref, <s) })?; let quotient_lts = timing.measure("reduction", || -> Result, MercError> {