Question about BDD

[jumormt]

Hi,

Assuming that c1 and c2 are both bool const. eq(c1 && c2, c2 && c1) returns false even though they are actually equivalent formula. Is there a way to have a unique id for each boolean formula? Checking equivalence with z3 solver is time-consuming.

I found a BDD implementation in this repository bdd.cpp. Is it a possible solution?

Thanks in advance.
Regards

[NikolajBjorner]

z3 does not expose canonicalization (using bdds). BDDs are used internally and not exposed.
Even the BDD package might never be exercised, but variants with weighted mult-terminal ZDDs are used a lot.
There are BDD packages already that can be used, such as CUDD and BuDDy and newer onces.