Implement `BddDfa`

**Is your feature request related to a problem? Please describe.**

`SymbolicDFA` is actually explicit in the state space and symbolic in the transition guards.

**Describe the solution you'd like**

Implement a fully symbolic version of the DFA, where all the components are represented symbolically.

**Describe alternatives you've considered**
n/a

**Additional context**
n/a
