tulip-control / dd

Binary Decision Diagrams (BDDs) in pure Python and Cython wrappers of CUDD, Sylvan, and BuDDy
https://pypi.org/project/dd
Other
181 stars 39 forks source link

Question: Recursive function for MDDs #76

Closed glarange closed 3 years ago

glarange commented 3 years ago

Looking to do a recursive probability function similar to https://github.com/tulip-control/dd/issues/62 , but for MDDs. The intended workflow is attached below

Quant_MDD_Workflow.pdf

Question is: Is there a way to build an MDD equivalent to:

bdd = BDD()
bdd.declare('x', 'y', 'z', 'w')
u = bdd.add_expr('x /\ y')  

There doesn't seem to be an attribute mdd.add_expr -- I tried, unsuccessfully. But is there another way to build an MDD from an expression that isn't converting a BDD into an MDD?

johnyf commented 3 years ago

The methods dd.mdd.MDD.ite and dd.mdd.MDD.find_or_add can be used to build directly MDDs, without converting from a BDD. Currently, a method dd.mdd.MDD.add_expr is not implemented.

glarange commented 3 years ago

I'm familiar with case operator for MDDs and ite only for BDDs. But how does ite work for MDDs?

johnyf commented 3 years ago

Similarly to how ite works for BDDs.