A | |
| Asssub [Domain0.O] | |
B | |
| Benum [Expr1.O] | |
| Benum [Expr1] | |
| Benum [Expr0.O] | |
| Benum [Expr0] | |
| Bint [Expr1.O] | |
| Bint [Expr1] | |
| Bint [Expr0.O] | |
| Bint [Expr0] | |
| Bool [Expr1.O] | |
| Bool [Expr1] | |
| Bool [Expr0.O] | |
| Bool [Expr0] | |
C | |
| Cond |
Normalized condition environments (base module)
|
D | |
| Domain0 |
Boolean (abstract) domain
|
| Domain1 |
Boolean (abstract) domain with integrated environment
|
E | |
| Enum |
Enumerated expressions with BDDs
|
| Env |
Normalized managers/environments
|
| Expr [Expr0.O] | |
| Expr0 |
Finite-type expressions with BDDs
|
| Expr1 |
Finite-type expressions linked to normalized environments
|
I | |
| Int |
Bounded integer expressions with BDDs
|
L | |
| List [Expr1.O] | |
| List [Expr1] | |
M | |
| Minterm [Enum] | |
| Minterm [Int] | |
| Minterm [Reg] | |
O | |
| O [Domain1] | |
| O [Domain0] | |
| O [Expr1] | |
| O [Expr0] | |
| O [Env] |
Opened signature
|
| Output |
Output of BDDs/MTBDDs
|
R | |
| Reg |
Bounded unsigned integer expressions with BDDs
|