1 /**CFile***********************************************************************
3 FileName [cuddInteract.c]
7 Synopsis [Functions to manipulate the variable interaction matrix.]
9 Description [Internal procedures included in this file:
11 <li> cuddSetInteract()
12 <li> cuddTestInteract()
13 <li> cuddInitInteract()
15 Static procedures included in this file:
19 <li> ddUpdateInteract()
22 The interaction matrix tells whether two variables are
23 both in the support of some function of the DD. The main use of the
24 interaction matrix is in the in-place swapping. Indeed, if two
25 variables do not interact, there is no arc connecting the two layers;
26 therefore, the swap can be performed in constant time, without
27 scanning the subtables. Another use of the interaction matrix is in
28 the computation of the lower bounds for sifting. Finally, the
29 interaction matrix can be used to speed up aggregation checks in
30 symmetric and group sifting.<p>
31 The computation of the interaction matrix is done with a series of
32 depth-first searches. The searches start from those nodes that have
33 only external references. The matrix is stored as a packed array of bits;
34 since it is symmetric, only the upper triangle is kept in memory.
35 As a final remark, we note that there may be variables that do
36 intercat, but that for a given variable order have no arc connecting
37 their layers when they are adjacent.]
41 Author [Fabio Somenzi]
43 Copyright [Copyright (c) 1995-2004, Regents of the University of Colorado
47 Redistribution and use in source and binary forms, with or without
48 modification, are permitted provided that the following conditions
51 Redistributions of source code must retain the above copyright
52 notice, this list of conditions and the following disclaimer.
54 Redistributions in binary form must reproduce the above copyright
55 notice, this list of conditions and the following disclaimer in the
56 documentation and/or other materials provided with the distribution.
58 Neither the name of the University of Colorado nor the names of its
59 contributors may be used to endorse or promote products derived from
60 this software without specific prior written permission.
62 THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS
63 "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT
64 LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS
65 FOR A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE
66 COPYRIGHT OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT,
67 INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING,
68 BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES;
69 LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER
70 CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT
71 LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN
72 ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE
73 POSSIBILITY OF SUCH DAMAGE.]
75 ******************************************************************************/
80 /*---------------------------------------------------------------------------*/
81 /* Constant declarations */
82 /*---------------------------------------------------------------------------*/
92 /*---------------------------------------------------------------------------*/
93 /* Stucture declarations */
94 /*---------------------------------------------------------------------------*/
97 /*---------------------------------------------------------------------------*/
98 /* Type declarations */
99 /*---------------------------------------------------------------------------*/
102 /*---------------------------------------------------------------------------*/
103 /* Variable declarations */
104 /*---------------------------------------------------------------------------*/
107 static char rcsid
[] DD_UNUSED
= "$Id: cuddInteract.c,v 1.12 2004/08/13 18:04:49 fabio Exp $";
110 /*---------------------------------------------------------------------------*/
111 /* Macro declarations */
112 /*---------------------------------------------------------------------------*/
115 /**AutomaticStart*************************************************************/
117 /*---------------------------------------------------------------------------*/
118 /* Static function prototypes */
119 /*---------------------------------------------------------------------------*/
121 static void ddSuppInteract (DdNode
*f
, int *support
);
122 static void ddClearLocal (DdNode
*f
);
123 static void ddUpdateInteract (DdManager
*table
, int *support
);
124 static void ddClearGlobal (DdManager
*table
);
126 /**AutomaticEnd***************************************************************/
129 /*---------------------------------------------------------------------------*/
130 /* Definition of exported functions */
131 /*---------------------------------------------------------------------------*/
134 /*---------------------------------------------------------------------------*/
135 /* Definition of internal functions */
136 /*---------------------------------------------------------------------------*/
139 /**Function********************************************************************
141 Synopsis [Set interaction matrix entries.]
143 Description [Given a pair of variables 0 <= x < y < table->size,
144 sets the corresponding bit of the interaction matrix to 1.]
150 ******************************************************************************/
161 assert(y
< table
->size
);
165 posn
= ((((table
->size
<< 1) - x
- 3) * x
) >> 1) + y
- 1;
166 word
= posn
>> LOGBPL
;
167 bit
= posn
& (BPL
-1);
168 table
->interact
[word
] |= 1L << bit
;
170 } /* end of cuddSetInteract */
173 /**Function********************************************************************
175 Synopsis [Test interaction matrix entries.]
177 Description [Given a pair of variables 0 <= x < y < table->size,
178 tests whether the corresponding bit of the interaction matrix is 1.
179 Returns the value of the bit.]
185 ******************************************************************************/
192 int posn
, word
, bit
, result
;
201 assert(y
< table
->size
);
205 posn
= ((((table
->size
<< 1) - x
- 3) * x
) >> 1) + y
- 1;
206 word
= posn
>> LOGBPL
;
207 bit
= posn
& (BPL
-1);
208 result
= (table
->interact
[word
] >> bit
) & 1L;
211 } /* end of cuddTestInteract */
214 /**Function********************************************************************
216 Synopsis [Initializes the interaction matrix.]
218 Description [Initializes the interaction matrix. The interaction
219 matrix is implemented as a bit vector storing the upper triangle of
220 the symmetric interaction matrix. The bit vector is kept in an array
221 of long integers. The computation is based on a series of depth-first
222 searches, one for each root of the DAG. Two flags are needed: The
223 local visited flag uses the LSB of the then pointer. The global
224 visited flag uses the LSB of the next pointer.
225 Returns 1 if successful; 0 otherwise.]
231 ******************************************************************************/
241 DdNode
*sentinel
= &(table
->sentinel
);
246 words
= ((n
* (n
-1)) >> (1 + LOGBPL
)) + 1;
247 table
->interact
= interact
= ALLOC(long,words
);
248 if (interact
== NULL
) {
249 table
->errorCode
= CUDD_MEMORY_OUT
;
252 for (i
= 0; i
< words
; i
++) {
256 support
= ALLOC(int,n
);
257 if (support
== NULL
) {
258 table
->errorCode
= CUDD_MEMORY_OUT
;
263 for (i
= 0; i
< n
; i
++) {
264 nodelist
= table
->subtables
[i
].nodelist
;
265 slots
= table
->subtables
[i
].slots
;
266 for (j
= 0; j
< slots
; j
++) {
268 while (f
!= sentinel
) {
269 /* A node is a root of the DAG if it cannot be
270 ** reached by nodes above it. If a node was never
271 ** reached during the previous depth-first searches,
272 ** then it is a root, and we start a new depth-first
275 if (!Cudd_IsComplement(f
->next
)) {
276 for (k
= 0; k
< n
; k
++) {
279 ddSuppInteract(f
,support
);
281 ddUpdateInteract(table
,support
);
283 f
= Cudd_Regular(f
->next
);
287 ddClearGlobal(table
);
292 } /* end of cuddInitInteract */
295 /*---------------------------------------------------------------------------*/
296 /* Definition of static functions */
297 /*---------------------------------------------------------------------------*/
300 /**Function********************************************************************
302 Synopsis [Find the support of f.]
304 Description [Performs a DFS from f. Uses the LSB of the then pointer
307 SideEffects [Accumulates in support the variables on which f depends.]
311 ******************************************************************************/
317 if (cuddIsConstant(f
) || Cudd_IsComplement(cuddT(f
))) {
321 support
[f
->index
] = 1;
322 ddSuppInteract(cuddT(f
),support
);
323 ddSuppInteract(Cudd_Regular(cuddE(f
)),support
);
324 /* mark as visited */
325 cuddT(f
) = Cudd_Complement(cuddT(f
));
326 f
->next
= Cudd_Complement(f
->next
);
329 } /* end of ddSuppInteract */
332 /**Function********************************************************************
334 Synopsis [Performs a DFS from f, clearing the LSB of the then pointers.]
342 ******************************************************************************/
347 if (cuddIsConstant(f
) || !Cudd_IsComplement(cuddT(f
))) {
350 /* clear visited flag */
351 cuddT(f
) = Cudd_Regular(cuddT(f
));
352 ddClearLocal(cuddT(f
));
353 ddClearLocal(Cudd_Regular(cuddE(f
)));
356 } /* end of ddClearLocal */
359 /**Function********************************************************************
361 Synopsis [Marks as interacting all pairs of variables that appear in
364 Description [If support[i] == support[j] == 1, sets the (i,j) entry
365 of the interaction matrix to 1.]
371 ******************************************************************************/
380 for (i
= 0; i
< n
-1; i
++) {
381 if (support
[i
] == 1) {
382 for (j
= i
+1; j
< n
; j
++) {
383 if (support
[j
] == 1) {
384 cuddSetInteract(table
,i
,j
);
390 } /* end of ddUpdateInteract */
393 /**Function********************************************************************
395 Synopsis [Scans the DD and clears the LSB of the next pointers.]
397 Description [The LSB of the next pointers are used as markers to tell
398 whether a node was reached by at least one DFS. Once the interaction
399 matrix is built, these flags are reset.]
405 ******************************************************************************/
412 DdNode
*sentinel
= &(table
->sentinel
);
416 for (i
= 0; i
< table
->size
; i
++) {
417 nodelist
= table
->subtables
[i
].nodelist
;
418 slots
= table
->subtables
[i
].slots
;
419 for (j
= 0; j
< slots
; j
++) {
421 while (f
!= sentinel
) {
422 f
->next
= Cudd_Regular(f
->next
);
428 } /* end of ddClearGlobal */