MVP for bottomup_cnf_to_bdd

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"

bin/bottomup_cnf_to_bdd.rs

@@ -0,0 +1,82 @@
+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.
+    /// allowed: `auto_minfill`, `auto_force`
+    #[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(),
+        "auto_force" => cnf.force_order(),
+        _ => panic!(
+            "Unknown order {} provided, expected one of: `auto_minfill`, `auto_force`",
+            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());
+}

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)]