BDD is not reduced when running CLI

[lisaoakley]

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

[SHoltzen]

Update here -- I added a quickcheck test to test for BDD canonicity during compilation and confirmed that compiled BDDs are reduced, so this is likely a printing issue and not affecting core performance.