From 54561192dd9b12e1e41d288deda14310f97be5d9 Mon Sep 17 00:00:00 2001 From: Carl Meyer Date: Tue, 17 Dec 2024 17:19:48 -0800 Subject: [PATCH 1/4] testing it out --- Cargo.lock | 265 ++++++++++++++++++++++++++++++++++++ Cargo.toml | 1 + crates/red_knot/Cargo.toml | 1 + crates/red_knot/src/main.rs | 17 +++ 4 files changed, 284 insertions(+) diff --git a/Cargo.lock b/Cargo.lock index 3f5155adf74e4..2d4208c191998 100644 --- a/Cargo.lock +++ b/Cargo.lock @@ -30,6 +30,12 @@ dependencies = [ "memchr", ] +[[package]] +name = "allocator-api2" +version = "0.2.21" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "683d7910e743518b0e34f1186f92494becacb047c7b6bf616c96772180fef923" + [[package]] name = "android-tzdata" version = "0.1.1" @@ -203,6 +209,18 @@ version = "2.6.0" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "b048fb63fd8b5923fc5aa7b340d8e156aec7ec02f0c78fa8a6ddc2613f6f71de" +[[package]] +name = "bitvec" +version = "1.0.1" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "1bc2832c24239b0141d5674bb9174f9d68a8b5b3f2753311927c172ca46f7e9c" +dependencies = [ + "funty", + "radium", + "tap", + "wyz", +] + [[package]] name = "block-buffer" version = "0.10.4" @@ -835,6 +853,15 @@ version = "0.3.3" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "fea41bba32d969b513997752735605054bc0dfa92b4c56bf1189f2e174be7a10" +[[package]] +name = "document-features" +version = "0.2.10" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "cb6969eaabd2421f8a2775cfd2471a2b634372b4a25d41e3bd647b79912850a0" +dependencies = [ + "litrs", +] + [[package]] name = "drop_bomb" version = "0.1.5" @@ -952,6 +979,15 @@ dependencies = [ "miniz_oxide", ] +[[package]] +name = "flume" +version = "0.11.1" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "da0e4dd2a88388a1f4ccc7c9ce104604dab68d9f408dc34cd45823d5a9069095" +dependencies = [ + "spin", +] + [[package]] name = "fnv" version = "1.0.7" @@ -985,6 +1021,12 @@ dependencies = [ "libc", ] +[[package]] +name = "funty" +version = "2.0.0" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "e6d5a32815ae3f33302d95fdcb2ce17862f8c65363dcfd29360480ba1001fc9c" + [[package]] name = "generic-array" version = "0.14.7" @@ -1102,6 +1144,16 @@ dependencies = [ "windows-sys 0.52.0", ] +[[package]] +name = "hugealloc" +version = "0.1.1" +source = "git+https://github.com/OxiDD/oxidd.git?rev=7905546ccfdac6b26d3f3c7aa7768b0289cd27bc#7905546ccfdac6b26d3f3c7aa7768b0289cd27bc" +dependencies = [ + "allocator-api2", + "libc", + "sptr", +] + [[package]] name = "humantime" version = "2.1.0" @@ -1444,6 +1496,12 @@ dependencies = [ "once_cell", ] +[[package]] +name = "is_sorted" +version = "0.1.1" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "357376465c37db3372ef6a00585d336ed3d0f11d4345eef77ebcb05865392b21" + [[package]] name = "itertools" version = "0.10.5" @@ -1571,6 +1629,11 @@ dependencies = [ "redox_syscall 0.5.3", ] +[[package]] +name = "linear-hashtbl" +version = "0.1.1" +source = "git+https://github.com/OxiDD/oxidd.git?rev=7905546ccfdac6b26d3f3c7aa7768b0289cd27bc#7905546ccfdac6b26d3f3c7aa7768b0289cd27bc" + [[package]] name = "linked-hash-map" version = "0.5.6" @@ -1589,6 +1652,12 @@ version = "0.7.3" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "643cb0b8d4fcc284004d5fd0d67ccf61dfffadb7f75e1e71bc420f4688a3a704" +[[package]] +name = "litrs" +version = "0.4.1" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "b4ce301924b7887e9d637144fdade93f9dfff9b60981d4ac161db09720d39aa5" + [[package]] name = "lock_api" version = "0.4.11" @@ -1703,6 +1772,12 @@ dependencies = [ "windows-sys 0.52.0", ] +[[package]] +name = "nanorand" +version = "0.7.0" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "6a51313c5820b0b02bd422f4b44776fbf47961755c74ce64afc73bfad10226c3" + [[package]] name = "natord" version = "1.0.9" @@ -1856,6 +1931,142 @@ version = "0.1.1" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "b15813163c1d831bf4a13c3610c05c0d03b39feb07f7e09fa234dac9b15aaf39" +[[package]] +name = "oxidd" +version = "0.9.0" +source = "git+https://github.com/OxiDD/oxidd.git?rev=7905546ccfdac6b26d3f3c7aa7768b0289cd27bc#7905546ccfdac6b26d3f3c7aa7768b0289cd27bc" +dependencies = [ + "cfg-if", + "document-features", + "oxidd-cache", + "oxidd-core", + "oxidd-derive", + "oxidd-dump", + "oxidd-manager-index", + "oxidd-reorder", + "oxidd-rules-bdd", + "oxidd-rules-mtbdd", + "oxidd-rules-tdd", + "oxidd-rules-zbdd", + "rustc-hash 1.1.0", +] + +[[package]] +name = "oxidd-cache" +version = "0.9.0" +source = "git+https://github.com/OxiDD/oxidd.git?rev=7905546ccfdac6b26d3f3c7aa7768b0289cd27bc#7905546ccfdac6b26d3f3c7aa7768b0289cd27bc" +dependencies = [ + "allocator-api2", + "document-features", + "hugealloc", + "oxidd-core", + "parking_lot", +] + +[[package]] +name = "oxidd-core" +version = "0.9.0" +source = "git+https://github.com/OxiDD/oxidd.git?rev=7905546ccfdac6b26d3f3c7aa7768b0289cd27bc#7905546ccfdac6b26d3f3c7aa7768b0289cd27bc" +dependencies = [ + "nanorand", +] + +[[package]] +name = "oxidd-derive" +version = "0.9.0" +source = "git+https://github.com/OxiDD/oxidd.git?rev=7905546ccfdac6b26d3f3c7aa7768b0289cd27bc#7905546ccfdac6b26d3f3c7aa7768b0289cd27bc" +dependencies = [ + "proc-macro-error", + "proc-macro2", + "quote", + "syn 2.0.90", +] + +[[package]] +name = "oxidd-dump" +version = "0.4.0" +source = "git+https://github.com/OxiDD/oxidd.git?rev=7905546ccfdac6b26d3f3c7aa7768b0289cd27bc#7905546ccfdac6b26d3f3c7aa7768b0289cd27bc" +dependencies = [ + "bitvec", + "document-features", + "is_sorted", + "memchr", + "oxidd-core", + "rustc-hash 1.1.0", +] + +[[package]] +name = "oxidd-manager-index" +version = "0.9.0" +source = "git+https://github.com/OxiDD/oxidd.git?rev=7905546ccfdac6b26d3f3c7aa7768b0289cd27bc#7905546ccfdac6b26d3f3c7aa7768b0289cd27bc" +dependencies = [ + "bitvec", + "crossbeam-utils", + "linear-hashtbl", + "oxidd-core", + "parking_lot", + "rayon", + "rustc-hash 1.1.0", +] + +[[package]] +name = "oxidd-reorder" +version = "0.4.0" +source = "git+https://github.com/OxiDD/oxidd.git?rev=7905546ccfdac6b26d3f3c7aa7768b0289cd27bc#7905546ccfdac6b26d3f3c7aa7768b0289cd27bc" +dependencies = [ + "flume", + "is_sorted", + "oxidd-core", + "rayon", + "smallvec", +] + +[[package]] +name = "oxidd-rules-bdd" +version = "0.9.0" +source = "git+https://github.com/OxiDD/oxidd.git?rev=7905546ccfdac6b26d3f3c7aa7768b0289cd27bc#7905546ccfdac6b26d3f3c7aa7768b0289cd27bc" +dependencies = [ + "bitvec", + "document-features", + "oxidd-core", + "oxidd-derive", + "oxidd-dump", +] + +[[package]] +name = "oxidd-rules-mtbdd" +version = "0.4.0" +source = "git+https://github.com/OxiDD/oxidd.git?rev=7905546ccfdac6b26d3f3c7aa7768b0289cd27bc#7905546ccfdac6b26d3f3c7aa7768b0289cd27bc" +dependencies = [ + "document-features", + "oxidd-core", + "oxidd-derive", + "oxidd-dump", +] + +[[package]] +name = "oxidd-rules-tdd" +version = "0.4.0" +source = "git+https://github.com/OxiDD/oxidd.git?rev=7905546ccfdac6b26d3f3c7aa7768b0289cd27bc#7905546ccfdac6b26d3f3c7aa7768b0289cd27bc" +dependencies = [ + "document-features", + "oxidd-core", + "oxidd-derive", + "oxidd-dump", +] + +[[package]] +name = "oxidd-rules-zbdd" +version = "0.9.0" +source = "git+https://github.com/OxiDD/oxidd.git?rev=7905546ccfdac6b26d3f3c7aa7768b0289cd27bc#7905546ccfdac6b26d3f3c7aa7768b0289cd27bc" +dependencies = [ + "bitvec", + "document-features", + "oxidd-core", + "oxidd-derive", + "oxidd-dump", +] + [[package]] name = "parking_lot" version = "0.12.3" @@ -2127,6 +2338,29 @@ 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", + "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.92" @@ -2203,6 +2437,12 @@ dependencies = [ "proc-macro2", ] +[[package]] +name = "radium" +version = "0.7.0" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "dc33ff2d4973d518d823d61aa239014831e521c75da58e3df4840d3f47749d09" + [[package]] name = "rand" version = "0.8.5" @@ -2265,6 +2505,7 @@ dependencies = [ "crossbeam", "ctrlc", "filetime", + "oxidd", "rayon", "red_knot_python_semantic", "red_knot_server", @@ -3443,6 +3684,15 @@ name = "spin" version = "0.9.8" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "6980e8d7511241f8acf4aebddbb1ff938df5eebe98691418c4468d0b72a96a67" +dependencies = [ + "lock_api", +] + +[[package]] +name = "sptr" +version = "0.3.2" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "3b9b39299b249ad65f3b7e96443bad61c02ca5cd3589f46cb6d610a0fd6c0d6a" [[package]] name = "stable_deref_trait" @@ -3538,6 +3788,12 @@ dependencies = [ "syn 2.0.90", ] +[[package]] +name = "tap" +version = "1.0.1" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "55937e1799185b12863d447f42597ed69d9928686b8d88a1df17376a097d8369" + [[package]] name = "tempfile" version = "3.14.0" @@ -4474,6 +4730,15 @@ version = "0.5.5" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "1e9df38ee2d2c3c5948ea468a8406ff0db0b29ae1ffde1bcf20ef305bcc95c51" +[[package]] +name = "wyz" +version = "0.5.1" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "05f360fc0b24296329c78fda852a1e9ae82de9cf7b27dae4b7f62f118f77b9ed" +dependencies = [ + "tap", +] + [[package]] name = "yansi" version = "1.0.1" diff --git a/Cargo.toml b/Cargo.toml index 7dd38b1f5a1ca..34254f3f07f4b 100644 --- a/Cargo.toml +++ b/Cargo.toml @@ -105,6 +105,7 @@ mimalloc = { version = "0.1.39" } natord = { version = "1.0.9" } notify = { version = "7.0.0" } ordermap = { version = "0.5.0" } +oxidd = { git = "https://github.com/OxiDD/oxidd.git", rev = "7905546ccfdac6b26d3f3c7aa7768b0289cd27bc", features = ["tdd"] } path-absolutize = { version = "3.1.1" } path-slash = { version = "0.2.1" } pathdiff = { version = "0.2.1" } diff --git a/crates/red_knot/Cargo.toml b/crates/red_knot/Cargo.toml index 07715be94ecb1..8471ba62201f4 100644 --- a/crates/red_knot/Cargo.toml +++ b/crates/red_knot/Cargo.toml @@ -24,6 +24,7 @@ colored = { workspace = true } countme = { workspace = true, features = ["enable"] } crossbeam = { workspace = true } ctrlc = { version = "3.4.4" } +oxidd = { workspace = true } rayon = { workspace = true } salsa = { workspace = true } tracing = { workspace = true, features = ["release_max_level_debug"] } diff --git a/crates/red_knot/src/main.rs b/crates/red_knot/src/main.rs index 49730267b29c9..a28603561c027 100644 --- a/crates/red_knot/src/main.rs +++ b/crates/red_knot/src/main.rs @@ -105,8 +105,25 @@ pub enum Command { Server, } +use oxidd::bdd::BDDFunction; +use oxidd::tdd::TDDFunction; +use oxidd::BooleanFunction; +use oxidd::ManagerRef; +use oxidd::TVLFunction; + #[allow(clippy::print_stdout, clippy::unnecessary_wraps, clippy::print_stderr)] pub fn main() -> ExitStatus { + let mgr = oxidd::bdd::new_manager(24, 24, 1); + let (x, y, z) = mgr.with_manager_exclusive(|mgr| { + ( + BDDFunction::new_var(mgr).unwrap(), + BDDFunction::new_var(mgr).unwrap(), + BDDFunction::new_var(mgr).unwrap(), + ) + }); + let res = x.and(&y).unwrap().or(&z).unwrap(); + dbg!(res.eval([(&x, false), (&y, true), (&z, false)])); + panic!("FOO"); run().unwrap_or_else(|error| { use std::io::Write; From 6870d2c53ec7c24f5130f1f42a79c0cdfbe6a052 Mon Sep 17 00:00:00 2001 From: Carl Meyer Date: Wed, 18 Dec 2024 09:05:47 -0800 Subject: [PATCH 2/4] use published version of crate --- Cargo.lock | 39 ++++++++++++++++++++++++------------- Cargo.toml | 2 +- crates/red_knot/src/main.rs | 8 ++++---- 3 files changed, 31 insertions(+), 18 deletions(-) diff --git a/Cargo.lock b/Cargo.lock index 2d4208c191998..815788b94832a 100644 --- a/Cargo.lock +++ b/Cargo.lock @@ -1147,7 +1147,8 @@ dependencies = [ [[package]] name = "hugealloc" version = "0.1.1" -source = "git+https://github.com/OxiDD/oxidd.git?rev=7905546ccfdac6b26d3f3c7aa7768b0289cd27bc#7905546ccfdac6b26d3f3c7aa7768b0289cd27bc" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "542733215a252c27c674e5d875a910d7de509cb74123d0bdbaa050f871ec84c2" dependencies = [ "allocator-api2", "libc", @@ -1632,7 +1633,8 @@ dependencies = [ [[package]] name = "linear-hashtbl" version = "0.1.1" -source = "git+https://github.com/OxiDD/oxidd.git?rev=7905546ccfdac6b26d3f3c7aa7768b0289cd27bc#7905546ccfdac6b26d3f3c7aa7768b0289cd27bc" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "e252bb7e9b36739fb2482438638e862241d111c76fae3ebee272454477c63a4f" [[package]] name = "linked-hash-map" @@ -1934,7 +1936,8 @@ checksum = "b15813163c1d831bf4a13c3610c05c0d03b39feb07f7e09fa234dac9b15aaf39" [[package]] name = "oxidd" version = "0.9.0" -source = "git+https://github.com/OxiDD/oxidd.git?rev=7905546ccfdac6b26d3f3c7aa7768b0289cd27bc#7905546ccfdac6b26d3f3c7aa7768b0289cd27bc" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "22f7c2dbbc26b8d2e1ae861401a4bfa1d2e229e39da77ff8f0d64f2b4793e6da" dependencies = [ "cfg-if", "document-features", @@ -1954,7 +1957,8 @@ dependencies = [ [[package]] name = "oxidd-cache" version = "0.9.0" -source = "git+https://github.com/OxiDD/oxidd.git?rev=7905546ccfdac6b26d3f3c7aa7768b0289cd27bc#7905546ccfdac6b26d3f3c7aa7768b0289cd27bc" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "efcc7923864f2a2525e76e26a3645b65a82e29ac3d3118d6906bad0117eb704e" dependencies = [ "allocator-api2", "document-features", @@ -1966,7 +1970,8 @@ dependencies = [ [[package]] name = "oxidd-core" version = "0.9.0" -source = "git+https://github.com/OxiDD/oxidd.git?rev=7905546ccfdac6b26d3f3c7aa7768b0289cd27bc#7905546ccfdac6b26d3f3c7aa7768b0289cd27bc" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "b47e2c527b7aba7a7c789c7e5300df5a338002b33284c823fd08e1c661d176d6" dependencies = [ "nanorand", ] @@ -1974,7 +1979,8 @@ dependencies = [ [[package]] name = "oxidd-derive" version = "0.9.0" -source = "git+https://github.com/OxiDD/oxidd.git?rev=7905546ccfdac6b26d3f3c7aa7768b0289cd27bc#7905546ccfdac6b26d3f3c7aa7768b0289cd27bc" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "4ccd72606db214bdf9b3880a6dedb50990fafdac23a05b65f982b65ac22862ac" dependencies = [ "proc-macro-error", "proc-macro2", @@ -1985,7 +1991,8 @@ dependencies = [ [[package]] name = "oxidd-dump" version = "0.4.0" -source = "git+https://github.com/OxiDD/oxidd.git?rev=7905546ccfdac6b26d3f3c7aa7768b0289cd27bc#7905546ccfdac6b26d3f3c7aa7768b0289cd27bc" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "84ef9fed6a604b8199c988efce9231de372b058cf9501d1b60fa53ed0ea1d43a" dependencies = [ "bitvec", "document-features", @@ -1998,7 +2005,8 @@ dependencies = [ [[package]] name = "oxidd-manager-index" version = "0.9.0" -source = "git+https://github.com/OxiDD/oxidd.git?rev=7905546ccfdac6b26d3f3c7aa7768b0289cd27bc#7905546ccfdac6b26d3f3c7aa7768b0289cd27bc" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "dd41278c0cd6f0418f78e8ed5a3a062fa31449a929b3a0d03d4c1056af620cdc" dependencies = [ "bitvec", "crossbeam-utils", @@ -2012,7 +2020,8 @@ dependencies = [ [[package]] name = "oxidd-reorder" version = "0.4.0" -source = "git+https://github.com/OxiDD/oxidd.git?rev=7905546ccfdac6b26d3f3c7aa7768b0289cd27bc#7905546ccfdac6b26d3f3c7aa7768b0289cd27bc" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "222b3b3c71f9c4a5f875c01fda840e25d40d4fa86a5f0636938c17f7adf6c068" dependencies = [ "flume", "is_sorted", @@ -2024,7 +2033,8 @@ dependencies = [ [[package]] name = "oxidd-rules-bdd" version = "0.9.0" -source = "git+https://github.com/OxiDD/oxidd.git?rev=7905546ccfdac6b26d3f3c7aa7768b0289cd27bc#7905546ccfdac6b26d3f3c7aa7768b0289cd27bc" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "f8ab7d000b0fb53ddcc282296929f51b2a5215591f6c6aa134a9fca9f133f61b" dependencies = [ "bitvec", "document-features", @@ -2036,7 +2046,8 @@ dependencies = [ [[package]] name = "oxidd-rules-mtbdd" version = "0.4.0" -source = "git+https://github.com/OxiDD/oxidd.git?rev=7905546ccfdac6b26d3f3c7aa7768b0289cd27bc#7905546ccfdac6b26d3f3c7aa7768b0289cd27bc" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "f9bd51a1a297d98cefd4843cf065aba5cb04b2e78b0623857f0f8babe9f3d421" dependencies = [ "document-features", "oxidd-core", @@ -2047,7 +2058,8 @@ dependencies = [ [[package]] name = "oxidd-rules-tdd" version = "0.4.0" -source = "git+https://github.com/OxiDD/oxidd.git?rev=7905546ccfdac6b26d3f3c7aa7768b0289cd27bc#7905546ccfdac6b26d3f3c7aa7768b0289cd27bc" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "753f378e1d76f1f23afd1a06bbe4f23025ac95d19fb3c2b3ff052c0d3fcd9af3" dependencies = [ "document-features", "oxidd-core", @@ -2058,7 +2070,8 @@ dependencies = [ [[package]] name = "oxidd-rules-zbdd" version = "0.9.0" -source = "git+https://github.com/OxiDD/oxidd.git?rev=7905546ccfdac6b26d3f3c7aa7768b0289cd27bc#7905546ccfdac6b26d3f3c7aa7768b0289cd27bc" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "821482c23511e87b1a9bd7f0454971f4a73b01a7ed16611179d79c5872690dce" dependencies = [ "bitvec", "document-features", diff --git a/Cargo.toml b/Cargo.toml index 34254f3f07f4b..8e20ac4d2f223 100644 --- a/Cargo.toml +++ b/Cargo.toml @@ -105,7 +105,7 @@ mimalloc = { version = "0.1.39" } natord = { version = "1.0.9" } notify = { version = "7.0.0" } ordermap = { version = "0.5.0" } -oxidd = { git = "https://github.com/OxiDD/oxidd.git", rev = "7905546ccfdac6b26d3f3c7aa7768b0289cd27bc", features = ["tdd"] } +oxidd = { version = "0.9.0", features = ["tdd"] } path-absolutize = { version = "3.1.1" } path-slash = { version = "0.2.1" } pathdiff = { version = "0.2.1" } diff --git a/crates/red_knot/src/main.rs b/crates/red_knot/src/main.rs index a28603561c027..9ef9d4a6acdd9 100644 --- a/crates/red_knot/src/main.rs +++ b/crates/red_knot/src/main.rs @@ -113,12 +113,12 @@ use oxidd::TVLFunction; #[allow(clippy::print_stdout, clippy::unnecessary_wraps, clippy::print_stderr)] pub fn main() -> ExitStatus { - let mgr = oxidd::bdd::new_manager(24, 24, 1); + let mgr = oxidd::tdd::new_manager(24, 24, 1); let (x, y, z) = mgr.with_manager_exclusive(|mgr| { ( - BDDFunction::new_var(mgr).unwrap(), - BDDFunction::new_var(mgr).unwrap(), - BDDFunction::new_var(mgr).unwrap(), + TDDFunction::new_var(mgr).unwrap(), + TDDFunction::new_var(mgr).unwrap(), + TDDFunction::new_var(mgr).unwrap(), ) }); let res = x.and(&y).unwrap().or(&z).unwrap(); From bf0918d72f583a33a963f055491ff613b9a31ea8 Mon Sep 17 00:00:00 2001 From: Carl Meyer Date: Thu, 19 Dec 2024 11:13:28 -0800 Subject: [PATCH 3/4] dot file --- Cargo.lock | 2 ++ crates/red_knot/Cargo.toml | 2 ++ crates/red_knot/src/main.rs | 27 +++++++++++++++++++++------ 3 files changed, 25 insertions(+), 6 deletions(-) diff --git a/Cargo.lock b/Cargo.lock index 815788b94832a..971520ebbc62b 100644 --- a/Cargo.lock +++ b/Cargo.lock @@ -2519,6 +2519,8 @@ dependencies = [ "ctrlc", "filetime", "oxidd", + "oxidd-core", + "oxidd-dump", "rayon", "red_knot_python_semantic", "red_knot_server", diff --git a/crates/red_knot/Cargo.toml b/crates/red_knot/Cargo.toml index 8471ba62201f4..339c1082d070f 100644 --- a/crates/red_knot/Cargo.toml +++ b/crates/red_knot/Cargo.toml @@ -25,6 +25,8 @@ countme = { workspace = true, features = ["enable"] } crossbeam = { workspace = true } ctrlc = { version = "3.4.4" } oxidd = { workspace = true } +oxidd-core = { version = "0.9.0" } +oxidd-dump = { version = "0.4.0" } rayon = { workspace = true } salsa = { workspace = true } tracing = { workspace = true, features = ["release_max_level_debug"] } diff --git a/crates/red_knot/src/main.rs b/crates/red_knot/src/main.rs index 9ef9d4a6acdd9..c103c229d4b5b 100644 --- a/crates/red_knot/src/main.rs +++ b/crates/red_knot/src/main.rs @@ -105,24 +105,39 @@ pub enum Command { Server, } -use oxidd::bdd::BDDFunction; use oxidd::tdd::TDDFunction; -use oxidd::BooleanFunction; use oxidd::ManagerRef; use oxidd::TVLFunction; +use oxidd_core::Manager; +use oxidd_dump::dot::dump_all; #[allow(clippy::print_stdout, clippy::unnecessary_wraps, clippy::print_stderr)] pub fn main() -> ExitStatus { let mgr = oxidd::tdd::new_manager(24, 24, 1); - let (x, y, z) = mgr.with_manager_exclusive(|mgr| { + let (x, y) = mgr.with_manager_exclusive(|mgr| { ( TDDFunction::new_var(mgr).unwrap(), TDDFunction::new_var(mgr).unwrap(), - TDDFunction::new_var(mgr).unwrap(), ) }); - let res = x.and(&y).unwrap().or(&z).unwrap(); - dbg!(res.eval([(&x, false), (&y, true), (&z, false)])); + mgr.with_manager_shared(|manager| { + let res = x + .or(&y.and(&x.not().unwrap()).unwrap()) + .unwrap() + .or(&y.not().unwrap().and(&x.not().unwrap()).unwrap()) + .unwrap(); + + manager.gc(); + + let file = std::fs::File::create("tdd.dot").expect("could not create `tdd.dot`"); + dump_all( + file, + manager, + [(&x, "x"), (&y, "y")], + [(&res, "x ∨ (y ∧ ~x) ∨ (~y ∧ ~x)")], + ) + .expect("dot export failed"); + }); panic!("FOO"); run().unwrap_or_else(|error| { use std::io::Write; From d91bb060f1de379bb1fc756df61b48184db41fff Mon Sep 17 00:00:00 2001 From: Carl Meyer Date: Fri, 20 Dec 2024 09:00:43 -0800 Subject: [PATCH 4/4] BDD --- crates/red_knot/src/main.rs | 24 ++++++++++++++---------- 1 file changed, 14 insertions(+), 10 deletions(-) diff --git a/crates/red_knot/src/main.rs b/crates/red_knot/src/main.rs index c103c229d4b5b..94d95839fdd15 100644 --- a/crates/red_knot/src/main.rs +++ b/crates/red_knot/src/main.rs @@ -105,36 +105,40 @@ pub enum Command { Server, } -use oxidd::tdd::TDDFunction; +use oxidd::bdd::BDDFunction; use oxidd::ManagerRef; -use oxidd::TVLFunction; +use oxidd::{BooleanFunction, BooleanFunctionQuant}; use oxidd_core::Manager; use oxidd_dump::dot::dump_all; #[allow(clippy::print_stdout, clippy::unnecessary_wraps, clippy::print_stderr)] pub fn main() -> ExitStatus { - let mgr = oxidd::tdd::new_manager(24, 24, 1); - let (x, y) = mgr.with_manager_exclusive(|mgr| { + let mgr = oxidd::bdd::new_manager(24, 24, 1); + let (x, y, z) = mgr.with_manager_exclusive(|mgr| { ( - TDDFunction::new_var(mgr).unwrap(), - TDDFunction::new_var(mgr).unwrap(), + BDDFunction::new_var(mgr).unwrap(), + BDDFunction::new_var(mgr).unwrap(), + BDDFunction::new_var(mgr).unwrap(), ) }); mgr.with_manager_shared(|manager| { - let res = x + let inner_func = x .or(&y.and(&x.not().unwrap()).unwrap()) .unwrap() .or(&y.not().unwrap().and(&x.not().unwrap()).unwrap()) .unwrap(); + let func = z.and(&inner_func).unwrap(); + + let func = func.restrict(&z).unwrap(); manager.gc(); - let file = std::fs::File::create("tdd.dot").expect("could not create `tdd.dot`"); + let file = std::fs::File::create("bdd.dot").expect("could not create `bdd.dot`"); dump_all( file, manager, - [(&x, "x"), (&y, "y")], - [(&res, "x ∨ (y ∧ ~x) ∨ (~y ∧ ~x)")], + [(&x, "x"), (&y, "y"), (&z, "z")], + [(&func, "z ^ (x ∨ (y ∧ ~x) ∨ (~y ∧ ~x))")], ) .expect("dot export failed"); });