Factorizing Equivalent Variable Pairs in ROBDD-Based Implementations of Pos

Roberto Bagnara^{1}^{,}^{⋆} and Peter Schachte^{2}

1 Dipartimento di Matematica, Università di Parma, Via M. D’Azeglio 85/A, Parma,

               Italy, bagnara@prmat.math.unipr.it

2 Department of Computer Science, The University of Melbourne, Parkville, Victoria

                3052, Australia, pets@cs.mu.oz.au

Abstract. The subject of groundness analysis for (constraint) logic programs has been widely studied, and interesting domains have been proposed. Pos has been recognized as the most suitable domain for capturing the kind of dependencies arising in groundness analysis, and Reduced Ordered Binary Decision Diagrams (ROBDDs) are generally accepted to be the most efficient representation for Pos. Unfortunately, the size of an ROBDDs is, in the worst case, exponential in the number of variables it depends upon. Earlier work [2] has shown that a hybrid representation that separates the definite information from the dependency information is considerably more efficient than keeping the two together. The aim of the present paper is to push this idea further, also separating out certain dependency information, in particular all pairs of variables that are always either both ground or neither ground. We find that this new hybrid representation is a significant improvement over previous work.

1 Introduction

The aim of groundness analysis (sometimes called definiteness analysis) is to derive statically, for all the program points of interest, which variables are bound to unique values (or ground). This kind of information is very important: it allows substantial optimizations to be performed at compile-time, and is also crucial to most semantics-based program manipulation tools. Moreover, many other analyses are made more precise by the availability of groundness information. For these reasons, the subject of groundness analysis for (constraint) logic programs has been widely studied. After the early attempts, some classes of Boolean functions have been recognized as constituting good abstract domains for groundness analysis [10, 13]. In particular, the set of positive Boolean functions, (namely, those functions that assume the true value under the valuation assigning true to all variables), which is denoted by Pos, allows to express Boolean properties of program variables where the property of one variable may depend on that property of other variables. For groundness analysis, since variables can be bound to terms containing other variables, the groundness of one variable may depend on

⋆ Much of this work was supported by EPSRC grant GR/L19515.

the groundness of other variables. Pos has been recognized as the most precise domain for capturing the kind of dependencies arising in groundness analysis.

This ability to express dependencies makes analysis based on Pos very precise, but also makes it relatively expensive, as many operations on Boolean formulae have exponential worst case complexity. Armstrong et al. [1] analyzed many representations of positive Boolean formulae for abstract interpretation, and found Reduced Ordered Binary Decision Diagrams (ROBDDs) [6] to give the best performance.

ROBDDs generated during program analysis often contain many variables that are definitely true. In the context of groundness analysis, this means that the corresponding program variable must be ground at that point in the program. It is shown in [2] that a hybrid representation for Boolean functions that keeps these definite variables separate is more efficient than ROBDDs alone. However, ROBDDs generated during program analysis also contain many pairs of variables that are equivalent. In terms of groundness, this means that either both variables are ground, or neither is. Such equivalent variables of course appear for a program goal of the form X = Y, but they also frequently appear naturally during the analysis process. For example, for a goal X = [Y|Z], where it can be established that Y is ground, the analyzer will deduce that X and Z are equivalent. Such equivalent pairs can greatly increase the size of ROBDDs, which in turn makes ROBDD operations much more expensive. For example, the ROBDD for the Boolean function z comprises one node (not counting the 1 and 0 terminal nodes), while (x ↔ y) ∧ z comprises 4 or 5 (usually 5). However, since x ↔ y simply means that x and y are equivalent, we may remove y from the Boolean function altogether, leaving us again with a single node, and replace y by x in the formulae being analyzed. Since the time complexity of most ROBDD algorithms is at best quadratic in the sizes of the graphs involved, this can significantly speed up analysis.

There is another reason for our interest in equivalent variables. A recursive definition of the form

f(x_{1}, …, x_{n}) = A ∨ (B ∧ f(x_{1}, …, x_{n})),

always has least fixpoint A, as can be seen by Kleene iteration. This is a special instance of Søndergaard’s immediate fixpoint theorem [16]. The key point here is that the formal parameters of the definition must be the same as the actual parameters in the recursive reference. We can establish this if we have a definition of the form

f(x_{1}, …, x_{n}) = A ∨ (B ∧ f(y_{1}, …, y_{n}) ∧ (x_{1} ↔ y_{1}) ∧ ⋯ ∧ (x_{n} ↔ y_{n})).

To show that our definition has this form, we need to find the equivalent variables in the recursive arm of the definition.

In this paper we present a hybrid representation for Boolean functions that uses a set to represent definite variables, a set of pairs of equivalent variables to represent equivalences, and an ROBDD to represent more complex dependencies.

This hybrid representation proves to be significantly more efficient overall than that of [2].

Notice that Boolean functions are used in the more general context of dependency analysis, including finiteness analysis for deductive database languages [5] suspension analysis for concurrent (constraint) logic programming languages [11], and functional dependency (or determinacy) analysis [17]. The hybrid representation we propose might be useful also in these contexts, although we have not studied this yet.

The balance of this paper proceeds as follows. In Sect. 2 we briefly review the usage of Boolean functions for groundness analysis of (constraint) logic programs (even though we assume familiarity with this subject) and we discuss the representation we use for Boolean functions. Section 3 presents our hybrid representation, with the necessary algorithms appearing in Sect. 4. Experimental results are presented in Sect. 5, and Sect. 6 concludes with some final remarks.

2 Preliminaries

Let U be a set. The set of all subsets of U will be denoted by ℘(U). The set of all finite subsets of U will be denoted by ℘_{f}(U). The notation S ⊆_{f} T stands for S ∈ ℘_{f}(T).

2.1 Boolean Functions for Groundness Analysis

After the early approaches to groundness analysis [14, 12], which suffered from serious precision drawbacks, the use of Boolean functions [10, 13] has become customary in the field. The reason is that Boolean functions allow to capture in a very precise way the groundness dependencies that are implicit in unification constraints such as z = f(g(x), y): the corresponding Boolean function is (x ∧ y) ↔ z, meaning that z is ground if and only if x and y are so. They also capture dependencies arising from other constraint domains: for instance, under CLP(R) x + 2y + z = 4 can be abstracted as ((x ∧ y) → z) ∧ ((x ∧ z) → y) ∧ ((y ∧ z) → x), indicating that determining any two variables is sufficient to determine the third.

Vars is a fixed denumerable set of variable symbols. The variables are ordered by the total order relation ≺. For convenience we sometimes use y ≻ x as an alternative for x ≺ y. We also use x ⪯ y and y ⪰ x to mean that either x ≺ y or x = y. We call the least variable α, that is, ∀v ∈ Vars : α ⪯ v. For a set of variables S we will denote by min^{≺}(S) the minimum element of S with respect to ≺. We also define the succ (successor) function over Vars as follows:

Definition 1. (The function succ: Vars → Vars.)

succ(v) =^{def} x, if v ≺ x and ¬∃y ∈ Vars . v ≺ y ≺ x.

Note that x is unique.

We now introduce Boolean functions based on the notion of Boolean valuation.

Definition 2. (Boolean valuations.) The set of Boolean valuations over Vars is A =^{def} Vars → {0, 1}. For each a ∈ A, each x ∈ Vars, and each c ∈ {0, 1} the valuation a[c/x] ∈ A is given, for each y ∈ Vars, by

a[c/x](y) =^{def} \{ \begin{matrix}c, & if x = y; \\ a(y), & otherwise. \end{matrix}

For X = {x_{1}, x_{2}, … } ⊆ Vars, we write a[c/X] for a[c/x_{1}][c/x_{2}] · · ·.

Definition 3. (Boolean functions.) The set of Boolean functions over Vars is F =^{def} A → {0, 1}. The distinguished elements ⊤, ⊥ ∈ F are the functions defined by ⊤ =^{def} λa ∈ A . 1 and ⊥ =^{def} λa ∈ A . 0. For f ∈ F, x ∈ Vars, and c ∈ {0, 1}, the function f[c/x] ∈ F is given, for each a ∈ A, by f[c/x](a) =^{def} f(a[c/x]). When X ⊆ Vars, f[c/X] is defined in the obvious way. If f ∈ F and x, y ∈ Vars the function f[y/x] ∈ F is given, for each a ∈ A, by

f[y/x](a) =^{def} f(a[a(y)/x]).

Boolean functions are constructed from the elementary functions corresponding to variables, and by means of the usual logical connectives. Thus x denotes the Boolean function f such that, for each a ∈ A, f(a) = 1 if and only if a(x) = 1. For f_{1}, f_{2} ∈ F, we write f_{1} ∧ f_{2} to denote the function g such that, for each a ∈ A, g(a) = 1 if and only if both f_{1}(a) = 1 and f_{2}(a) = 1. The other Boolean connectives and quantifiers are handled similarly.

The question of whether a Boolean function f entails particular variable x (which is what, in the context of groundness analysis, we call definite groundness information) is equivalent to the question whether f → x is a tautology (namely, f → x = ⊤). In what follows we will also need the notion of dependent variables of a function, as well as disentailed, or definitely false, variables.

Definition 4. (Dependent, true, false, and equivalent variables.) For f ∈ F, the set of variables on which f depends, the set of variables necessarily true for f, the set of variables necessarily false for f, and the set of equivalent variables for f, are given, respectively, by

vars(f) =^{def} { x ∈ Vars | ∃a ∈ A . f(a[0/x]) ≠ f(a[1/x]) },
true(f) =^{def} { x ∈ Vars | ∀a ∈ A : f(a) = 1 ⟹ a(x) = 1 },
false(f) =^{def} { x ∈ Vars | ∀a ∈ A : f(a) = 1 ⟹ a(x) = 0 },
equiv(f) =^{def} { (x, y) ∈ Vars^{2} | x ≠ y, ∀a ∈ A : f(a) = 1 ⟹ a(x) = a(y) }.

2.2 Binary Decision Diagrams

Binary Decision Diagrams (BDDs) are a well-known representations of Boolean functions [6, 7]. A BDD is a rooted directed acyclic graph where each internal node is labeled with a Boolean variable and has two out edges, leading to the node’s true and false successors. External (leaf) nodes are either 1 or 0. The Boolean function represented by an BDD can be evaluated for a given truth value assignment by traversing the graph from the root node, taking the true edge for nodes whose label is assigned 1 and the false edge when the label is assigned 0. The terminal node reached in this traversal is the function value for that assignment.

When a total ordering on the variables is available, we can define Ordered Binary Decision Diagrams (OBDDs) as BDDs with the restriction that the label of a node is always less than the label of any internal node in its successors. Reduced Ordered Binary Decision Diagrams (OBDDs) are OBDDs with the additional condition that they do not contain any two distinct nodes which represent the same Boolean function. This means that the two terminal nodes must be unique, no two distinct nodes may have the same label and true and false successors, and no node may have two identical successors (because then it would represent the same Boolean function as the successors).

We now define ROBDDs formally. Although an ROBDD is a particular kind of rooted, directed, and acyclic graph, we prefer not to use the standard notation for graphs. Thus an ROBDD is identified with the set of its nodes, one of which is designated as the root, the edges being formally part of the nodes themselves.

Definition 5. (ROBDD) If N is the set of nodes of an ROBDD then N satisfies

N ⊆ {0, 1} ∪ Vars × N × N.

The nodes 0 and 1 are called terminal nodes. All the other nodes in N are called non-terminal nodes. For each non-terminal node n ∈ N, n_{var} ∈ Vars denotes the variable associated with n, n_{false} ∈ N denotes the false successor of n, and n_{true} ∈ N denotes the true successor of n. With this notation, N must also satisfy the irredundancy and the ordering conditions: for each non-terminal node n ∈ N n_{false} ≠ n_{true} and (m = n_{false} or m = n_{true}) ⟹ (m ∈ {0, 1} or n_{var} ≺ m_{var}). Moreover, N is rooted and connected, that is, there exists r ∈ N (the root) such that

∀n ∈ N \ {r} : ∃m ∈ N . (n = m_{false} or n = m_{true}).

A ROBDDs is a pair (r, N) that satisfies the above conditions. The set of all ROBDDs is denoted by D.

The meaning of an ROBDD is given as follows.

Definition 6. (Semantics of ROBDDs.) The function ⟦·⟧_{D}: D → F is given, for each (r, N) ∈ D, by N′ =^{def} N \ {r} and

⟦(r, N)⟧_{D} =^{def} \{ \begin{matrix}⊥, & if r = 0; \\ ⊤, & if r = 1; \\ (r_{var} ∧ ⟦(r_{true}, N′)⟧_{D}) ∨ (¬r_{var} ∧ ⟦(r_{false}, N′)⟧_{D}), & otherwise. \end{matrix}

For simplicity, we will identify an ROBDD with the ROBDD node that constitutes its root, since the set of all the nodes can be recovered by any traversal that starts from the root.

In the implementation, a new ROBDD node is created, given a label variable v and true and false successors n and m respectively, by the make node(v, n, m) function. This is defined such that, if n = m, n will be returned. Furthermore, if an identical call to make node has previously been made, the result of that call will be returned. This guarantees that if n and m are reduced, then so is the resulting node. Note that it is an error if v ⪰ n_{var} or v ⪰ m_{var}.

ROBDDs have one very important property: they are canonical. This means that, for each fixed variable ordering, two ROBDDs represent the same function if and only if they are identical [6]. In fact, the definition of make node is such that two ROBDDs are identical if and only if they are stored at the same memory address. This is important to the efficiency of many ROBDD operations.

We will often confuse ROBDDs with the Boolean functions they represent. For instance, for n ∈ D, when we write vars(n) or true(n) what we really mean is vars(⟦n⟧_{D}) or true(⟦n⟧_{D}). This convention of referring to the semantics simplifies the presentation and should not cause problems.

3 A New Representation for Pos

We introduce a new representation for Pos. It is made up of three components: a set of ground variables, a set of equivalent variables, and an ROBDD, whence the name GER representation.^{1} A set of ground variables is trivially an element of V =^{def} ℘_{f}(Vars). For G ∈ V we define ⟦G⟧_{V} =^{def} ⋀(G), where ⋀{x_{1}, …, x_{n}} =^{def}

x_{1} ∧ ⋯ ∧ x_{n} and ⋀ ∅ =^{def} ⊤.

The set of equivalent variables is simply given by a transitively closed set of ordered pairs of variables.

Definition 7. (A representation for equivalent variables.) Sets of equivalent variables are represented by means of elements of L ⊆ ℘_{f}(Vars × Vars) such that

1. ∀L ∈ L : ∀x, y ∈ Vars : (x, y) ∈ L ⟹ x ≺ y;

2. ∀L ∈ L : ∀x, y, z ∈ Vars : (x, y), (y, z) ∈ L ⟹ (x, z) ∈ L.

For L ∈ L we use the following notation:

L|1 =^{def} { x ∈ Vars | (x, y) ∈ L },  vars(L) =^{def} L|1 ∪ L|2,
L|2 =^{def} { y ∈ Vars | (x, y) ∈ L }.

The family of functions λ_{L}: Vars → Vars is defined, for each L ∈ L and each x ∈ Vars, by λ_{L}(x) =^{def} min^{≺}({x} ∪ { y ∈ Vars | (y, x) ∈ L }). λ_{L} maps each variable to the least variable of its equivalence class, which we call its leader. (L, ⊇) is

1 In [2] we had only a set of ground variables and a ROBDD.

clearly a lattice. We will denote the glb and the lub over (L, ⊇) by ∧_{L} (transitive closure of the union) and ∨_{L} (intersection), respectively. The semantics function

⟦·⟧_{L}: L → F is given by ⟦L⟧_{L} =^{def} ⋀{ x ↔ y | (x, y) ∈ L }.

In the GER representation, an element of Pos is represented by an element of V × L × D. There are elements of Pos that can be represented by several such triples and, in the GER representation, we need to make a choice among those. This choice must be canonical and economical. Economy can be explained as follows: true variables are most efficiently represented in the first component (a bit-vector at the implementation level) and should not occur anywhere else in the representation. Equivalent variables are best represented in the second component of the GER representation (implemented as a vector of integers). As equivalent variables partition the space of variables into equivalence classes, only one variable per equivalence class must occur in the ROBDD constituting the third component of the representation. If we choose, say, the least variable (with respect to the ⪯ ordering on Vars) of each equivalence class as the representative of the class, we have also ensured canonicity.

Definition 8. (GER representation.) The GER representation for Pos is given by the set

G =^{def} \{ ⟨G, L, n⟩ | \begin{matrix}G ∈ V, L ∈ L, n ∈ D, \\ G ∩ vars(L) = G ∩ vars(n) = L|2 ∩ vars(n) = ∅, \\ true(n) = equiv(n) = ∅ \end{matrix} \}.

The meaning of G’s elements is given by the function ⟦·⟧_{G}: G → F:

⟦⟨G, L, n⟩⟧_{G} =^{def} ⟦G⟧_{V} ∧ ⟦L⟧_{L} ∧ ⟦n⟧_{D},

What is required now is a normalization function mapping each element of V × L × D into the right representative in G.

Definition 9. (Normalization function η.) The function η: V × L × D → V × L × D is given by

η(⟨G, L, n⟩) =^{def} ⟨Ĝ, L̂, n̂⟩

where

Ĝ =^{def} true(⟦⟨G, L, n⟩⟧_{G}),
L̂ =^{def} equiv(⟦⟨G, L, n⟩⟧_{G}) \ { (x, y) ∈ Ĝ^{2} | x ≺ y },
n̂ =^{def} n[1/Ĝ][λL̂(x_{1})/x_{1}] ⋯ [λL̂(x_{n})/x_{n}], if vars(n) \ Ĝ = {x_{1}, …, x_{n}}.

A very basic implementation for η is given by the normalize function depicted in Alg. 1. The need for looping can be understood by means of the following examples. Forcing a variable to true in a ROBDD can result in new entailed

Require: an element ⟨G, L, n⟩ ∈ V × L × D

function normalize(⟨G, L, n⟩) 1: G_{new} := G; L_{new} := L; n_{new} := n; 2: repeat 3: G_{old} := G_{new}; L_{old} := L_{new}; n_{old} := n_{new}; 4: G_{new} := G_{new} ∪ { x, y | (x, y) ∈ L_{new}, {x, y} ∩ G_{new} ≠ ∅ } 5: L_{new} := L_{new} \ { (x, y) ∈ G_{new}^{2} | x ≺ y } 6: n_{new} := n_{new}[1/G_{new}]; 7: G_{new} := G_{new} ∪ true(n_{new}); 8: L_{new} := L_{new} ∧_{L} equiv(n_{new}); 9: {x_{1}, …, x_{k}} := vars(n_{new}); 10: n_{new} := n_{new}[λ_{L_{new}}(x_{1})/x_{1}] ⋯ [λ_{L_{new}}(x_{k})/x_{k}] 11: until G_{new} = G_{old} and L_{new} = L_{old} and n_{new} = n_{old}; 12: return ⟨G_{new}, L_{new}, n_{new}⟩;

Algorithm 1: The normalize function.

variables: if n represents x → y then n[1/x] represents y. Renaming a ROBDD node n by means of a set of equivalent variables L can also give rise to new entailed variables. Suppose that n represents the Boolean formula x∨y and that L = {(x, y)}. Then n[λ_{L}(y)/y] represents x. Renaming can also result in new equivalent variables: take n representing x ↔ (y ∧ z) and L = {(y, z)} for an example.

Theorem 1. We have that η: V × L × D → G. Furthermore, for each triple ⟨G, L, N⟩ ∈ V × L × D, we have

⟦⟨G, L, N⟩⟧_{G} = ⟦η(⟨G, L, N⟩)⟧_{G}.

Finally, the normalize function in Alg. 1 is a correct implementation of η.

It is important to remark that in the actual implementation several specializations are used instead of Alg. 1. In other words, for every possible use of normalize, conditions can be granted so as to use a simpler algorithm instead. While space limitations do not allows us to be more precise, we just observe that roughly 50% of the times normalize would be called with the ROBDD 1. This indicates that definitely ground variables and equivalent variables constitute a significant proportion of the dependencies that arise in practice.

3.1 Operations for the Analysis

Let us briefly review the operations we need over Pos for the purpose of groundness analysis. Modeling forward execution of (constraint) logic programs requires computing the logical conjunction of two functions, the merge over different computation paths amounts to logical disjunction, whereas projection onto a designated set of variables is handled through existential quantification. Conjunction with functions of the form x ↔ (y_{1} ∧ ⋯ ∧ y_{k}), for k ≥ 0, accommodate both abstract mgus and the combination operation in domains like Pat(Pos) [9].

Let Ω be an operation over Pos. The corresponding operation over G can be specified, roughly speaking, as η ∘ Ω ∘ ⟦·⟧_{G}. However, this is simply a specification: the problem is how to compute η ∘ Ω ∘ ⟦·⟧_{G} more efficiently exploiting the fact that both definitely ground variables and pair of equivalent variables are kept separate in the GER representation. The intuitive recipe (which has been extensively validated through experimentation) for achieving efficiency can be synthesized in the motto “keep the ROBDD component as small as possible and touch it as little as possible”. The specification above does the contrary: it pushes all the information into the ROBDD component, performs the operation on the ROBDD, and normalizes the result. Let us take the conjunction operation ∧_{G}: G × G → G and suppose we want to compute ⟨G_{1}, L_{1}, n_{1}⟩ ∧_{G} ⟨G_{2}, L_{2}, n_{2}⟩. A first approximation is to compute

η(⟨G_{1} ∪ G_{2}, L_{1} ∧_{L} L_{2}, n_{1} ∧_{D} n_{2}⟩),  (1)

but we can do better if we reduce the ROBDDs n_{1} and n_{2} before computing the conjunction (whose complexity is O(|n_{1}| · |n_{2}|), where |n| denotes the number of nodes in the ROBDD n). In order to apply the ∧_{D} operator to the smallest possible ROBDD nodes we can use the alternative expression

η(⟨G′_{1} ∪ G′_{2}, L′_{1} ∧_{L} L′_{2}, n′_{1} ∧_{D} n′_{2}⟩),  (2)

where ⟨G′_{i}, L′_{i}, n′_{i}⟩ = η(⟨G_{1} ∪ G_{2}, L_{1} ∧_{L} L_{2}, n_{i}), for i = 1, 2. For lack of space we cannot enter into details, but the current implementation uses an expression which is intermediate between (1) and (2). Indeed, the attentive reader will have noticed that there is a tradeoff in the above motto: keeping the ROBDDs as small as possible, as in (2), implies performing several (possibly fruitless) visits of the ROBDDs in order to collect entailed and equivalent variables.

Disjunction is computationally less complex than conjunction in that it does not require normalization through η. This, however, comes at the price of some extra complication in the definition.

⟨G_{1}, L_{1}, n_{1}⟩ ∨_{G} ⟨G_{2}, L_{2}, n_{2}⟩ =^{def} ⟨G_{1} ∩ G_{2}, L′, n′_{1} ∨_{D} n′_{2}⟩,

with L′ =^{def} L′_{1} ∨_{L} L′_{2} and

L′_{1} =^{def} L_{1} ∧_{L} _{⋀_{L}} ; {(x,y)∈G_{1}\G_{2} \atop x≺y} \{(x, y)\},  L′_{2} =^{def} L_{2} ∧_{L} _{⋀_{L}} ; {(x,y)∈G_{2}\G_{1} \atop x≺y} \{(x, y)\},

G′_{1} =^{def} { λ_{L′}(x) | x ∈ G_{1} \ G_{2} },  G′_{2} =^{def} { λ_{L′}(x) | x ∈ G_{2} \ G_{1} },
L′′_{1} =^{def} (L′_{1} \ L′_{2}) ∨_{L} L_{1},  L′′_{2} =^{def} (L′_{2} \ L′_{1}) ∨_{L} L_{2},
n′_{1} =^{def} n_{1} ∧_{D} \begin{matrix}⋀ & _{D} \\ x∈G′_{1} \end{matrix} x ∧_{D} \begin{matrix}⋀ & _{D} \\ (x,y)∈L′′_{1} \end{matrix} x ↔ y, n′_{2} =^{def} n_{2} ∧_{D} \begin{matrix}⋀ & _{D} \\ x∈G′_{2} \end{matrix} x ∧_{D} \begin{matrix}⋀ & _{D} \\ (x,y)∈L′′_{2} \end{matrix} x ↔ y.

For i = 1, 2, L′_{i} contains the equivalent variables in L_{i} plus those implied by the groundness not shared by the two representations that are about to be disjoined (since x ∧ y implies x ↔ y). Thus L′ contains the common equivalent pairs. For i = 1, 2, G′_{i} contains the non-common ground variables to be restored into the ROBDD components, taking into account the common equivalences. Similarly, L′′_{i} contains the non-common equivalences to be restored into the respective ROBDD: notice that, for x, y ∈ G_{i} \ G_{(imod2)+1}, care is taken not to restore both x ∧ y and x ↔ y.

For the projection operation over G, which is indeed quite simple, we refer the reader to [4].

4 Some Specialized Algorithms

In order to implement the normalize function, its specializations, and the other operations for the analysis, we need efficient algorithms for several operations. Algorithms for finding all the variables entailed in an ROBDD have been presented in [2, 15], while the operation n[1/V] (called valuation or co-factoring) can be easily implemented as described in [7].

4.1 Finding Equivalent Variables in ROBDDs

An algorithm for finding all the pairs of variables in an ROBDD that are equivalent is presented as Alg. 2. The algorithm follows directly from the following

Require: an ROBDD node n function equiv vars(n) equiv vars aux(n, {⟨x, y⟩ : α ⪯ x ≺ y ⪯ max vars(n)})

function equiv vars aux(n, U)

if n = 1 then

∅ else if n = 0 then

U else

{ ⟨n_{var}, v⟩ | v ∈ (vars entailed(n_{true}) ∩ vars disentailed(n_{false})) }

∪(equiv vars aux(n_{true}, U) ∩ equiv vars aux(n_{false}, U))

Algorithm 2: The equiv vars function.

theorem.

Theorem 2. ⟦n⟧_{D} entails x ↔ y where x ≺ y if and only if n = 0, or n_{var} = x and ⟦n_{true}⟧_{D} entails y and ⟦n_{false}⟧_{D} disentails y, or n_{var} ≺ x and ⟦n_{true}⟧_{D} and ⟦n_{false}⟧_{D} both entail x ↔ y.

We refer the reader to [2, 15] for the possible implementations of vars entailed (and, by duality, of vars disentailed). Observe that a crucial ingredient for the efficiency of the implementation is caching the results of the calls to equiv vars, vars entailed, and vars disentailed.

4.2 Removing Equivalent Variables

Once we have identified which variables are equivalent to which others, we can significantly reduce the size of an ROBDD by removing all but one of each equivalence class of variables. Defining the leader function for an ROBDD node n as

λ_{n} =^{def} λ_{equiv(n)},

our aim is to restrict away all but the first variable in each equivalence class, that is, all variables v such that λ_{n}(v) ≠ v. To motivate the algorithm, we begin with a simple theorem.

Theorem 3. Given an ROBDD rooted at n, and its corresponding leader function λ_{n}, for every node m ≠ n appearing in the ROBDD such that λ_{n}(m_{var}) = n_{var}, either m_{true} = 0 or m_{false} = 0.

We “remove” a variable from a Boolean function using existential quantification. For an ROBDD node m, removing m_{var} leaves disjoin(m_{true}, m_{false}). So Theorem 3 tells us that when λ_{n}(m_{var}) ≠ m_{var}, either m_{true} or m_{false} will be 0, making the disjunction trivial.

This suggests the algorithm shown as Algorithm 3 for removing all the “unneeded” variables in an ROBDD n given its leader function λ_{n}. Two obvious optimizations of this algorithm immediately suggest themselves. Firstly, we may easily compute the last variable (in the ordering) z such that λ_{n}(z) ≠ z; we may then add the case else if n_{var} > z then n immediately after the initial if. The second and more important optimization is to avoid recomputing the squeeze equiv function by the usual caching technique, returning the result of an earlier call with the same arguments. Since the λ_{n} function is the same in all recursive calls to squeeze equiv, we may simplify this by clearing our table of previous results whenever squeeze equiv is called non-recursively (from outside). This allows us to use only the n argument as a parameter to this cache.

When we conjoin two Boolean functions in their GER representation, we also have the opportunity to use the variable equivalences of each argument to reduce the size of the ROBDD component of the other argument. In order to do this, we need an algorithm to compute, given any ROBDD m and equivalent variable set L, the ROBDD n whose semantics is

⟦n⟧_{D} = ∃L|2 . ⟦L⟧_{L} ∧ ⟦m⟧_{D}.

Space limitations preclude a full exposition of this algorithm, but it may be found in [4].

Require: an ROBDD node n and a leader function λ function squeeze equiv(n, λ) if is terminal(n) then

n else if λ(n_{var}) = n_{var} then

make node(n_{var}, squeeze equiv(n_{true}, λ), squeeze equiv(n_{false}, λ)) else if n_{true} = 0 then

squeeze equiv(n_{false}, λ) else

squeeze equiv(n_{true}, λ)

Algorithm 3: The squeeze equiv function.

5 Experimental Evaluation

The ideas presented in this section have been experimentally validated in the context of the development of the China analyzer [3]. China is a data-flow analyzer for CLP(H_{N}) languages (i.e., Prolog, CLP(R), clp(FD) and so forth) written in C^{++} and Prolog. It performs bottom-up analysis deriving information about success-patterns and, optionally, call-patterns by means of program transformations and optimized fixpoint computation techniques. We have performed the analysis of a suite comprising 170 programs on the domain Pattern(Pos) (similar to Pat(Pos) [3]), switching off all the other domains currently supported by China^{2}, and switching off the widening operations normally used to throttle the complexity of the analysis.

A selection of the experimental results is reported in Tables 1 and 2. These tables give, for each program, the analysis times and the number of ROBDD nodes allocated for the standard implementation based on ROBDDs only, but making use of the optimized algorithms described in [15] (R), for the implementation where definitely ground variables are factored out from the ROBDDs as explained in [2] (GR), and for the implementation based on the ideas presented in this paper (GER). The analysis has been considered impractical (and thus stopped) as soon as the amount of memory used by China exceeded 16 MB (for medium sized programs this corresponds to roughly 320.000 ROBDD nodes). This is indicated by ∞ in Table 1 and by ✠ in Table 2.

The computation times have been taken on a Pentium II machine clocked at 233MHz, with 64 MB of RAM, and running Linux 2.0.32.

As it can be seen from the tables, the proposed technique improves the stateof-the-art of groundness analysis with Pattern(Pos) considerably. Programs that were out of reach for previous implementations are now analyzable in reasonable time, while for most other programs the measured speedup is between a factor of 2 and an order of magnitude. As far as the the memory requirements of the analysis are concerned, the new representation allows for big savings, as indicated by Table 2. Comparing the results with those of [8, page 45], and

2 Namely, numerical bounds and relations, aliasing, freeness, and polymorphic types.

Goal independent Goal dependent
Program  R GR GER R GR GER
action.pl  1.59 1.58 0.17 3.21 2.78 1.44
bp0-6.pl  0.18 0.09 0.04 0.18 0.06 0.07
bridge.clpr  0.3 0.33 0.11 0.1 0.02 0.02

chat parser.pl  ∞ ∞ 0.54 ∞ ∞ 2.11

critical.clpr  0.18 0.17 0.03 ∞ ∞ 0.14
cs2.pl  0.11 0.09 0.04 0.08 0.03 0.04
csg.clpr  0.11 0.11 0.01 0.06 0.04 0.02
ime v2-2-1.pl  0.28 0.19 0.08 0.53 0.2 0.12
kalah.pl  0.23 0.1 0.05 0.24 0.09 0.12
log interpreter.pl 0.51 0.43 0.17 2.95 2.56 0.6
peval.pl  0.87 0.73 0.31 1.97 1.58 0.55
read.pl  0.41 0.16 0.1 0.76 0.54 0.24
reducer.pl  0.11 0.1 0.07 0.9 0.83 0.25
rubik.pl  ∞ ∞ 0.13 ∞ ∞ 0.64
scc.pl  ∞ ∞ 0.62 1.04 0.15 0.14
sdda.pl  0.11 0.09 0.03 1.94 1.47 0.16
sim v5-2.pl  0.24 0.21 0.19 0.37 0.25 0.29

simple analyzer.pl ∞ ∞ 0.16 ∞ ∞ 4.2

unify.pl  1.39 0.66 0.14 ∞ ∞ 0.78

Table 1. Results obtained with China: analysis time in seconds.

Goal independent  Goal dependent
Program R GR GER R GR GER
action.pl  228913 228027 6301 186745 173167 20861
bp0-6.pl  33838 12694 2016 12162 1219 103
bridge.clpr  14765 14762 6324 4044 3243 2174
chat parser.pl         ✠  ✠ 17291  ✠  ✠ 26634
critical.clpr  14824 14284 1893  ✠  ✠ 7846
cs2.pl  16044 11359 1698 4425 214 64
csg.clpr 317 106 23 196 30 27
ime v2-2-1.pl  42088 21210 3336 59203 20693 2634
kalah.pl  42008 10962 2253 8487 322 114
log interpreter.pl 61249 50083 3070 213388 167080 9354
peval.pl  96883 75218 14256 190905 147545 20357
read.pl  49710 14883 2108 55804 32764 3095
reducer.pl  13534 11542 2435 92485 87306 7317
rubik.pl               ✠  ✠ 3825  ✠  ✠ 5261
scc.pl                 ✠  ✠ 16751 82788 5762 215
sdda.pl  19561 14360 786 201732 157191 2798
sim v5-2.pl  18600 13073 4969 5958 319 120

simple analyzer.pl     ✠  ✠ 6772  ✠  ✠ 65125

unify.pl  188476 94923 9569  ✠  ✠ 25679

Table 2. Results obtained with China: number of BDD nodes.

scaling the timings in order to account for the difference in performance between a Pentium-II at 233MHz and a Sun SparcStation 10/30, it can be seen that we have significantly pushed forward the practicality of Pos.

It is worth noticing that while the analyses based on Pattern(Pos) are computationally more complex than those simply based on Pos (Cortesi et al. measured a slowdown of around 20), they are also significantly more precise [8].

6 Conclusion

We have studied the problem of efficient dependency analysis, and in particular groundness analysis, of (constraint) logic programs, using the Pos domain. As others have concluded that ROBDDs are the most efficient representation for use in this sort of analysis, we have concentrated on improving the efficiency of the operations needed during program analysis for ROBDDs. However, since many ROBDD operations have super-linear time cost, we sought to reduce the size of the ROBDDs being manipulated by removing certain information from the ROBDDs and representing it in a way specialized to its nature. We remove definite variables as in [2], storing them in a bit vector. The main accomplishment of this work, however, has been to remove all pairs of equivalent variables, storing them as an array of variable numbers. We have shown how this new hybrid representation significantly decreases the size of the ROBDDs being manipulated. More importantly, analysis times are significantly improved beyond the significant speedup achieved in [2].

References

[1] T. Armstrong, K. Marriott, P. Schachte, and H. Søndergaard. Two classes of Boolean functions for dependency analysis. Science of Computer Programming, 31(1):3–45, 1998.

[2] R. Bagnara. A reactive implementation of Pos using ROBDDs. In H. Kuchen and S. D. Swierstra, editors, Programming Languages: Implementations, Logics and Programs, Proceedings of the Eighth International Symposium, volume 1140 of Lecture Notes in Computer Science, pages 107– 121, Aachen, Germany, 1996. Springer-Verlag, Berlin.

[3] R. Bagnara. Data-Flow Analysis for Constraint Logic-Based Languages. PhD thesis, Dipartimento di Informatica, Università di Pisa, Corso Italia 40, I-56125 Pisa, Italy, March 1997. Printed as Report TD-1/97.

[4] R. Bagnara and P. Schachte. Efficient implementation of Pos. Technical Report 98/5, Department of Computer Science, The University of Melbourne, Australia, 1998.

[5] P. Bigot, S. K. Debray, and K. Marriott. Understanding finiteness analysis using abstract interpretation. In K. Apt, editor, Logic Programming: Proceedings of the Joint International Conference and Symposium on Logic Programming, MIT Press Series in Logic Programming, pages 735–749, Washington, USA, 1992. The MIT Press.

[6] R. E. Bryant. Graph-based algorithms for Boolean function manipulation. IEEE Transactions on Computers, C-35(8):677–691, August 1986.

[7] R. E. Bryant. Symbolic boolean manipulation with ordered binary-decision diagrams. ACM Computing Surveys, 24(3):293–318, September 1992.

[8] A. Cortesi, B. Le Charlier, and P. Van Hentenryck. Conceptual and software support for abstract domain design: Generic structural domain and open product. Technical Report CS-93-13, Brown University, Providence, RI, 1993.

[9] A. Cortesi, B. Le Charlier, and P. Van Hentenryck. Combinations of abstract domains for logic programming. In Conference Record of POPL ’94: 21st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pages 227–239, Portland, Oregon, 1994.

[10] P. W. Dart. Dependency Analysis and Query Interfaces for Deductive Databases. PhD thesis, The University of Melbourne, Department of Computer Science, 1988. Printed as Technical Report 88/35.

[11] M. Falaschi, M. Gabbrielli, K. Marriott, and C. Palamidessi. Confluence and concurrent constraint programming. In V. S. Alagar and M. Nivat, editors, Proceedings of the Fourth International Conference on Algebraic Methodology and Software Technology (AMAST’95), volume 936 of Lecture Notes in Computer Science, pages 531–545. Springer-Verlag, Berlin, 1995.

[12] N. D. Jones and H. Søndergaard. A semantics-based framework for the abstract interpretation of Prolog. In S. Abramsky and C. Hankin, editors, Abstract Interpretation of Declarative Languages, chapter 6, pages 123–142. Ellis Horwood Ltd, West Sussex, England, 1987.

[13] K. Marriott and H. Søndergaard. Notes for a tutorial on abstract interpretation of logic programs. North American Conference on Logic Programming, Cleveland, Ohio, USA, 1989.

[14] C. S. Mellish. Some global optimizations for a Prolog compiler. Journal of Logic Programming, 2(1):43–66, 1985.

[15] P. Schachte. Efficient ROBDD operations for program analysis. In K. Ramamohanarao, editor, ACSC’96: Proceedings of the 19th Australasian Computer Science Conference, pages 347–356. Australian Computer Science Communications, 1996.

[16] H. Søndergaard. Immediate fixpoints and their use in groundness analysis. In V. Chandru and V. Vinay, editors, Foundations of Software Technology and Theoretical Computer Science, volume 1180 of Lecture Notes in Computer Science, pages 359–370. Springer-Verlag, Berlin, 1996.

[17] J. Zobel. Analysis of Logic Programs. PhD thesis, The University of Melbourne, 1990.