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..ec7c5027 --- /dev/null +++ b/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::>::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)]