From 5d387118631b98cc32df300f21b7d18b9ed0a258 Mon Sep 17 00:00:00 2001
From: Matthew Wang <matt@matthewwang.me>
Date: Sun, 23 Jul 2023 17:19:19 -0400
Subject: [PATCH 1/2] MVP for `bottomup_cnf_to_bdd`

To use:

```
cargo run --bin bottomup_cnf_to_bdd --features="cli" -- -f cnf/php-4-6.cnf -v > out.json
```

To-do:

- more orders (need to implement the force heuristic?)
- specify manual variable order
- more stats
- progress bar
---
 Cargo.toml                 | 13 ++++++-
 bin/bottomup_cnf_to_bdd.rs | 80 ++++++++++++++++++++++++++++++++++++++
 src/builder/bdd/robdd.rs   |  6 +++
 3 files changed, 98 insertions(+), 1 deletion(-)
 create mode 100644 bin/bottomup_cnf_to_bdd.rs

diff --git a/Cargo.toml b/Cargo.toml
index 1d918ac4..5f101a71 100644
--- a/Cargo.toml
+++ b/Cargo.toml
@@ -21,6 +21,9 @@ segment-tree = "2.0.0"
 bumpalo = "3.11.1"
 petgraph = "0.6.2"
 rand_chacha = "0.3.1"
+# optional: only used to build [[bin]]
+clap = { version = "4.2.1", features = ["derive"], optional = true }
+serde_json = { version = "1.0.81", optional = true }
 
 [target.'cfg(target_arch = "wasm32")'.dependencies]
 getrandom = { version = "0.2", features = ["js"] }
@@ -30,8 +33,8 @@ wasm-bindgen = { version = "0.2.84" }
 
 # example/test-only
 [dev-dependencies]
-clap = { version = "4.2.1", features = ["derive"] }
 serde_json = { version = "1.0.81" }
+clap = { version = "4.2.1", features = ["derive"] }
 
 [lib]
 name = "rsdd"
@@ -49,6 +52,14 @@ incremental = false
 codegen-units = 16
 rpath = false
 
+[features]
+cli = ["clap", "serde_json"]
+
+[[bin]]
+name = "bottomup_cnf_to_bdd"
+path = "bin/bottomup_cnf_to_bdd.rs"
+required-features = ["cli"]
+
 [[example]]
 name = "one_shot_benchmark"
 path = "examples/one_shot_benchmark.rs"
diff --git a/bin/bottomup_cnf_to_bdd.rs b/bin/bottomup_cnf_to_bdd.rs
new file mode 100644
index 00000000..ebf044f3
--- /dev/null
+++ b/bin/bottomup_cnf_to_bdd.rs
@@ -0,0 +1,80 @@
+use std::{fs, time::Instant};
+
+use clap::Parser;
+use rsdd::{
+    builder::{
+        bdd::{BddBuilder, RobddBuilder},
+        cache::LruIteTable,
+    },
+    plan::bdd_plan::BddPlan,
+    repr::{bdd::BddPtr, cnf::Cnf, dtree::DTree},
+    serialize::BDDSerializer,
+};
+
+#[derive(Parser, Debug)]
+#[clap(author, version, about, long_about = None)]
+struct Args {
+    /// input CNF in DIMACS form
+    #[clap(short, long, value_parser)]
+    file: String,
+
+    /// variable order for BDD.
+    /// defaults to `auto_minfill`, which uses a min-fill heuristic.
+    #[clap(long, value_parser, default_value_t = String::from("auto_minfill"))]
+    order: String,
+
+    /// compilation order (a tree describing sequence of clause-conjunctions).
+    /// defaults to `dtree`, a variable order-based decision tree decomposition
+    #[clap(long, value_parser, default_value_t = String::from("dtree"))]
+    strategy: String,
+
+    /// show verbose output (including timing information, cache profiling, etc.)
+    #[clap(short, long, value_parser)]
+    verbose: bool,
+}
+
+fn main() {
+    let args = Args::parse();
+
+    let file = fs::read_to_string(args.file).unwrap();
+
+    let cnf = Cnf::from_dimacs(&file);
+
+    let start = Instant::now();
+
+    let order = match args.order.as_str() {
+        "auto_minfill" => cnf.min_fill_order(),
+        _ => panic!(
+            "Unknown order {} provided, expected one of: `auto_minfill`",
+            args.order
+        ),
+    };
+
+    let plan = match args.strategy.as_str() {
+        "dtree" => {
+            let dtree = DTree::from_cnf(&cnf, &order);
+            BddPlan::from_dtree(&dtree)
+        }
+        _ => panic!(
+            "Unknown strategy {} provided, expected one of: `dtree`",
+            args.order
+        ),
+    };
+
+    let builder = RobddBuilder::<LruIteTable<BddPtr>>::new(order);
+    let bdd = builder.compile_plan(&plan);
+
+    let elapsed = start.elapsed();
+
+    if args.verbose {
+        eprintln!("=== STATS ===");
+
+        let stats = builder.stats();
+        eprintln!("compilation time: {:.4}s", elapsed.as_secs_f64());
+        eprintln!("recursive calls: {}", stats.num_recursive_calls);
+    }
+
+    let serialized = BDDSerializer::from_bdd(bdd);
+
+    println!("{}", serde_json::to_string(&serialized).unwrap());
+}
diff --git a/src/builder/bdd/robdd.rs b/src/builder/bdd/robdd.rs
index 7747b28b..a9582eaf 100644
--- a/src/builder/bdd/robdd.rs
+++ b/src/builder/bdd/robdd.rs
@@ -304,6 +304,12 @@ impl<'a, T: IteTable<'a, BddPtr<'a>> + Default> RobddBuilder<'a, T> {
         // TODO: this num_vars should be tied to the specific BDD, not the manager
         self.smooth_helper(bdd, 0, num_vars)
     }
+
+    pub fn stats(&'a self) -> BddBuilderStats {
+        BddBuilderStats {
+            num_recursive_calls: self.stats.borrow().num_recursive_calls,
+        }
+    }
 }
 
 #[cfg(test)]

From 88ba26bf0fd380fc7a8217305268c69741cfdf35 Mon Sep 17 00:00:00 2001
From: Matthew Wang <matt@matthewwang.me>
Date: Sun, 23 Jul 2023 17:25:25 -0400
Subject: [PATCH 2/2] Adds force heuristic option

---
 bin/bottomup_cnf_to_bdd.rs | 4 +++-
 1 file changed, 3 insertions(+), 1 deletion(-)

diff --git a/bin/bottomup_cnf_to_bdd.rs b/bin/bottomup_cnf_to_bdd.rs
index ebf044f3..ec7c5027 100644
--- a/bin/bottomup_cnf_to_bdd.rs
+++ b/bin/bottomup_cnf_to_bdd.rs
@@ -20,6 +20,7 @@ struct Args {
 
     /// variable order for BDD.
     /// defaults to `auto_minfill`, which uses a min-fill heuristic.
+    /// allowed: `auto_minfill`, `auto_force`
     #[clap(long, value_parser, default_value_t = String::from("auto_minfill"))]
     order: String,
 
@@ -44,8 +45,9 @@ fn main() {
 
     let order = match args.order.as_str() {
         "auto_minfill" => cnf.min_fill_order(),
+        "auto_force" => cnf.force_order(),
         _ => panic!(
-            "Unknown order {} provided, expected one of: `auto_minfill`",
+            "Unknown order {} provided, expected one of: `auto_minfill`, `auto_force`",
             args.order
         ),
     };