Bug:

RSDD CLI is generating a non-reduced BDD with duplicate leaves/redundant nodes. We suspect this is leading to a noticeable performance loss in runtime of programs using larger BDDs. It is unclear if this issue is in the CLI only, or if it is in the core RSDD code.

Repro Steps:

(1) Add print statement to weighted_model_count.rs code to get printed BDD output

Here is the change as a git diff to main branch at commit sha `39aadfb`:

diff --git a/bin/weighted_model_count.rs b/bin/weighted_model_count.rs
index e2359d4..a482696 100644
--- a/bin/weighted_model_count.rs
+++ b/bin/weighted_model_count.rs
@@ -155,6 +155,7 @@ fn single_wmc(
     let bdd = builder.smooth(bdd, num_vars);

     let res = bdd.unsmoothed_wmc(&params);
+ println!("{}", bdd.to_string_debug());

     let elapsed = start.elapsed();

(2) Run RSDD CLI

Command:

cargo run --release --bin weighted_model_count --features="cli" -- -f minimal_example.sexp -w minimal_example_weights.json

‌

minimal_example.sexp:

(And (Var T0) (Var T1))

‌

minimal_example_weights.json:

{"T0": { "low": 0.9, "high": 0.1}, "T1": { "low": 0.9, "high": 0.1}}

‌

Outputs:

Expected Output:

(0, (1, T, F))
unweighted model count: 1
weighted model count: 0.01

Actual Output:

(0, (1, T, F), (1, F, F))
unweighted model count: 1
weighted model count: 0.010000000000000002