Decision Diagrams (DDs) are a well populated family of data structures, used for efficient representation and manipulation of huge data sets. Typically a given application requires choosing one particular category of DDs, like Binary Decision Diagrams (BDDs) or Data Decision Diagrams (DDDs), and sticking with it. Each category provides a language to specify its operations. For instance, the operation language of BDDs provides if-then-else, apply, etc. We focus on two main kinds of operation languages: BDD-like and DDDlike. They overlap: some operations can be expressed in both kinds of languages, while others are only available in one kind. We propose in this article a critical comparison of BDD-like and DDDlike languages. From the identified problems, we also propose a unified language for DD operations. It covers both BDD-like and DDD-like languages, and even some operations that cannot be expressed in either.
Decision Diagrams (DDs) are now widely used in model checking as an extremely
compact representations of state spaces [
Typically a given application requires choosing one particular category of DDs, like Binary Decision Diagrams (BDDs) or Data Decision Diagrams (DDDs), and sticking with it. Then, the user has to learn its operations, which might be a non-trivial task. DDs are used for both efficient memory representation and efficient computation time. But knowing which operation leads to better efficiency sometimes requires deep knowledge and understanding of the DD category.
Two solutions try to circumvent this problem. The first one is to use
highlevel Domain Specific Languages (DSLs), specific to an application domain. For
instance, CrocoPat4 completely hides the DDs and provides to the user a
language for manipulating relational expressions. We do not consider high-level
languages here. The second solution is automatic optimization of low-level
operations [
Section 2 first does a brief presentation of DDs. It presents the terminology we are using in the remainder of the article, and the categories of DDs we cover.
We compare two kinds of languages, those used in BDD-like structures (BDDs, Algebraic Decision Diagrams (ADDs), Multi-valued Decision Diagrams (MDDs), for instance) in Section 3, and those used in DDD-like structures (DDDs, Set Decision Diagrams (SDDs), Σ Decision Diagrams (ΣDDs)) in Section 4. They offer very different operations to their users. Moreover, their expressiveness differ. We think they are therefore good candidates for comparison.
We then propose in Section 5 low-level operations that generalize both BDDlike and DDD-like operations. They only apply to DDs where the function’s results are stored in terminal vertices, so Edge-Valued Decision Diagrams (EVDDs) are not covered in this article. Moreover, hierarchy as in SDDs and continuous input domains are not handled for simplicity. 2
Decision Diagrams are representations of functions using Directed Acyclic Graphs
(DAGs) with maximal sharing from the leaves and roots. DD categories differ on
the signatures of represented functions. We note B the Boolean domain and N
the natural integers. Function signatures are for instance Bn → B for BDDs [
Represented functions are total. They return a value in their ouput domain
for each value of their input domain. These domains can be infinite, either
because they are discrete but not bounded as in DDDs or ADDs [
A DD represents a function, which can also be seen as an association of each input element with an output one. We consider categories where every input element is a path of the graph, ending with a terminal vertex labeled by the function’s corresponding output value. Each vertex on the path is a variable of the function, and edges are labeled by their possible values. An order over
x 1 0 variables specifies the allowed succession of vertices in the graph. For instance, the Boolean function x ∨ y is represented by the BDD in Figure 1.
The function is described by the following
y {0, 1} 1 set of paths:
1
0
y
0
x −→0 y −→0 0, x −→0 y −→1 1
x −→1 y −→0 1, x −→1 y −→1 1
BDD-like operations are used on DDs representing functions with a finite and
homogeneous input domain. Their signatures are thus of the form Xn → O,
where X is a finite domain. This includes categories such as BDDs [
Several operations are defined for BDDs in [
The following operations form the BDD-like manipulation language. It is composed of functions, which take DDs (noted di), variables (vi), input values (xi), output values (ti) or operators ( ) as parameters. We give – informally – the result of each operation as its set of returned paths. constant(t)= nv1 −x→1 . . . vn −x−→n to6 constant(t) creates a DD where all paths lead to the terminal value t. It represents the constant function that returns t whatever its inputs are. apply( , dl, dr)= v1 −x→1 . . . vn −x−→n t1 t2 make(v, x) creates a DD where only the variable v is relevant to the function’s result. The paths where v has value x lead to terminal value 1, and others to terminal 0, even for DD categories with unbounded terminals such as ADDs. We explain this restriction in Problem 1. make(v, x)= v1 −x→1 . . . v −X−\−{−x→} . . . vn −x−→n 0 ∪ n v1 −x→1 . . . v −→x . . . vn −x−→n 1 o apply( , dl, dr) computes dl dr. It takes two DDs dl and dr representing functions of signature Xn → O, and a binary operator : O × O → O on their output domain. It returns the DD of the function computed by: ( v1 −x→1 . . . vn −x−→n t1 ∈ dl ) v1 −x→1 . . . vn −x−→n t2 ∈ dr ∧
6 We omit universal quantification on xi for readability, as in other operations.
restrict(v, x, d) restricts d to the value x of the variable v, and then ignores
this variable’s values. The returned function’s result is similar to the original
one, when v has value x, so this operation computes f |v=x. The resulting DD
still has all variables, including v, which has no effect on its result.
restrict(v, x, d)= nv1 −x→1 . . . v −→X . . . vn −x−→n t v1 −x→1 . . . v −→x . . . vn −x−→n t ∈ d
o
compose(v, dl, dr) substitutes the variable v in dl with the DD dr. Both DDs dl
and dr must represent functions of type Xn → X. This operation can be expressed
using apply and restrict, and does not appear in articles on BDDs other than [
The language for BDD-like operations is widely used, in many libraries and applications. The example given below7 builds a BDD for x ∧ y ∧ z. It then restricts the function for variable x = 0 and counts the paths leading to terminal 1. Results of operations are given as comments, after //. Notice that all operations, except satisfy-count, return a DD containing all variables x, y, z. Their declaration is required before executing the operation. As the operation is composed of nested function calls, it should be read from bottom to top. The call to constant is common in BDD programming, but not useful here. satisfy - count // =⇒ 2 ( 1 , restrict // =⇒ x −0−,→1 y −→0 z −→0 1 ∪ · · · → 0 ( x, 0 , apply // =⇒ x −→0 y −→0 z −→0 1 ∪ · · · → 0 ( ∧ , make (z , 0) // =⇒ x −0−,→1 y −0−,→1 z −→0 1 ∪ x −0−,→1 y −0−,→1 z −→1 0 , apply // =⇒ x −→0 y −→0 z −0−,→1 1 ∪ · · · → 0 ( ∧ , make (y, 0) // =⇒ x −0−,→1 y −→0 z −0−,→1 1 ∪ x −0−,→1 y −→1 z −0−,→1 0 , apply // =⇒ x −→0 y −0−,→1 z −0−,→1 1 ∪ x −→1 y −0−,→1 z −0−,→1 0 ( ∧ , make (x, 0) // =⇒ x −→0 y −0−,→1 z −0−,→1 1 ∪ x −→1 y −0−,→1 z −0−,→1 0 , constant (1) // =⇒ x −0−,→1 y −0−,→1 z −0−,→1 1 ) ) ) ) )
This language for BDD-like operations has several drawbacks. We describe them in the remainder of this section. Note that these drawbacks do not prevent wide use of this language.
Problem 1 (make restricts terminal values). Creating a DD with this operation requires a default value for other paths. For instance, make(x, 0) creates a DD returning 1 whenever x = 0, but implicitly also 0 for the other cases.
Boolean functions have a trivial implicit result, as only two terminal values are available. But it is not the case for ADDs, which represent functions Bn → N. Their implicit result is chosen as the identity element 0 of addition. With addition, all terminal values can be obtained, as in apply(+, make(x, 0), make(x, 0)) which returns x −→0 y −0−,→1 z −0−,→1 2 ∪ x −→1 y −0−,→1 z −0−,→1 0.
So, the set of terminal values should be a monoid for BDD-like operations. It requires defining a + operation to generate all possible terminal values. Note that constant can then be also restricted to the terminals’ generator only. Problem 2 (The language is not minimalist). The compose operation is redundant. It can be expressed using two other operations, apply and restrict. Usually, this is not a problem, as redundant operations can be safely removed from the language to get a minimal one. But the operation is specifically defined because its algorithm is more efficient. So, this BDD-like language is not minimalist, but removing the redundant operation has an efficiency cost.
The same task can be defined in several ways, that are not equivalent regarding efficiency. Writing a complex operation therefore requires knowledge from the user on how its evaluation internally works.
Problem 3 (The language requires embedding). A usual operation in model checking is to compute the fixed point of next states computation. But the BDD-like language has no operations for iteration or recursion. So, it requires to be embedded into a general-purpose language, that can compute the fixed point.
The BDD-like languages are thus truly DSLs. They describe an operation in
a concise and readable manner, but are not as expressive as a general-purpose
programming language. They can express only very simple computations.
Problem 4 (Operations cannot be optimized). In [
This problem is very similar to Problem 2, which occurs because the compose operation cannot be expressed efficiently enough using other operations. The language is not low-level enough to enable optimizations that could bring the same efficiency. Its operations take whole DDs as parameters and return a whole DD. So, the language lacks more intrusive operations, that apply to parts of the DDs. DDD-like operations presented in Section 4 define them, and have shown great optimizations thanks to lower-level operations. 4
The main difference between BDD-like and DDD-like structures is the input
domain of represented functions. In [
These categories include DDDs [
DDD-like operations are partitioned in two languages: a language of binary set operations (Sec. 4.1) and a language of unary set transformation (Sec. 4.2). They are not totally disjoint, as bridges exist between them. 4.1
Binary Set Operations The language of set expressions is composed of the usual binary set operations ∪, ∩, \ – or their multiset counterparts – applied to two DDs. These three operations are distinct, whereas they are all covered by apply in BDD-like operations. A general definition is difficult, because domains of variables can be unbounded. To preserve the finite graph representation of the function, an infinite number of paths must lead to terminal 0, whereas a finite number lead to other terminals. So, the operation applied to terminals should always return 0 when both its operands are 0 to ensure termination. A general apply could exist, given operator on terminals respects this constraint.
These operations are a small subset of BDD-like operations. For instance, they are not sufficient to compute a state space. So, they are completed with a language for set transformations. 4.2
Unary Set Transformations
The unary set transformations, initially proposed in [
These transformations are homomorphisms. They must therefore enforce a constraint: all must be linear for a union ∪ operator defined in the DD category: h(d1 ∪ d2) = h(d1) ∪ h(d2). The linearity property means that every input DD can be split in several DDs, then the operation applied to each, and the result obtained by union of their results. For simplicity, operations given below do not mention particular cases required by linearity. These cases are common to all operations, and are discussed in Problems 8 and 9. Note that these operations are applied on quasi-reduced DDs, i.e. without level skipping.
Unary transformations are parametric: they take parameters that define their behavior in addition to the DD to transform. To describe the language of such operations, we show each one with both kinds of parameters. The first one, between brackets, contains all parameters except the DD to transform. The second one, between parentheses, is this DD. We thus clearly distinguish between parameters that define the operation, and the parameter to which it is applied. terminal[t] is the only operation that allows to create a DD outside unary set transformations. It is therefore crucial, as the basis for each operation. This nullary operation creates a DD terminal valued by t. It is close to the constant BDD-like operation. But they differ because the DD returned by terminal represents the nullary function that returns t, whereas the DD returned by constant represents a n-ary function. terminal[t]()= {7→ t} constant[dc] returns the constant DD dc, whatever its input DD is. This operation is parameterized by the DD to return, and is applied to a DD that it ignores (almost, see Problem 8). The name of this operation can be misleading. The returned DD represents a function that can be constant or not: all its paths do not necessarily lead to the same terminal. But the constant operation returns this DD independently of its input. It thus differs from constant of BDD-like operations, which returns a constant function. constant[dc](d) = dc make[v −→x](d)= v −{−y−6=−x→} v1 −x→1 . . . vn −x−→n 0
v −→x v1 −x→1 . . . vn −x−→n t identity[] returns its input with no modification. This operation can be expressed using other operations, but is introduced in DDDs for efficiency. identity[](d) = d; make[v −→x] adds a prefix v −→x to a DD. It differs from the BDD-like make operations, because it adds a variable to the represented function given as parameter, whereas the BDD-like creates an n-ary function from scratch.
match[v −→x, h] is the inverse operation of make. It selects paths where v −→x is a prefix of the DD, and then applies another operation h to the subDD that prefix leads to. Other paths return the identity DD.
n o
v1 −x→1 . . . vn −x−→n t v −→x v1 −x→1 . . . vn −x−→n t ∈ d This operation is overloaded, as it also exists to match a terminal. match[t, h](d)= h ({t | t ∈ d}) composition[h1, h2] computes the composition h1 ◦h2, and applies it to its input DD. It has no relation with compose of BDD-like operations, which substitutes a variable with the result of a DD.
composition[h1, h2](d) = (h1 ◦ h2)(d) = h1(h2(d)) union[h1, h2] (respectively intersection) computes the union (resp. intersection) of results of h1 and h2 applied to the input DD. This operation wraps some of the set operations presented in Sec. 4.1. Set difference \ is not wrapped because it is not a linear operation. Note that these two operations can be easily extended to n-ary versions as they are associative and commutative. union[h1, h2](d) = h1(d) ∪ h2(d) intersection[h1, h2](d) = h1(d) ∩ h2(d) fixpoint[h] has been introduced for model checking applications. Problem 3 shows that BDD-like languages lack operations for iteration. fixpoint provides such an operation. It computes the fixed point of h, applied to the input DD. fixpoint[h](d) = h∞(d) = h(. . . h(d) . . . )
The DDD-like unary set transformations are much more expressive than the BDD-like operations. Figure 2 shows a Petri net and an operation that computes its state space, which will be improved later. The operation uses the fixpoint operator where BDD-like operations require to be embedded in a general purpose language. To encode an least fixed point, identity is used to keep previously computed states.
We show how the operation works by applying the operation for transition t to the DDD path q −→1 p −→2 r −→0 1 representing the initial state of the Petri net. =⇒ =⇒ =⇒ =⇒ =⇒ q −→0 p −→0 make[r −→1, . . .] (1) =⇒ q −→0 p −→0 r −→1 match[1, . . .] (1) q −→0 p −→0 match[r −→0, . . .] (r −→0 1) q −→0 match[p −→2, . . .] (p −→2 r −→0 1) q −→0 make[p −→0, . . .] (r −→0 1) match[q −→1, . . .] (q −→1 p −→2 r −→0 1) make[q −→0, . . .] (p −→2 r −→0 1) =⇒ =⇒ q −→0 p −→0 r −→1 identity[] (1)
q −→0 p −→0 r −→1 1 Problem 5 (Operations usually must be lazily defined). The operation given in Figure 2 has a bug, because the match operation for transition u requires exactly one token in p. So, it cannot be applied from the initial state. We have to enumerate all possible cases, by adding : , match [q −→1, make [q −→0, match [p −→1, make [p −→0,
match [r −→0, make [r −→1, match [1, identity []. . .] // u
We cannot express “add n tokens” or “remove n tokens”, only “set to n tokens”. In practice, an operation usually has an a priori unbounded number of match calls. They will be discovered during computation. Description of the operation would be infinite, so it is in practice rather defined lazily. Then match uses a function returning the operation associated with each encountered value. Problem 6 (Lazy operations cannot be optimized). The operations that compute the state space of Petri net in Figure 2 can be optimized. The operation p
t 1 2 1 1 v 1 r 1 1 u
q 1 1 fixpoint [ union [
identity , match [q −→1, make [q −→0, match [p −→2, make [p −→0, , match [q −→1, make [q −→0, match [p −→1, make [p −→0,
match [r −→0, make [r −→1, match [1, identity []. . .] // t , match [q −→0, make [q −→1, match [p −→0, make [p −→1, match [r −→0, make [r −→1, match [1, identity []. . .] // u match [r −→1, make [r −→0, match [1, identity []. . .] // v , match [q −→1, make [q −→0, union [ match [p −→1, make [p −→0, match [r −→0, make [r −→1, match [1, identity []. . .] , match [p −→2, union [ make [p −→0, match [r −→0, make [r −→1, match [1, identity []. . .] make [p −→1, match [r −→0, make [r −→1, match [1, identity []. . .]
]. . .] , match [q −→0, make [q −→1, match [p −→0, make [p −→1,
match [r −→1, make [r −→0, identity []. . .]
Non-optimized and optimized ones are expressed in the same language. So, the language is suitable for optimization by program transformation. It solves the Problem 4 of BDD-like languages.
Lazy operations seen in Problem 5 are useful to deal with a priori unbounded structures. But they have a drawback: they cannot be optimized, because their suboperations are not known until execution. To circumvent the problem, new operations have been added in DDD-like languages. They are redundant with existing ones, but provide the missing information. However, as more optimizations are added, more specific operations like these must also be added. This approach creates several redundant ways to define the same operations. Users have to know which one is better to enable most optimizations.
Problem 7 (Weak typing). Each operation is designed to work on DDs of
a given type, i.e. a variable order and a category that defines the variables’
domains and output domain. For instance, the following operation can only be
applied to DDDs of variable order x < y. It detects the path x −→1 y −→1 1.
match [x −→1, match [y −→1, match [1, constant [ terminal [
Operations’ operands which are DDs are not explicitly typed. Only the user knows their type. So, an operation can discover at runtime that it is not applied to an intended operand. The operation then fails, but how this failure is reported is unclear in the DDD-like languages: return of a special terminal >, assertion to stop the program, exception that can be caught. . . or even return of terminal 0 which is in fact silent.
Instead of giving a DD of the wrong type to an operation, typing errors can
also appear because of DDs returned by inner operations. This leads to errors
(known in DDDs as the “top” > terminal) that are hard to debug8. Such a typing
error occurs when operands of union or intersection do not return DDs of the
same type. For instance, the following operation is erroneous because the first
part of union returns a DDD with variable order x < y whereas the second has
variable order y < x.
union [ make [x −→1, make [y −→0, constant [ terminal [
, make [y −→1, make [x −→0, constant [ terminal [
It seems easy here to check the typing problems. But lazy operations, required for Problem 5, prevent checking in most practical cases.
Problem 8 (An identity DD is only transformed to an identity DD). The linearity constraint of homomorphisms requires that every DD can be split in several other DDs, operations applied to them, and their results merged.
Each DD can be decomposed to itself and the identity DD (noted d0), where all paths lead to terminal 0. From the definition of linearity, a DD can be decomposed in itself and the identity, as in h(d) = h(d ∪ d0) = h(d) ∪ h(d0). So, every operation must return the identity DD when applied to the identity d0. 8 Users that have used at least once a DDD library know the pain to look at thousands of lines of DD paths to search where something went wrong.
For instance, all operations applied to the DDD representing the empty set return the empty set. Even constant[dc](d0) cannot return its DD parameter dc when applied to d0. In this particular case, it must return the identity d0. This constraint does not exist in BDD-like operations. They can return any DD when applied to the identity one.
This requirement prevents the user of DDD-like operations to start its application with the identity DD, and then filling it through operations. In model checking applications using DDDs, we have to start therefore with an initially non-empty set of states, which is usually the initial state.
Problem 9 (Operations on terminals must also be linear). This is another consequence of homomorphisms, as in Problem 8. Consider a DD representing multisets. Each path represents an element of the multiset, its terminal represents its cardinality. The multiset union sums the terminals of identical paths. Because each DD can be decomposed, the result computed for a path leading to n must be the same as the sum of results for the same path ending with n1 and n2, where n = n1 + n2.
For instance, Fig. 3 shows an operation that tries to count paths leading to terminal 1. Its result is computed by adding all subresults, given as destinations of red bold arrows. The final result is shown for a DD (left part) and for one arbitrary decomposition of the DD (right part). They differ, because the operation on terminals is not linear.
x 0 2 1 1 0 + ⇔ 1 x 0
1 1 + x 1 1 0
6= = 3
Fig. 3. Counting paths leading to terminal 1 is not a linear operation
Users specify operations only for paths leading to 1 in DDDs. This category
has Boolean terminals, and homomorphisms always return the identity DD d0
when paths end with 0. For DDs representing multisets (MSDDs in [
Problem 10 (Goal of restriction to linear operations is unclear). Even
if we allow operations to return not only DDs, but also other data types such
as integers, the linearity constraint is too restrictive for many operations. For
instance, even a simple operation like counting the number of paths leading to
a particular terminal value is not a linear operation (see Fig. 3 of Problem 9).
DDD-like languages have an operation to count paths, but it cannot be used
within linear operations. So, this special operation is doomed to appear only
at the end of a computation. The reason why DDDs define their operations
as homomorphisms is not explicitly given in [
We believe that the main justification for such constraints is efficiency.
Linearity, h(d1 ∪ d2) = h(d1) ∪ h(d2), ensures not only that a DD can be decomposed to its paths to compute the operation’s result, but also that the subresults can always be combined before the next computation. Consider the operation (f ◦ g)(d1 ∪ d2). It can be rewritten as the union of two compositions (f ◦ g)(d1) ∪ (f ◦ g)(d2), or as f (g(d1) ∪ f (g(d2)). In both cases, the result if the same, whether f is applied to two subresults g(d1) and g(d2), or to their union g(d1) ∪ g(d2). The second case is likely to do less computations9 than the first one, thus saving time and memory.
This optimization is possible because of the linearity constraint. We propose in Sec. 5 to move this constraint where it should be: as an optimization enabled only when operations can be proven linear.
Problem 11 (Unary operations are not enough). Some operations, such as set union ∪, intersection ∩ or difference \ for DDDs are not unary. As DDDlike set transformations are unary only, there is no way for a user to describe them inside the homomorphisms framework.
Restriction to unary functions is useful to define operations as combinators. For instance, composition[match[x −→1, identity], make[y −→0, identity]] is a unary operation, because each suboperation is also unary and returns exactly one result. The input DD argument of composed functions is implicit.
Composition of n-ary operations does not allow such shortcuts, because several links can exist between the inputs and outputs of composed operations. But n-ary operations are the general case, that is missing in DDD-like operations. 5
We propose in this section a language for generalized operations, that solves the problems identified in Sections 3 and 4. This language covers both BDD-like and DDD-like languages. Throughout the section, a simple program given in Fig. 4 is used as example. It counts the similar paths in two DDs. Note that the proposed operations are applied to quasi-reduced DDs, as in DDD-like unary operations. Missing parts must be rebuilt on-the-fly when the operations are applied. Program A program is a set of named operations, like check , check y, check x<y and count in Fig. 4. Naming enables recursion. There is therefore no need for a particular fixpoint operation, nor embedding loops in a general-purpose language (Problem 3). One of these named operations is called by the user. Typed inputs and outputs Each named operation has typed inputs and outputs (Problem 7). For instance, count(l: in t, r: in t, o: out int) has two inputs l and r of the same type t, and one output o of type int. To handle n-ary operations (Problem 11), several – or no – inputs and outputs are possible. All of them are DDs, for homogeneity, even values (int) are considered as terminals. Operand types are defined by a DD category (BDD, DDD, etc.) and a variable order. We
check (l: in v , r: in v , o: out int ) = match | l: |t| , r: |t| ⇒ o ←make |1|
| l: |t| , r: |u| ⇒ o ←make |0| check y (l: in u, r: in u, o: out int ) = match | l : y −→v dl, r : y −→v dr ⇒ check (l ← dl, r ← dr, o → o)
| l : y −→u dl, r : y −→v dr ⇒ o ←make |0| check x<y (l: in t, r: in t, o: out int ) = match | l : x −→v dl, r : x −→v dr ⇒ check y(l ← dl, r ← dr, o → o)
| l : x −→u dl, r : x −→v dr ⇒ o ←make |0|
count (l: in t, r: in t, o: out int ) =
merge o from check x<y(l ← l, r ← r, o) with +
propose in [
We use four types of DDs in our example. Three types correspond to DDs with Boolean terminals and unbounded variables: no variable (type v), variable y (type u) and variables x < y (type t). The fourth type corresponds to DDs with natural terminals and no variables (type int ), used to count the results. Predefined operation templates Operations can be of three kinds, that we call “operation templates”. They are inspired from DDD-like operations, but are minimalist as each one has a very specific role. They thus solve Problem 2. match | prefix n ⇒ call | . . . takes as parameter a finite mapping from prefix patterns to operation calls. As we deal with n-ary operations, a pattern is composed of n prefixes, one for each input operand. For each set of DD paths, one taken from each operand, this operation finds the first matching pattern, and applies the associated operation. A prefix can be: – a terminal constant or placeholder10 for instance |1| or |t|, – a DD placeholder (which also covers a terminal), for instance d, – a prefix with constants or placeholders as variable or/and edge values, and another prefix for the successor, for instance 1 −→x d, x −→0 d, or x −→y|t|.
As in functional languages with pattern-matching, all the patterns of a match must cover all possible prefixes of the input DDs. They also must bind all the outputs of the operation. The following binary operation, which uses the value of x as discriminant, is only valid when x has a Boolean domain. match | d1 : x −→1 d, d2 : x −→y d0 ⇒ . . . | d1 : x −→0 d, d2 : x −→y d0 ⇒ . . . di are the names of input parameters that are matched against a prefix, and “ . . . ” is here the next operation to perform (not given). Scope of placeholders is in their pattern, so the two ys are distinct in the previous example, but the two xs in a pattern x −→x have the same value. The following unary operation is valid even for unbounded domains, as placeholder y can take any value. 10 We name terminal placeholder a language variable that can store a terminal value.
The term “variable” is already used in DDs, so we do not use it to avoid ambiguities. match | d1 : x −→x d ⇒ . . . | d1 : x −→y d ⇒ . . .
Note that patterns overlap in the previous examples. We chose the usual policy of functional languages: only the first matching pattern is applied. This is useful to define default cases.
Operation calls bind inputs and outputs of caller and callee. We can wrap a placeholder with an expression, to compute a value from its content. However, we do not describe expressions here, by lack of space. So, placeholders are simply bound to inputs and outputs of operations. make | pattern | . . . creates a DD from patterns using constants and placeholders. Patterns are expressed in the same way as in match. They must also cover all possible prefixes of created DD. In Fig.4, we only create terminals, but this operation can also create DD nodes. For instance, the code below creates the DD x −→0 0 ∪ x −→1 1, when d is a placeholder holding the terminal 0, x is a variable and y is a free placeholder of Boolean domain. Placeholders used in the patterns can be bound to a value or be free. The latter case is useful to fill a whole unbounded domain. make | x −→0 d | x −→y|1|
As patterns may overlap, we chose a policy consistent with match: when a prefix can be created using several patterns, the first one prevails. Note that this operation template does not require a default value, and thus solves Problem 1. merge placeholder from call with operator is a new operation. It is required because there is no more a global ∪ operator as in DDD-like languages. Each match operation does not return a single DD, but a multiset of DDs, because it generates one or several DDs for each matching prefix. merge maps operations to how their results should be merged. The operator used to merge results (+ in Fig 4) is specified only for terminals, following the BDD-like apply mechanism. It is applied on terminals of paths that differ only by their terminal values.
This operator must be associative and commutative, because there is no order on generated DDs. Moreover, when dealing with unbounded domains, it must have an identity element. Homomorphisms are a special case, where the merge operator respects linearity. 6
This article does a critical comparison of BDD-like and DDD-like manipulation languages. It also proposes a new language for manipulation of DDs, that takes inspiration from both BDD-like languages and DDD-like languages, and covers them. This language also enables more operations. We give the example of counting paths that are similar in two DDs. This operation cannot be defined in the BDD-like and DDD-like languages, but is available in our proposal. The proposed language solves the problems we identify, such as minimalism of the language or expressiveness. It provides a small number of operations that have been carefully designed to allow future optimizations and are general enough to handle n-ary typed operations.
We plan to extend the proposed language to hierarchical DDs, as they are useful DD categories. Moreover, we have to redefine the optimizations that already exist for SDDs. Adding some kind of genericity to the language is also required, because the proposed specification of types can prevent code reuse.