From bf0918d72f583a33a963f055491ff613b9a31ea8 Mon Sep 17 00:00:00 2001
From: Carl Meyer <carl@astral.sh>
Date: Thu, 19 Dec 2024 11:13:28 -0800
Subject: [PATCH] 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 815788b948..971520ebbc 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 8471ba6220..339c1082d0 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 9ef9d4a6ac..c103c229d4 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;