From 1c00514076e17b6936a3909651fd48c3790a5987 Mon Sep 17 00:00:00 2001 From: Tim Beurskens Date: Wed, 28 Jun 2023 12:10:12 +0200 Subject: [PATCH 1/4] update random graph generator --- Cargo.lock | 267 +++++++++++++++++++---------------- Cargo.toml | 1 + random_graph_gen/Cargo.toml | 5 +- random_graph_gen/src/main.rs | 99 +++++++++---- 4 files changed, 225 insertions(+), 147 deletions(-) diff --git a/Cargo.lock b/Cargo.lock index 049e120..a4378db 100644 --- a/Cargo.lock +++ b/Cargo.lock @@ -4,13 +4,68 @@ version = 3 [[package]] name = "aho-corasick" -version = "0.7.20" +version = "1.0.2" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "cc936419f96fa211c1b9166887b38e5e40b19958e5b895be7c1f93adec7071ac" +checksum = "43f6cb1bf222025340178f382c426f13757b2960e89779dfcb319c32542a5a41" dependencies = [ "memchr", ] +[[package]] +name = "anstream" +version = "0.3.2" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "0ca84f3628370c59db74ee214b3263d58f9aadd9b4fe7e711fd87dc452b7f163" +dependencies = [ + "anstyle", + "anstyle-parse", + "anstyle-query", + "anstyle-wincon", + "colorchoice", + "is-terminal", + "utf8parse", +] + +[[package]] +name = "anstyle" +version = "1.0.1" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "3a30da5c5f2d5e72842e00bcb57657162cdabef0931f40e2deb9b4140440cecd" + +[[package]] +name = "anstyle-parse" +version = "0.2.1" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "938874ff5980b03a87c5524b3ae5b59cf99b1d6bc836848df7bc5ada9643c333" +dependencies = [ + "utf8parse", +] + +[[package]] +name = "anstyle-query" +version = "1.0.0" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "5ca11d4be1bab0c8bc8734a9aa7bf4ee8316d462a08c6ac5052f888fef5b494b" +dependencies = [ + "windows-sys", +] + +[[package]] +name = "anstyle-wincon" +version = "1.0.1" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "180abfa45703aebe0093f79badacc01b8fd4ea2e35118747e5811127f926e188" +dependencies = [ + "anstyle", + "windows-sys", +] + +[[package]] +name = "anyhow" +version = "1.0.71" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "9c7d0618f0e0b7e8ff11427422b64564d5fb0be1940354bfe2e0529b18a9d9b8" + [[package]] name = "bitflags" version = "1.3.2" @@ -31,46 +86,57 @@ checksum = "baf1de4339761588bc0619e3cbc0120ee582ebb74b53b4efbf79117bd2da40fd" [[package]] name = "clap" -version = "4.1.8" +version = "4.3.8" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "c3d7ae14b20b94cb02149ed21a86c423859cbe18dc7ed69845cace50e52b40a5" +checksum = "d9394150f5b4273a1763355bd1c2ec54cc5a2593f790587bcd6b2c947cfa9211" dependencies = [ - "bitflags", + "clap_builder", "clap_derive", - "clap_lex", - "is-terminal", "once_cell", +] + +[[package]] +name = "clap_builder" +version = "4.3.8" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "9a78fbdd3cc2914ddf37ba444114bc7765bbdcb55ec9cbe6fa054f0137400717" +dependencies = [ + "anstream", + "anstyle", + "bitflags", + "clap_lex", "strsim", - "termcolor", ] [[package]] name = "clap_derive" -version = "4.1.8" +version = "4.3.2" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "44bec8e5c9d09e439c4335b1af0abaab56dcf3b94999a936e1bb47b9134288f0" +checksum = "b8cd2b2a819ad6eec39e8f1d6b53001af1e5469f8c177579cdaeb313115b825f" dependencies = [ "heck", - "proc-macro-error", "proc-macro2", "quote", - "syn", + "syn 2.0.22", ] [[package]] name = "clap_lex" -version = "0.3.2" +version = "0.5.0" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "350b9cf31731f9957399229e9b2adc51eeabdfbe9d71d9a0552275fd12710d09" -dependencies = [ - "os_str_bytes", -] +checksum = "2da6da31387c7e4ef160ffab6d5e7f00c42626fe39aea70a7b0f1773f7dd6c1b" + +[[package]] +name = "colorchoice" +version = "1.0.0" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "acbf1af155f9b9ef647e42cdc158db4b64a1b61f743629225fde6f3e0be2a7c7" [[package]] name = "csv" -version = "1.2.0" +version = "1.2.2" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "af91f40b7355f82b0a891f50e70399475945bb0b0da4f1700ce60761c9d3e359" +checksum = "626ae34994d3d8d668f4269922248239db4ae42d538b14c398b74a52208e8086" dependencies = [ "csv-core", "itoa", @@ -94,7 +160,7 @@ source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "6d2301688392eb071b0bf1a37be05c469d3cc4dbbd95df672fe28ab021e6a096" dependencies = [ "quote", - "syn", + "syn 1.0.109", ] [[package]] @@ -117,13 +183,13 @@ checksum = "7fcaabb2fef8c910e7f4c7ce9f67a1283a1715879a7c230ca9d6d1ae31f16d91" [[package]] name = "errno" -version = "0.2.8" +version = "0.3.1" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "f639046355ee4f37944e44f60642c6f3a7efa3cf6b78c78a0d989a8ce6c396a1" +checksum = "4bcfec3a70f97c962c307b2d2c56e358cf1d00b558d74262b5f929ee8cc7e73a" dependencies = [ "errno-dragonfly", "libc", - "winapi", + "windows-sys", ] [[package]] @@ -138,9 +204,9 @@ dependencies = [ [[package]] name = "getrandom" -version = "0.2.8" +version = "0.2.10" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "c05aeb6a22b8f62540c194aac980f2115af067bfe15a0734d7277a768d396b31" +checksum = "be4136b2a15dd319360be1c07d9933517ccf0be8f16bf62a3bee4f0d618df427" dependencies = [ "cfg-if", "libc", @@ -167,19 +233,20 @@ checksum = "fed44880c466736ef9a5c5b5facefb5ed0785676d0c02d612db14e54f0d84286" [[package]] name = "io-lifetimes" -version = "1.0.5" +version = "1.0.11" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "1abeb7a0dd0f8181267ff8adc397075586500b81b28a73e8a0208b00fc170fb3" +checksum = "eae7b9aee968036d54dce06cebaefd919e4472e753296daccd6d344e3e2df0c2" dependencies = [ + "hermit-abi", "libc", "windows-sys", ] [[package]] name = "is-terminal" -version = "0.4.4" +version = "0.4.7" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "21b6b32576413a8e69b90e952e4a026476040d81017b80445deda5f2d3921857" +checksum = "adcf93614601c8129ddf72e2d5633df827ba6551541c6d8c59520a371475be1f" dependencies = [ "hermit-abi", "io-lifetimes", @@ -198,9 +265,9 @@ dependencies = [ [[package]] name = "itoa" -version = "1.0.5" +version = "1.0.6" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "fad582f4b9e86b6caa621cabeb0963332d92eea04729ab12892c2533951e6440" +checksum = "453ad9f582a441959e5f0d088b02ce04cfe8d51a8eaf077f12ac6d3e94164ca6" [[package]] name = "lazy_static" @@ -210,15 +277,15 @@ checksum = "e2abad23fbc42b3700f2f279844dc832adb2b2eb069b2df918f455c4e18cc646" [[package]] name = "libc" -version = "0.2.139" +version = "0.2.147" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "201de327520df007757c1f0adce6e827fe8562fbc28bfd9c15571c66ca1f5f79" +checksum = "b4668fb0ea861c1df094127ac5f1da3409a82116a4ba74fca2e58ef927159bb3" [[package]] name = "linux-raw-sys" -version = "0.1.4" +version = "0.3.8" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "f051f77a7c8e6957c0696eac88f26b0117e54f52d3fc682ab19397a8812846a4" +checksum = "ef53942eb7bf7ff43a617b3e2c1c4a5ecf5944a7c1bc12d7ee39bbb15e5c1519" [[package]] name = "max_clique_gen" @@ -244,15 +311,9 @@ dependencies = [ [[package]] name = "once_cell" -version = "1.17.1" +version = "1.18.0" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "b7e5500299e16ebb147ae15a00a942af264cf3688f47923b8fc2cd5858f23ad3" - -[[package]] -name = "os_str_bytes" -version = "6.4.1" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "9b7820b9daea5457c9f21c69448905d723fbd21136ccf521748f23fd49e723ee" +checksum = "dd8b5dd2ae5ed71462c540258bedcb51965123ad7e7ccf4b9a8cafaa4a63576d" [[package]] name = "output_vt100" @@ -281,44 +342,20 @@ dependencies = [ "yansi", ] -[[package]] -name = "proc-macro-error" -version = "1.0.4" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "da25490ff9892aab3fcf7c36f08cfb902dd3e71ca0f9f9517bea02a73a5ce38c" -dependencies = [ - "proc-macro-error-attr", - "proc-macro2", - "quote", - "syn", - "version_check", -] - -[[package]] -name = "proc-macro-error-attr" -version = "1.0.4" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "a1be40180e52ecc98ad80b184934baf3d0d29f979574e439af5a55274b35f869" -dependencies = [ - "proc-macro2", - "quote", - "version_check", -] - [[package]] name = "proc-macro2" -version = "1.0.51" +version = "1.0.63" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "5d727cae5b39d21da60fa540906919ad737832fe0b1c165da3a34d6548c849d6" +checksum = "7b368fba921b0dce7e60f5e04ec15e565b3303972b42bcfde1d0713b881959eb" dependencies = [ "unicode-ident", ] [[package]] name = "quote" -version = "1.0.23" +version = "1.0.28" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "8856d8364d252a14d474036ea1358d63c9e6965c8e5c1885c18f73d70bff9c7b" +checksum = "1b9ab9c7eadfd8df19006f1cf1a4aed13540ed5cbc047010ece5826e10825488" dependencies = [ "proc-macro2", ] @@ -355,8 +392,9 @@ dependencies = [ [[package]] name = "random_graph_gen" -version = "0.1.0" +version = "0.2.0" dependencies = [ + "anyhow", "clap", "csv", "rand", @@ -365,9 +403,9 @@ dependencies = [ [[package]] name = "regex" -version = "1.7.1" +version = "1.8.4" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "48aaa5748ba571fb95cd2c85c09f629215d3a6ece942baa100950af03a34f733" +checksum = "d0ab3ca65655bb1e41f2a8c8cd662eb4fb035e67c3f78da1d61dffe89d07300f" dependencies = [ "aho-corasick", "memchr", @@ -376,9 +414,9 @@ dependencies = [ [[package]] name = "regex-syntax" -version = "0.6.28" +version = "0.7.2" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "456c603be3e8d448b072f410900c09faf164fbce2d480456f50eea6e25f9c848" +checksum = "436b050e76ed2903236f032a59761c1eb99e1b0aead2c257922771dab1fc8c78" [[package]] name = "rsbdd" @@ -404,9 +442,9 @@ checksum = "08d43f7aa6b08d49f382cde6a7982047c3426db949b1424bc4b7ec9ae12c6ce2" [[package]] name = "rustix" -version = "0.36.8" +version = "0.37.20" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "f43abb88211988493c1abb44a70efa56ff0ce98f233b7b276146f1f3f7ba9644" +checksum = "b96e891d04aa506a6d1f318d2771bcb1c7dfda84e126660ace067c9b474bb2c0" dependencies = [ "bitflags", "errno", @@ -418,15 +456,15 @@ dependencies = [ [[package]] name = "ryu" -version = "1.0.12" +version = "1.0.13" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "7b4b9743ed687d4b4bcedf9ff5eaa7398495ae14e61cba0a295704edbc7decde" +checksum = "f91339c0467de62360649f8d3e185ca8de4224ff281f66000de5eb2a77a79041" [[package]] name = "serde" -version = "1.0.152" +version = "1.0.164" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "bb7d1f0d3021d347a83e556fc4683dea2ea09d87bccdf88ff5c12545d89d5efb" +checksum = "9e8c8cf938e98f769bc164923b06dce91cea1751522f46f8466461af04c9027d" [[package]] name = "strsim" @@ -453,25 +491,27 @@ dependencies = [ ] [[package]] -name = "termcolor" -version = "1.2.0" +name = "syn" +version = "2.0.22" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "be55cf8942feac5c765c2c993422806843c9a9a45d4d5c407ad6dd2ea95eb9b6" +checksum = "2efbeae7acf4eabd6bcdcbd11c92f45231ddda7539edc7806bd1a04a03b24616" dependencies = [ - "winapi-util", + "proc-macro2", + "quote", + "unicode-ident", ] [[package]] name = "unicode-ident" -version = "1.0.6" +version = "1.0.9" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "84a22b9f218b40614adcb3f4ff08b703773ad44fa9423e4e0d346d5db86e4ebc" +checksum = "b15811caf2415fb889178633e7724bad2509101cde276048e013b9def5e51fa0" [[package]] -name = "version_check" -version = "0.9.4" +name = "utf8parse" +version = "0.2.1" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "49874b5167b65d7193b8aba1567f5c7d93d001cafc34600cee003eda787e483f" +checksum = "711b9620af191e0cdc7468a8d14e709c3dcdb115b36f838e601583af800a370a" [[package]] name = "wasi" @@ -495,15 +535,6 @@ version = "0.4.0" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "ac3b87c63620426dd9b991e5ce0329eff545bccbbb34f3be09ff6fb6ab51b7b6" -[[package]] -name = "winapi-util" -version = "0.1.5" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "70ec6ce85bb158151cae5e5c87f95a8e97d2c0c4b001223f33a334e3ce5de178" -dependencies = [ - "winapi", -] - [[package]] name = "winapi-x86_64-pc-windows-gnu" version = "0.4.0" @@ -512,18 +543,18 @@ checksum = "712e227841d057c1ee1cd2fb22fa7e5a5461ae8e48fa2ca79ec42cfc1931183f" [[package]] name = "windows-sys" -version = "0.45.0" +version = "0.48.0" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "75283be5efb2831d37ea142365f009c02ec203cd29a3ebecbc093d52315b66d0" +checksum = "677d2418bec65e3338edb076e806bc1ec15693c5d0104683f2efe857f61056a9" dependencies = [ "windows-targets", ] [[package]] name = "windows-targets" -version = "0.42.1" +version = "0.48.0" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "8e2522491fbfcd58cc84d47aeb2958948c4b8982e9a2d8a2a35bbaed431390e7" +checksum = "7b1eb6f0cd7c80c79759c929114ef071b87354ce476d9d94271031c0497adfd5" dependencies = [ "windows_aarch64_gnullvm", "windows_aarch64_msvc", @@ -536,45 +567,45 @@ dependencies = [ [[package]] name = "windows_aarch64_gnullvm" -version = "0.42.1" +version = "0.48.0" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "8c9864e83243fdec7fc9c5444389dcbbfd258f745e7853198f365e3c4968a608" +checksum = "91ae572e1b79dba883e0d315474df7305d12f569b400fcf90581b06062f7e1bc" [[package]] name = "windows_aarch64_msvc" -version = "0.42.1" +version = "0.48.0" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "4c8b1b673ffc16c47a9ff48570a9d85e25d265735c503681332589af6253c6c7" +checksum = "b2ef27e0d7bdfcfc7b868b317c1d32c641a6fe4629c171b8928c7b08d98d7cf3" [[package]] name = "windows_i686_gnu" -version = "0.42.1" +version = "0.48.0" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "de3887528ad530ba7bdbb1faa8275ec7a1155a45ffa57c37993960277145d640" +checksum = "622a1962a7db830d6fd0a69683c80a18fda201879f0f447f065a3b7467daa241" [[package]] name = "windows_i686_msvc" -version = "0.42.1" +version = "0.48.0" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "bf4d1122317eddd6ff351aa852118a2418ad4214e6613a50e0191f7004372605" +checksum = "4542c6e364ce21bf45d69fdd2a8e455fa38d316158cfd43b3ac1c5b1b19f8e00" [[package]] name = "windows_x86_64_gnu" -version = "0.42.1" +version = "0.48.0" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "c1040f221285e17ebccbc2591ffdc2d44ee1f9186324dd3e84e99ac68d699c45" +checksum = "ca2b8a661f7628cbd23440e50b05d705db3686f894fc9580820623656af974b1" [[package]] name = "windows_x86_64_gnullvm" -version = "0.42.1" +version = "0.48.0" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "628bfdf232daa22b0d64fdb62b09fcc36bb01f05a3939e20ab73aaf9470d0463" +checksum = "7896dbc1f41e08872e9d5e8f8baa8fdd2677f29468c4e156210174edc7f7b953" [[package]] name = "windows_x86_64_msvc" -version = "0.42.1" +version = "0.48.0" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "447660ad36a13288b1db4d4248e857b510e8c3a225c822ba4fb748c0aafecffd" +checksum = "1a515f5799fe4961cb532f983ce2b23082366b898e52ffbce459c86f67c8378a" [[package]] name = "yansi" diff --git a/Cargo.toml b/Cargo.toml index 758b8cb..ba6859a 100644 --- a/Cargo.toml +++ b/Cargo.toml @@ -38,3 +38,4 @@ csv = "1.2" regex = "1.7" glob = "0.3" pretty_assertions = "1.3" +anyhow = "1.0" \ No newline at end of file diff --git a/random_graph_gen/Cargo.toml b/random_graph_gen/Cargo.toml index 9f023e8..11dabfb 100644 --- a/random_graph_gen/Cargo.toml +++ b/random_graph_gen/Cargo.toml @@ -1,6 +1,6 @@ [package] name = "random_graph_gen" -version = "0.1.0" +version = "0.2.0" description = "Generates a random edge list formatted graph" edition.workspace = true authors.workspace = true @@ -9,4 +9,5 @@ authors.workspace = true clap.workspace = true rand.workspace = true rustc-hash.workspace = true -csv.workspace = true \ No newline at end of file +csv.workspace = true +anyhow.workspace = true \ No newline at end of file diff --git a/random_graph_gen/src/main.rs b/random_graph_gen/src/main.rs index 083ae09..107c157 100644 --- a/random_graph_gen/src/main.rs +++ b/random_graph_gen/src/main.rs @@ -26,6 +26,10 @@ struct Args { /// Use undirected edges (test for both directions in the set-complement operation) undirected: bool, + #[clap(long)] + /// Construct a complete graph + complete: bool, + #[clap(short, long)] /// Output in dot (GraphViz) format dot: bool, @@ -39,23 +43,41 @@ struct Args { colors: Option, } -fn main() -> io::Result<()> { +fn main() -> anyhow::Result<()> { let args = Args::parse(); let mut selection = if let Some(file_to_convert) = args.convert { - let file = File::open(file_to_convert).expect("Could not open file"); + let file = File::open(file_to_convert)?; let mut bufreader = BufReader::new(file); - read_graph(&mut bufreader, args.undirected).expect("Could not parse edge list") + read_graph(&mut bufreader, args.undirected)? + } else if args.complete { + if args.vertices.is_none() { + Err(anyhow::anyhow!( + "Must provide vertices for a complete graph" + ))? + } + + let vertices = args.vertices.unwrap(); + + let edges = if args.undirected { + (vertices * (vertices - 1)) / 2 + } else { + vertices * (vertices - 1) + }; + + generate_graph(vertices, edges, args.undirected)? } else { if args.vertices.is_none() || args.edges.is_none() { - panic!("Must provide vertices and edges if not converting a graph"); + Err(anyhow::anyhow!( + "Must provide vertices and edges if not converting a graph" + ))? } - generate_graph(args.vertices.unwrap(), args.edges.unwrap(), args.undirected) + generate_graph(args.vertices.unwrap(), args.edges.unwrap(), args.undirected)? }; // convert to a graph-coloring problem if let Some(num_colors) = args.colors { - selection = augment_colors(&selection, num_colors); + selection = augment_colors(&selection, num_colors)?; } let mut writer = if let Some(output_file) = args.output { @@ -86,7 +108,7 @@ fn main() -> io::Result<()> { } // flush the writer before dropping it - writer.flush().expect("Could not flush write buffer"); + writer.flush()?; Ok(()) } @@ -115,7 +137,7 @@ fn generate_graph( num_vertices: usize, num_edges: usize, undirected: bool, -) -> Vec<(String, String)> { +) -> anyhow::Result> { let mut rng = rand::thread_rng(); let vertices = (0..num_vertices) @@ -125,8 +147,15 @@ fn generate_graph( for (i, v1) in vertices.iter().enumerate() { if undirected { - for v2 in vertices[(i + 1)..].iter() { - edges.push((v1.clone(), v2.clone())); + if let Some(vertices) = vertices.get((i + 1)..) { + for v2 in vertices.iter() { + edges.push((v1.clone(), v2.clone())); + } + } else { + Err(anyhow::anyhow!( + "Index out of bounds for vertex range {}..", + i + 1 + ))? } } else { for (j, v2) in vertices.iter().enumerate() { @@ -139,10 +168,19 @@ fn generate_graph( edges.shuffle(&mut rng); - edges[0..num_edges].to_vec() + if let Some(edges) = edges.get(0..num_edges) { + Ok(edges.to_vec()) + } else { + Err(anyhow::anyhow!( + "Cannot satisfy the desired amount of edges" + )) + } } -fn augment_colors(edges: &Vec<(String, String)>, num_colors: usize) -> Vec<(String, String)> { +fn augment_colors( + edges: &Vec<(String, String)>, + num_colors: usize, +) -> anyhow::Result> { let mut vertex_map: FxHashMap = FxHashMap::default(); let mut color_map: FxHashMap = FxHashMap::default(); @@ -164,23 +202,30 @@ fn augment_colors(edges: &Vec<(String, String)>, num_colors: usize) -> Vec<(Stri let vertices = vertex_map.keys().cloned().collect::>(); for (i, v1) in vertices.iter().enumerate() { - for v2 in vertices[(i + 1)..].iter() { - let c1 = color_map[v1]; - let c2 = color_map[v2]; - - let ov1 = &vertex_map[v1]; - let ov2 = &vertex_map[v2]; - - // only add an edge to new_edges if the colors are different, or the vertices are not connected - if ov1 != ov2 - && (c1 != c2 - || (!edges.contains(&(ov1.clone(), ov2.clone())) - && !edges.contains(&(ov2.clone(), ov1.clone())))) - { - new_edges.push((v1.clone(), v2.clone())); + if let Some(vertices) = vertices.get((i + 1)..) { + for v2 in vertices.iter() { + let c1 = color_map[v1]; + let c2 = color_map[v2]; + + let ov1 = &vertex_map[v1]; + let ov2 = &vertex_map[v2]; + + // only add an edge to new_edges if the colors are different, or the vertices are not connected + if ov1 != ov2 + && (c1 != c2 + || (!edges.contains(&(ov1.clone(), ov2.clone())) + && !edges.contains(&(ov2.clone(), ov1.clone())))) + { + new_edges.push((v1.clone(), v2.clone())); + } } + } else { + Err(anyhow::anyhow!( + "Index out of bounds for vertex range {}..", + i + 1 + ))? } } - new_edges + Ok(new_edges) } From 52f716036876ac00b640adfbc07c5e8d1fbf31bf Mon Sep 17 00:00:00 2001 From: Tim Beurskens Date: Wed, 5 Apr 2023 11:21:34 +0200 Subject: [PATCH 2/4] rayon introduction --- Cargo.lock | 259 +++++++++++++++++++++++++++++++---------------------- Cargo.toml | 4 +- src/bdd.rs | 5 +- 3 files changed, 156 insertions(+), 112 deletions(-) diff --git a/Cargo.lock b/Cargo.lock index a4378db..97ddafe 100644 --- a/Cargo.lock +++ b/Cargo.lock @@ -62,15 +62,21 @@ dependencies = [ [[package]] name = "anyhow" -version = "1.0.71" +version = "1.0.72" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "9c7d0618f0e0b7e8ff11427422b64564d5fb0be1940354bfe2e0529b18a9d9b8" +checksum = "3b13c32d80ecc7ab747b80c3784bce54ee8a7a0cc4fbda9bf4cda2cf6fe90854" + +[[package]] +name = "autocfg" +version = "1.1.0" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "d468802bab17cbc0cc575e9b053f41e72aa36bfa6b7f55e3529ffa43161b97fa" [[package]] name = "bitflags" -version = "1.3.2" +version = "2.3.3" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "bef38d45163c2f1dde094a7dfd33ccf595c92905c8f8f4fdc18d06fb1037718a" +checksum = "630be753d4e58660abd17930c71b647fe46c27ea6b63cc59e1e3851406972e42" [[package]] name = "cc" @@ -86,9 +92,9 @@ checksum = "baf1de4339761588bc0619e3cbc0120ee582ebb74b53b4efbf79117bd2da40fd" [[package]] name = "clap" -version = "4.3.8" +version = "4.3.17" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "d9394150f5b4273a1763355bd1c2ec54cc5a2593f790587bcd6b2c947cfa9211" +checksum = "5b0827b011f6f8ab38590295339817b0d26f344aa4932c3ced71b45b0c54b4a9" dependencies = [ "clap_builder", "clap_derive", @@ -97,27 +103,26 @@ dependencies = [ [[package]] name = "clap_builder" -version = "4.3.8" +version = "4.3.17" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "9a78fbdd3cc2914ddf37ba444114bc7765bbdcb55ec9cbe6fa054f0137400717" +checksum = "9441b403be87be858db6a23edb493e7f694761acdc3343d5a0fcaafd304cbc9e" dependencies = [ "anstream", "anstyle", - "bitflags", "clap_lex", "strsim", ] [[package]] name = "clap_derive" -version = "4.3.2" +version = "4.3.12" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "b8cd2b2a819ad6eec39e8f1d6b53001af1e5469f8c177579cdaeb313115b825f" +checksum = "54a9bb5758fc5dfe728d1019941681eccaf0cf8a4189b692a0ee2f2ecf90a050" dependencies = [ "heck", "proc-macro2", "quote", - "syn 2.0.22", + "syn", ] [[package]] @@ -132,6 +137,49 @@ version = "1.0.0" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "acbf1af155f9b9ef647e42cdc158db4b64a1b61f743629225fde6f3e0be2a7c7" +[[package]] +name = "crossbeam-channel" +version = "0.5.8" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "a33c2bf77f2df06183c3aa30d1e96c0695a313d4f9c453cc3762a6db39f99200" +dependencies = [ + "cfg-if", + "crossbeam-utils", +] + +[[package]] +name = "crossbeam-deque" +version = "0.8.3" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "ce6fd6f855243022dcecf8702fef0c297d4338e226845fe067f6341ad9fa0cef" +dependencies = [ + "cfg-if", + "crossbeam-epoch", + "crossbeam-utils", +] + +[[package]] +name = "crossbeam-epoch" +version = "0.9.15" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "ae211234986c545741a7dc064309f67ee1e5ad243d0e48335adc0484d960bcc7" +dependencies = [ + "autocfg", + "cfg-if", + "crossbeam-utils", + "memoffset", + "scopeguard", +] + +[[package]] +name = "crossbeam-utils" +version = "0.8.16" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "5a22b2d63d4d1dc0b7f1b6b2747dd0088008a9be28b6ddf0b1e7d335e3037294" +dependencies = [ + "cfg-if", +] + [[package]] name = "csv" version = "1.2.2" @@ -153,16 +201,6 @@ dependencies = [ "memchr", ] -[[package]] -name = "ctor" -version = "0.1.26" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "6d2301688392eb071b0bf1a37be05c469d3cc4dbbd95df672fe28ab021e6a096" -dependencies = [ - "quote", - "syn 1.0.109", -] - [[package]] name = "diff" version = "0.1.13" @@ -227,29 +265,17 @@ checksum = "95505c38b4572b2d910cecb0281560f54b440a19336cbbcb27bf6ce6adc6f5a8" [[package]] name = "hermit-abi" -version = "0.3.1" +version = "0.3.2" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "fed44880c466736ef9a5c5b5facefb5ed0785676d0c02d612db14e54f0d84286" - -[[package]] -name = "io-lifetimes" -version = "1.0.11" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "eae7b9aee968036d54dce06cebaefd919e4472e753296daccd6d344e3e2df0c2" -dependencies = [ - "hermit-abi", - "libc", - "windows-sys", -] +checksum = "443144c8cdadd93ebf52ddb4056d257f5b52c04d3c804e657d19eb73fc33668b" [[package]] name = "is-terminal" -version = "0.4.7" +version = "0.4.9" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "adcf93614601c8129ddf72e2d5633df827ba6551541c6d8c59520a371475be1f" +checksum = "cb0889898416213fab133e1d33a0e5858a48177452750691bde3666d0fdbaf8b" dependencies = [ "hermit-abi", - "io-lifetimes", "rustix", "windows-sys", ] @@ -265,9 +291,9 @@ dependencies = [ [[package]] name = "itoa" -version = "1.0.6" +version = "1.0.9" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "453ad9f582a441959e5f0d088b02ce04cfe8d51a8eaf077f12ac6d3e94164ca6" +checksum = "af150ab688ff2122fcef229be89cb50dd66af9e01a4ff320cc137eecc9bacc38" [[package]] name = "lazy_static" @@ -283,9 +309,9 @@ checksum = "b4668fb0ea861c1df094127ac5f1da3409a82116a4ba74fca2e58ef927159bb3" [[package]] name = "linux-raw-sys" -version = "0.3.8" +version = "0.4.3" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "ef53942eb7bf7ff43a617b3e2c1c4a5ecf5944a7c1bc12d7ee39bbb15e5c1519" +checksum = "09fc20d2ca12cb9f044c93e3bd6d32d523e6e2ec3db4f7b2939cd99026ecd3f0" [[package]] name = "max_clique_gen" @@ -302,6 +328,15 @@ version = "2.5.0" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "2dffe52ecf27772e601905b7522cb4ef790d2cc203488bbd0e2fe85fcb74566d" +[[package]] +name = "memoffset" +version = "0.9.0" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "5a634b1c61a95585bd15607c6ab0c4e5b226e695ff2800ba0cdccddf208c406c" +dependencies = [ + "autocfg", +] + [[package]] name = "n_queens_gen" version = "0.1.0" @@ -310,19 +345,20 @@ dependencies = [ ] [[package]] -name = "once_cell" -version = "1.18.0" +name = "num_cpus" +version = "1.16.0" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "dd8b5dd2ae5ed71462c540258bedcb51965123ad7e7ccf4b9a8cafaa4a63576d" +checksum = "4161fcb6d602d4d2081af7c3a45852d875a03dd337a6bfdd6e06407b61342a43" +dependencies = [ + "hermit-abi", + "libc", +] [[package]] -name = "output_vt100" -version = "0.1.3" +name = "once_cell" +version = "1.18.0" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "628223faebab4e3e40667ee0b2336d34a5b960ff60ea743ddfdbcf7770bcfb66" -dependencies = [ - "winapi", -] +checksum = "dd8b5dd2ae5ed71462c540258bedcb51965123ad7e7ccf4b9a8cafaa4a63576d" [[package]] name = "ppv-lite86" @@ -332,30 +368,28 @@ checksum = "5b40af805b3121feab8a3c29f04d8ad262fa8e0561883e7653e024ae4479e6de" [[package]] name = "pretty_assertions" -version = "1.3.0" +version = "1.4.0" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "a25e9bcb20aa780fd0bb16b72403a9064d6b3f22f026946029acb941a50af755" +checksum = "af7cee1a6c8a5b9208b3cb1061f10c0cb689087b3d8ce85fb9d2dd7a29b6ba66" dependencies = [ - "ctor", "diff", - "output_vt100", "yansi", ] [[package]] name = "proc-macro2" -version = "1.0.63" +version = "1.0.66" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "7b368fba921b0dce7e60f5e04ec15e565b3303972b42bcfde1d0713b881959eb" +checksum = "18fb31db3f9bddb2ea821cde30a9f70117e3f119938b5ee630b7403aa6e2ead9" dependencies = [ "unicode-ident", ] [[package]] name = "quote" -version = "1.0.28" +version = "1.0.31" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "1b9ab9c7eadfd8df19006f1cf1a4aed13540ed5cbc047010ece5826e10825488" +checksum = "5fe8a65d69dd0808184ebb5f836ab526bb259db23c657efa38711b1072ee47f0" dependencies = [ "proc-macro2", ] @@ -401,11 +435,45 @@ dependencies = [ "rustc-hash", ] +[[package]] +name = "rayon" +version = "1.7.0" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "1d2df5196e37bcc87abebc0053e20787d73847bb33134a69841207dd0a47f03b" +dependencies = [ + "either", + "rayon-core", +] + +[[package]] +name = "rayon-core" +version = "1.11.0" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "4b8f95bd6966f5c87776639160a66bd8ab9895d9d4ab01ddba9fc60661aebe8d" +dependencies = [ + "crossbeam-channel", + "crossbeam-deque", + "crossbeam-utils", + "num_cpus", +] + [[package]] name = "regex" -version = "1.8.4" +version = "1.9.1" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "d0ab3ca65655bb1e41f2a8c8cd662eb4fb035e67c3f78da1d61dffe89d07300f" +checksum = "b2eae68fc220f7cf2532e4494aded17545fce192d59cd996e0fe7887f4ceb575" +dependencies = [ + "aho-corasick", + "memchr", + "regex-automata", + "regex-syntax", +] + +[[package]] +name = "regex-automata" +version = "0.3.3" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "39354c10dd07468c2e73926b23bb9c2caca74c5501e38a35da70406f1d923310" dependencies = [ "aho-corasick", "memchr", @@ -414,9 +482,9 @@ dependencies = [ [[package]] name = "regex-syntax" -version = "0.7.2" +version = "0.7.4" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "436b050e76ed2903236f032a59761c1eb99e1b0aead2c257922771dab1fc8c78" +checksum = "e5ea92a5b6195c6ef2a0295ea818b312502c6fc94dde986c5553242e18fd4ce2" [[package]] name = "rsbdd" @@ -430,6 +498,7 @@ dependencies = [ "lazy_static", "pretty_assertions", "rand", + "rayon", "regex", "rustc-hash", ] @@ -442,13 +511,12 @@ checksum = "08d43f7aa6b08d49f382cde6a7982047c3426db949b1424bc4b7ec9ae12c6ce2" [[package]] name = "rustix" -version = "0.37.20" +version = "0.38.4" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "b96e891d04aa506a6d1f318d2771bcb1c7dfda84e126660ace067c9b474bb2c0" +checksum = "0a962918ea88d644592894bc6dc55acc6c0956488adcebbfb6e273506b7fd6e5" dependencies = [ "bitflags", "errno", - "io-lifetimes", "libc", "linux-raw-sys", "windows-sys", @@ -456,15 +524,21 @@ dependencies = [ [[package]] name = "ryu" -version = "1.0.13" +version = "1.0.15" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "1ad4cc8da4ef723ed60bced201181d83791ad433213d8c24efffda1eec85d741" + +[[package]] +name = "scopeguard" +version = "1.2.0" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "f91339c0467de62360649f8d3e185ca8de4224ff281f66000de5eb2a77a79041" +checksum = "94143f37725109f92c262ed2cf5e59bce7498c01bcc1502d7b9afe439a4e9f49" [[package]] name = "serde" -version = "1.0.164" +version = "1.0.173" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "9e8c8cf938e98f769bc164923b06dce91cea1751522f46f8466461af04c9027d" +checksum = "e91f70896d6720bc714a4a57d22fc91f1db634680e65c8efe13323f1fa38d53f" [[package]] name = "strsim" @@ -481,20 +555,9 @@ dependencies = [ [[package]] name = "syn" -version = "1.0.109" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "72b64191b275b66ffe2469e8af2c1cfe3bafa67b529ead792a6d0160888b4237" -dependencies = [ - "proc-macro2", - "quote", - "unicode-ident", -] - -[[package]] -name = "syn" -version = "2.0.22" +version = "2.0.26" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "2efbeae7acf4eabd6bcdcbd11c92f45231ddda7539edc7806bd1a04a03b24616" +checksum = "45c3457aacde3c65315de5031ec191ce46604304d2446e803d71ade03308d970" dependencies = [ "proc-macro2", "quote", @@ -503,9 +566,9 @@ dependencies = [ [[package]] name = "unicode-ident" -version = "1.0.9" +version = "1.0.11" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "b15811caf2415fb889178633e7724bad2509101cde276048e013b9def5e51fa0" +checksum = "301abaae475aa91687eb82514b328ab47a211a533026cb25fc3e519b86adfc3c" [[package]] name = "utf8parse" @@ -519,28 +582,6 @@ version = "0.11.0+wasi-snapshot-preview1" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "9c8d87e72b64a3b4db28d11ce29237c246188f4f51057d65a7eab63b7987e423" -[[package]] -name = "winapi" -version = "0.3.9" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "5c839a674fcd7a98952e593242ea400abe93992746761e38641405d28b00f419" -dependencies = [ - "winapi-i686-pc-windows-gnu", - "winapi-x86_64-pc-windows-gnu", -] - -[[package]] -name = "winapi-i686-pc-windows-gnu" -version = "0.4.0" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "ac3b87c63620426dd9b991e5ce0329eff545bccbbb34f3be09ff6fb6ab51b7b6" - -[[package]] -name = "winapi-x86_64-pc-windows-gnu" -version = "0.4.0" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "712e227841d057c1ee1cd2fb22fa7e5a5461ae8e48fa2ca79ec42cfc1931183f" - [[package]] name = "windows-sys" version = "0.48.0" @@ -552,9 +593,9 @@ dependencies = [ [[package]] name = "windows-targets" -version = "0.48.0" +version = "0.48.1" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "7b1eb6f0cd7c80c79759c929114ef071b87354ce476d9d94271031c0497adfd5" +checksum = "05d4b17490f70499f20b9e791dcf6a299785ce8af4d709018206dc5b4953e95f" dependencies = [ "windows_aarch64_gnullvm", "windows_aarch64_msvc", diff --git a/Cargo.toml b/Cargo.toml index ba6859a..14fc723 100644 --- a/Cargo.toml +++ b/Cargo.toml @@ -22,6 +22,7 @@ rustc-hash.workspace = true clap.workspace = true csv.workspace = true regex.workspace = true +rayon.workspace = true [dev-dependencies] glob.workspace = true @@ -38,4 +39,5 @@ csv = "1.2" regex = "1.7" glob = "0.3" pretty_assertions = "1.3" -anyhow = "1.0" \ No newline at end of file +anyhow = "1.0" +rayon = "1.7" diff --git a/src/bdd.rs b/src/bdd.rs index 08acc18..87ec512 100644 --- a/src/bdd.rs +++ b/src/bdd.rs @@ -333,9 +333,10 @@ impl BDDEnv { /// ite computes if a then b else c pub fn ite(&self, a: Rc>, b: Rc>, c: Rc>) -> Rc> { + let (left, right) = rayon::join(|| self.implies(Rc::clone(&a), Rc::clone(&b)), self.implies(self.not(Rc::clone(&a)), Rc::clone(&c))); + self.and( - self.implies(Rc::clone(&a), Rc::clone(&b)), - self.implies(self.not(Rc::clone(&a)), Rc::clone(&c)), + left, right ) } From d681d7968f746e5ca48b1ebcb2987eea760c2aca Mon Sep 17 00:00:00 2001 From: Tim Beurskens Date: Thu, 20 Jul 2023 17:35:55 +0200 Subject: [PATCH 3/4] temporary disable rayon --- Cargo.lock | 2 +- Cargo.toml | 2 +- src/bdd.rs | 5 ++--- 3 files changed, 4 insertions(+), 5 deletions(-) diff --git a/Cargo.lock b/Cargo.lock index 97ddafe..403e043 100644 --- a/Cargo.lock +++ b/Cargo.lock @@ -488,7 +488,7 @@ checksum = "e5ea92a5b6195c6ef2a0295ea818b312502c6fc94dde986c5553242e18fd4ce2" [[package]] name = "rsbdd" -version = "0.10.5" +version = "0.10.6" dependencies = [ "clap", "csv", diff --git a/Cargo.toml b/Cargo.toml index 14fc723..837213d 100644 --- a/Cargo.toml +++ b/Cargo.toml @@ -9,7 +9,7 @@ authors = ["Tim Beurskens "] [package] name = "rsbdd" description = "A BDD-based SAT solver" -version = "0.10.5" +version = "0.10.6" edition.workspace = true authors.workspace = true diff --git a/src/bdd.rs b/src/bdd.rs index 87ec512..08acc18 100644 --- a/src/bdd.rs +++ b/src/bdd.rs @@ -333,10 +333,9 @@ impl BDDEnv { /// ite computes if a then b else c pub fn ite(&self, a: Rc>, b: Rc>, c: Rc>) -> Rc> { - let (left, right) = rayon::join(|| self.implies(Rc::clone(&a), Rc::clone(&b)), self.implies(self.not(Rc::clone(&a)), Rc::clone(&c))); - self.and( - left, right + self.implies(Rc::clone(&a), Rc::clone(&b)), + self.implies(self.not(Rc::clone(&a)), Rc::clone(&c)), ) } From a305655773fa36c8b3a30035c4081d74daf7f2bd Mon Sep 17 00:00:00 2001 From: Tim Beurskens Date: Thu, 20 Jul 2023 19:19:30 +0200 Subject: [PATCH 4/4] add documentation --- src/bdd.rs | 69 ++++++++++++++++++++++++++++++++++-------------------- 1 file changed, 44 insertions(+), 25 deletions(-) diff --git a/src/bdd.rs b/src/bdd.rs index 08acc18..7d4076d 100644 --- a/src/bdd.rs +++ b/src/bdd.rs @@ -90,9 +90,23 @@ impl From> for BDD { } #[derive(Debug, Clone, Copy, PartialEq, Eq)] +/// Single variable assignment in a truth table. +/// +/// The variable assignments in a truth table can be one of True, False or Any. +/// [`True`] is assigned when the variable can only be assigned a 'true' value; +/// [`False`] is assigned when the variable can only be 'false'. +/// When the variable can either be true or false, the truth table can either consist of +/// both options (as separate models), or assign [`Any`]. +/// +/// [`Any`]: TruthTableEntry::Any +/// [`True`]: TruthTableEntry::True +/// [`False`]: TruthTableEntry::False pub enum TruthTableEntry { + /// Assigned when the variable can only be true True, + /// Assigned when the variable can only be false False, + /// Assigned when the variable can either be true or false Any, } @@ -160,6 +174,7 @@ impl Default for BDDEnv { } impl BDDEnv { + /// Compute the size of the BDD (number of nodes) pub fn size(&self) -> usize { self.nodes.borrow().len() } @@ -215,8 +230,10 @@ impl BDDEnv { } } - // make a new choice based on the given symbol and the left and right subtree. - // the new choice is then simplified and a reference is added to the lookup table + /// Make a new choice based on the given symbol and the left and right subtree. + /// The new choice is then simplified and a reference is added to the lookup table. + /// + /// This function is probably the main bottleneck for bdd computations (in its current implementation). pub fn mk_choice( &self, true_subtree: Rc>, @@ -239,7 +256,7 @@ impl BDDEnv { } } - // find the true or false node in the lookup table and return a reference to it + /// Find the true or false node in the lookup table and return a reference to it. pub fn mk_const(&self, v: bool) -> Rc> { if v { Rc::clone(self.nodes.borrow().get(&BDD::True).unwrap()) @@ -248,11 +265,12 @@ impl BDDEnv { } } - // find an equivalent subtree in the lookup table and return a reference to it + /// Find an equivalent subtree in the lookup table and return a reference to it pub fn find(&self, r: &Rc>) -> Rc> { Rc::clone(self.nodes.borrow().get(r.as_ref()).unwrap()) } + /// Create a new BDD graph pub fn new() -> Self { let mut nodes = FxHashMap::default(); @@ -264,7 +282,7 @@ impl BDDEnv { } } - // conjunction + /// Logic conjunction pub fn and(&self, a: Rc>, b: Rc>) -> Rc> { match (a.as_ref(), b.as_ref()) { (BDD::False, _) | (_, &BDD::False) => self.mk_const(false), @@ -289,7 +307,7 @@ impl BDDEnv { } } - // disjunction + /// Disjunction pub fn or(&self, a: Rc>, b: Rc>) -> Rc> { // self.not(self.nor(a, b)) @@ -317,6 +335,7 @@ impl BDDEnv { } } + /// Logic negation pub fn not(&self, a: Rc>) -> Rc> { match a.as_ref() { BDD::False => self.mk_const(true), @@ -327,6 +346,7 @@ impl BDDEnv { } } + /// Implication pub fn implies(&self, a: Rc>, b: Rc>) -> Rc> { self.or(self.not(a), b) } @@ -370,7 +390,6 @@ impl BDDEnv { self.mk_choice(self.mk_const(true), s, self.mk_const(false)) } - #[inline] fn cmp_count bool + Copy>( &self, branches: &[Rc>], @@ -415,16 +434,31 @@ impl BDDEnv { } fn count_leq_recursive(&self, a: &[Rc>], b: &[Rc>], n: i64) -> Rc> { + self.cmp_count_compare(a, b, n, Self::aln) + } + + fn count_geq_recursive(&self, a: &[Rc>], b: &[Rc>], n: i64) -> Rc> { + self.cmp_count_compare(a, b, n, Self::amn) + } + + #[inline] + fn cmp_count_compare>], i64) -> Rc> + Copy>( + &self, + a: &[Rc>], + b: &[Rc>], + n: i64, + cmp: CmpFn, + ) -> Rc> { if a.is_empty() { - self.aln(b, n) + cmp(self, b, n) } else { let first = &a[0]; let remainder = a[1..].to_vec(); self.ite( Rc::clone(first), - self.count_leq_recursive(&remainder, b, n + 1), - self.count_leq_recursive(&remainder, b, n), + self.cmp_count_compare(&remainder, b, n + 1, cmp), + self.cmp_count_compare(&remainder, b, n, cmp), ) } } @@ -437,21 +471,6 @@ impl BDDEnv { self.count_geq_recursive(a, b, 0) } - fn count_geq_recursive(&self, a: &[Rc>], b: &[Rc>], n: i64) -> Rc> { - if a.is_empty() { - self.amn(b, n) - } else { - let first = &a[0]; - let remainder = a[1..].to_vec(); - - self.ite( - Rc::clone(first), - self.count_geq_recursive(&remainder, b, n + 1), - self.count_geq_recursive(&remainder, b, n), - ) - } - } - pub fn count_eq(&self, a: &[Rc>], b: &[Rc>]) -> Rc> { self.and(self.count_leq(a, b), self.count_geq(a, b)) }