BDD

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,17 @@ dependencies = [
  "windows-sys 0.52.0",
 ]
 
+[[package]]
+name = "hugealloc"
+version = "0.1.1"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "542733215a252c27c674e5d875a910d7de509cb74123d0bdbaa050f871ec84c2"
+dependencies = [
+ "allocator-api2",
+ "libc",
+ "sptr",
+]
+
 [[package]]
 name = "humantime"
 version = "2.1.0"
@@ -1444,6 +1497,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 +1630,12 @@ dependencies = [
  "redox_syscall 0.5.3",
 ]
 
+[[package]]
+name = "linear-hashtbl"
+version = "0.1.1"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "e252bb7e9b36739fb2482438638e862241d111c76fae3ebee272454477c63a4f"
+
 [[package]]
 name = "linked-hash-map"
 version = "0.5.6"
@@ -1589,6 +1654,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 +1774,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 +1933,153 @@ version = "0.1.1"
 source = "registry+https://github.com/rust-lang/crates.io-index"
 checksum = "b15813163c1d831bf4a13c3610c05c0d03b39feb07f7e09fa234dac9b15aaf39"
 
+[[package]]
+name = "oxidd"
+version = "0.9.0"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "22f7c2dbbc26b8d2e1ae861401a4bfa1d2e229e39da77ff8f0d64f2b4793e6da"
+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 = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "efcc7923864f2a2525e76e26a3645b65a82e29ac3d3118d6906bad0117eb704e"
+dependencies = [
+ "allocator-api2",
+ "document-features",
+ "hugealloc",
+ "oxidd-core",
+ "parking_lot",
+]
+
+[[package]]
+name = "oxidd-core"
+version = "0.9.0"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "b47e2c527b7aba7a7c789c7e5300df5a338002b33284c823fd08e1c661d176d6"
+dependencies = [
+ "nanorand",
+]
+
+[[package]]
+name = "oxidd-derive"
+version = "0.9.0"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "4ccd72606db214bdf9b3880a6dedb50990fafdac23a05b65f982b65ac22862ac"
+dependencies = [
+ "proc-macro-error",
+ "proc-macro2",
+ "quote",
+ "syn 2.0.90",
+]
+
+[[package]]
+name = "oxidd-dump"
+version = "0.4.0"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "84ef9fed6a604b8199c988efce9231de372b058cf9501d1b60fa53ed0ea1d43a"
+dependencies = [
+ "bitvec",
+ "document-features",
+ "is_sorted",
+ "memchr",
+ "oxidd-core",
+ "rustc-hash 1.1.0",
+]
+
+[[package]]
+name = "oxidd-manager-index"
+version = "0.9.0"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "dd41278c0cd6f0418f78e8ed5a3a062fa31449a929b3a0d03d4c1056af620cdc"
+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 = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "222b3b3c71f9c4a5f875c01fda840e25d40d4fa86a5f0636938c17f7adf6c068"
+dependencies = [
+ "flume",
+ "is_sorted",
+ "oxidd-core",
+ "rayon",
+ "smallvec",
+]
+
+[[package]]
+name = "oxidd-rules-bdd"
+version = "0.9.0"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "f8ab7d000b0fb53ddcc282296929f51b2a5215591f6c6aa134a9fca9f133f61b"
+dependencies = [
+ "bitvec",
+ "document-features",
+ "oxidd-core",
+ "oxidd-derive",
+ "oxidd-dump",
+]
+
+[[package]]
+name = "oxidd-rules-mtbdd"
+version = "0.4.0"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "f9bd51a1a297d98cefd4843cf065aba5cb04b2e78b0623857f0f8babe9f3d421"
+dependencies = [
+ "document-features",
+ "oxidd-core",
+ "oxidd-derive",
+ "oxidd-dump",
+]
+
+[[package]]
+name = "oxidd-rules-tdd"
+version = "0.4.0"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "753f378e1d76f1f23afd1a06bbe4f23025ac95d19fb3c2b3ff052c0d3fcd9af3"
+dependencies = [
+ "document-features",
+ "oxidd-core",
+ "oxidd-derive",
+ "oxidd-dump",
+]
+
+[[package]]
+name = "oxidd-rules-zbdd"
+version = "0.9.0"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "821482c23511e87b1a9bd7f0454971f4a73b01a7ed16611179d79c5872690dce"
+dependencies = [
+ "bitvec",
+ "document-features",
+ "oxidd-core",
+ "oxidd-derive",
+ "oxidd-dump",
+]
+
 [[package]]
 name = "parking_lot"
 version = "0.12.3"
@@ -2127,6 +2351,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 +2450,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 +2518,9 @@ dependencies = [
  "crossbeam",
  "ctrlc",
  "filetime",
+ "oxidd",
+ "oxidd-core",
+ "oxidd-dump",
  "rayon",
  "red_knot_python_semantic",
  "red_knot_server",
@@ -3443,6 +3699,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 +3803,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 +4745,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"

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 = { version = "0.9.0", features = ["tdd"] }
 path-absolutize = { version = "3.1.1" }
 path-slash = { version = "0.2.1" }
 pathdiff = { version = "0.2.1" }

crates/red_knot/Cargo.toml

@@ -24,6 +24,9 @@ colored = { workspace = true }
 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"] }

crates/red_knot/src/main.rs

@@ -105,8 +105,44 @@ pub enum Command {
     Server,
 }
 
+use oxidd::bdd::BDDFunction;
+use oxidd::ManagerRef;
+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::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(),
+        )
+    });
+    mgr.with_manager_shared(|manager| {
+        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("bdd.dot").expect("could not create `bdd.dot`");
+        dump_all(
+            file,
+            manager,
+            [(&x, "x"), (&y, "y"), (&z, "z")],
+            [(&func, "z ^ (x ∨ (y ∧ ~x) ∨ (~y ∧ ~x))")],
+        )
+        .expect("dot export failed");
+    });
+    panic!("FOO");
     run().unwrap_or_else(|error| {
         use std::io::Write;