source: icGREP/icgrep-devel/cudd-2.5.1/nanotrav/ntrShort.c @ 5815

Last change on this file since 5815 was 4597, checked in by nmedfort, 4 years ago

Upload of the CUDD library.

File size: 17.9 KB
Line 
1/**CFile***********************************************************************
2
3  FileName    [ntrShort.c]
4
5  PackageName [ntr]
6
7  Synopsis    [Symbolic shortest paths algorithms.]
8
9  Description [This file contains the functions that implement the
10  symbolic version of several shortest path algorithms described in the
11  JFM paper on ADDs.]
12
13  Author      [Fabio Somenzi, Iris Bahar]
14
15  Copyright   [Copyright (c) 1995-2012, Regents of the University of Colorado
16
17  All rights reserved.
18
19  Redistribution and use in source and binary forms, with or without
20  modification, are permitted provided that the following conditions
21  are met:
22
23  Redistributions of source code must retain the above copyright
24  notice, this list of conditions and the following disclaimer.
25
26  Redistributions in binary form must reproduce the above copyright
27  notice, this list of conditions and the following disclaimer in the
28  documentation and/or other materials provided with the distribution.
29
30  Neither the name of the University of Colorado nor the names of its
31  contributors may be used to endorse or promote products derived from
32  this software without specific prior written permission.
33
34  THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS
35  "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT
36  LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS
37  FOR A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE
38  COPYRIGHT OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT,
39  INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING,
40  BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES;
41  LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER
42  CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT
43  LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN
44  ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE
45  POSSIBILITY OF SUCH DAMAGE.]
46
47******************************************************************************/
48
49#include "ntr.h"
50#include "cuddInt.h"
51
52/*---------------------------------------------------------------------------*/
53/* Constant declarations                                                     */
54/*---------------------------------------------------------------------------*/
55
56/*---------------------------------------------------------------------------*/
57/* Stucture declarations                                                     */
58/*---------------------------------------------------------------------------*/
59
60/*---------------------------------------------------------------------------*/
61/* Type declarations                                                         */
62/*---------------------------------------------------------------------------*/
63
64/*---------------------------------------------------------------------------*/
65/* Variable declarations                                                     */
66/*---------------------------------------------------------------------------*/
67
68#ifndef lint
69static char rcsid[] UTIL_UNUSED = "$Id: ntrShort.c,v 1.5 2012/02/05 01:53:01 fabio Exp fabio $";
70#endif
71
72/*---------------------------------------------------------------------------*/
73/* Macro declarations                                                        */
74/*---------------------------------------------------------------------------*/
75
76/**AutomaticStart*************************************************************/
77
78/*---------------------------------------------------------------------------*/
79/* Static function prototypes                                                */
80/*---------------------------------------------------------------------------*/
81
82static DdNode * ntrBellman (DdManager *dd, DdNode *D, DdNode *source, DdNode **x, DdNode **y, int vars, int pr);
83static DdNode * ntrWarshall (DdManager *dd, DdNode *D, DdNode **x, DdNode **y, int vars, int pr);
84static DdNode * ntrSquare (DdManager *dd, DdNode *D, DdNode **x, DdNode **y, DdNode **z, int vars, int pr, int st);
85
86/**AutomaticEnd***************************************************************/
87
88/*---------------------------------------------------------------------------*/
89/* Definition of exported functions                                          */
90/*---------------------------------------------------------------------------*/
91
92/**Function********************************************************************
93
94  Synopsis    [Computes shortest paths in a state graph.]
95
96  Description [Computes shortest paths in the state transition graph of
97  a network.  Three methods are availabe:
98  <ul>
99  <li> Bellman-Ford algorithm for single-source shortest paths; the
100  algorithm computes the distance (number of transitions) from the initial
101  states to all states.
102  <li> Floyd-Warshall algorithm for all-pair shortest paths.
103  <li> Repeated squaring algorithm for all-pair shortest paths.
104  </ul>
105  The function returns 1 in case of success; 0 otherwise.
106  ]
107
108  SideEffects [ADD variables are created in the manager.]
109
110  SeeAlso     []
111
112******************************************************************************/
113int
114Ntr_ShortestPaths(
115  DdManager * dd,
116  BnetNetwork * net,
117  NtrOptions * option)
118{
119    NtrPartTR *TR;
120    DdNode *edges, *source, *res, *r, *q, *bddSource;
121    DdNode **xadd, **yadd, **zadd;
122    int i;
123    int pr = option->verb;
124    int algorithm = option->shortPath;
125    int selectiveTrace = option->selectiveTrace;
126    int nvars = net->nlatches;
127
128    /* Set background to infinity for shortest paths. */
129    Cudd_SetBackground(dd,Cudd_ReadPlusInfinity(dd));
130
131    /* Build the monolithic TR. */
132    TR = Ntr_buildTR(dd,net,option,NTR_IMAGE_MONO);
133
134    /* Build the ADD variable vectors for x and y. */
135    xadd = ALLOC(DdNode *, nvars);
136    yadd = ALLOC(DdNode *, nvars);
137    for(i = 0; i < nvars; i++) {
138        q = Cudd_addIthVar(dd,TR->x[i]->index);
139        Cudd_Ref(q);
140        xadd[i] = q;
141        q = Cudd_addIthVar(dd,TR->y[i]->index);
142        Cudd_Ref(q);
143        yadd[i] = q;
144    }
145
146    /* Convert the transition relation BDD into an ADD... */
147    q = Cudd_BddToAdd(dd,TR->part[0]);
148    Cudd_Ref(q);
149    /* ...replacing zeroes with infinities... */
150    r = Cudd_addIte(dd,q,Cudd_ReadOne(dd),Cudd_ReadPlusInfinity(dd));
151    Cudd_Ref(r);
152    Cudd_RecursiveDeref(dd,q);
153    /* ...and zeroing the diagonal. */
154    q = Cudd_addXeqy(dd,nvars,xadd,yadd);
155    Cudd_Ref(q);
156    edges = Cudd_addIte(dd,q,Cudd_ReadZero(dd),r);
157    Cudd_Ref(edges);
158    Cudd_RecursiveDeref(dd,r);
159    Cudd_RecursiveDeref(dd,q);
160
161    switch(algorithm) {
162    case NTR_SHORT_BELLMAN:
163        bddSource = Ntr_initState(dd,net,option);
164        source = Cudd_BddToAdd(dd,bddSource);
165        Cudd_Ref(source);
166        res = ntrBellman(dd,edges,source,xadd,yadd,nvars,pr);
167        if (res == NULL) return(0);
168        Cudd_Ref(res);
169        Cudd_RecursiveDeref(dd,source);
170        Cudd_RecursiveDeref(dd,bddSource);
171        if (pr >= 0) {
172            (void) fprintf(stdout,"Distance Matrix");
173            Cudd_PrintDebug(dd,res,nvars,pr);
174        }
175        break;
176    case NTR_SHORT_FLOYD:
177        res = ntrWarshall(dd,edges,xadd,yadd,nvars,pr);
178        if (res == NULL) return(0);
179        Cudd_Ref(res);
180        if (pr >= 0) {
181            (void) fprintf(stdout,"Distance Matrix");
182            Cudd_PrintDebug(dd,res,2*nvars,pr);
183        }
184        break;
185    case NTR_SHORT_SQUARE:
186        /* Create a third set of ADD variables. */
187        zadd = ALLOC(DdNode *, nvars);
188        for(i = 0; i < nvars; i++) {
189            int level;
190            level = Cudd_ReadIndex(dd,TR->x[i]->index);
191            q = Cudd_addNewVarAtLevel(dd,level);
192            Cudd_Ref(q);
193            zadd[i] = q;
194        }
195        /* Compute the shortest paths. */
196        res = ntrSquare(dd,edges,zadd,yadd,xadd,nvars,pr,selectiveTrace);
197        if (res == NULL) return(0);
198        Cudd_Ref(res);
199        /* Dispose of the extra variables. */
200        for(i = 0; i < nvars; i++) {
201            Cudd_RecursiveDeref(dd,zadd[i]);
202        }
203        FREE(zadd);
204        if (pr >= 0) {
205            (void) fprintf(stdout,"Distance Matrix");
206            Cudd_PrintDebug(dd,res,2*nvars,pr);
207        }
208        break;
209    default:
210        (void) printf("Unrecognized method. Try again.\n");
211        return(0);
212    }
213
214    /* Here we should compute the paths. */
215
216    /* Clean up. */
217    Ntr_freeTR(dd,TR);
218    Cudd_RecursiveDeref(dd,edges);
219    Cudd_RecursiveDeref(dd,res);
220    for(i = 0; i < nvars; i++) {
221        Cudd_RecursiveDeref(dd,xadd[i]);
222        Cudd_RecursiveDeref(dd,yadd[i]);
223    }
224    FREE(xadd);
225    FREE(yadd);
226
227    if (option->autoDyn & 1) {
228        (void) printf("Order after short path computation\n");
229        if (!Bnet_PrintOrder(net,dd)) return(0);
230    }
231
232    return(1);
233
234} /* end of Ntr_ShortestPaths */
235
236
237/*---------------------------------------------------------------------------*/
238/* Definition of internal functions                                          */
239/*---------------------------------------------------------------------------*/
240
241/*---------------------------------------------------------------------------*/
242/* Definition of static functions                                            */
243/*---------------------------------------------------------------------------*/
244
245
246/**Function********************************************************************
247
248  Synopsis    [Bellman-Ford algorithm for single-source shortest paths.]
249
250  Description [Bellman-Ford algorithm for single-source shortest
251  paths.  Returns the vector of the distances of all states from the
252  initial states.  In case of multiple initial states the distance for
253  each state is from the nearest initial state.  Negative-weight
254  cycles are detected, though only in the naive way.  (Lack of
255  convergence after nodes-1 iterations.)  In such a case, a constant
256  ADD with value minus infinity is returned.  Bellman-Ford is based on
257  matrix-vector multiplication.  The matrix is the distance matrix
258  D(x,y), such that D(a,b) is the length of the arc connecting state a
259  to state b.  The vector V(x) stores the distances of all states from
260  the initial states.  The actual vector used in the matrix-vector
261  multiplication is diff(x), that holds those distances that have
262  changed during the last update.]
263
264  SideEffects []
265
266  SeeAlso     [ntrWarshall ntrSquare]
267
268******************************************************************************/
269static DdNode *
270ntrBellman(
271  DdManager *dd,
272  DdNode *D,
273  DdNode *source,
274  DdNode **x,
275  DdNode **y,
276  int vars,
277  int pr)
278{
279    DdNode *u, *w, *V, *min, *diff;
280    DdApaNumber i, nodes, one;
281    int digits = vars + 1;
282
283    /* To avoid overflow when there are many variables, use APA. */
284    nodes = Cudd_NewApaNumber(digits);
285    Cudd_ApaPowerOfTwo(digits,nodes,vars);
286    i = Cudd_NewApaNumber(digits);
287    one = Cudd_NewApaNumber(digits);
288    Cudd_ApaSetToLiteral(digits,one,1);
289
290#if 0
291    /* Find the distances from the initial state along paths using one
292    ** arc. */
293    w = Cudd_Cofactor(dd,D,source); /* works only if source is a cube */
294    Cudd_Ref(w);
295    V = Cudd_addSwapVariables(dd,w,x,y,vars);
296    Cudd_Ref(V);
297    Cudd_RecursiveDeref(dd,w);
298#endif
299
300    /* The initial states are at distance 0. The other states are
301    ** initially at infinite distance. */
302    V = Cudd_addIte(dd,source,Cudd_ReadZero(dd),Cudd_ReadPlusInfinity(dd));
303    Cudd_Ref(V);
304
305    /* Selective trace algorithm.  For the next update, only consider the
306    ** nodes whose distance has changed in the last update. */
307    diff = V;
308    Cudd_Ref(diff);
309
310    for (Cudd_ApaSetToLiteral(digits,i,1);
311         Cudd_ApaCompare(digits,i,digits,nodes) < 0;
312         Cudd_ApaAdd(digits,i,one,i)) {
313        if (pr>2) {(void) printf("V"); Cudd_PrintDebug(dd,V,vars,pr);}
314        /* Compute the distances via triangulation as a function of x. */
315        w = Cudd_addTriangle(dd,diff,D,x,vars);
316        Cudd_Ref(w);
317        Cudd_RecursiveDeref(dd,diff);
318        u = Cudd_addSwapVariables(dd,w,x,y,vars);
319        Cudd_Ref(u);
320        Cudd_RecursiveDeref(dd,w);
321        if (pr>2) {(void) printf("u"); Cudd_PrintDebug(dd,u,vars,pr);}
322
323        /* Take the minimum of the previous distances and those just
324        ** computed. */
325        min = Cudd_addApply(dd,Cudd_addMinimum,V,u);
326        Cudd_Ref(min);
327        Cudd_RecursiveDeref(dd,u);
328        if (pr>2) {(void) printf("min"); Cudd_PrintDebug(dd,min,vars,pr);}
329
330        if (V == min) {         /* convergence */
331            Cudd_RecursiveDeref(dd,min);
332            if (pr>0) {
333                (void) printf("Terminating after ");
334                Cudd_ApaPrintDecimal(stdout,digits,i);
335                (void) printf(" iterations\n");
336            }
337            break;
338        }
339        /* Find the distances that decreased. */
340        diff = Cudd_addApply(dd,Cudd_addDiff,V,min);
341        Cudd_Ref(diff);
342        if (pr>2) {(void) printf("diff"); Cudd_PrintDebug(dd,diff,vars,pr);}
343        Cudd_RecursiveDeref(dd,V);
344        V = min;
345    }
346    /* Negative cycle detection. */
347    if (Cudd_ApaCompare(digits,i,digits,nodes) == 0 &&
348        diff != Cudd_ReadPlusInfinity(dd)) {
349        (void) printf("Negative cycle\n");
350        Cudd_RecursiveDeref(dd,diff);
351        Cudd_RecursiveDeref(dd,V);
352        V = Cudd_ReadMinusInfinity(dd);
353        Cudd_Ref(V);
354    }
355
356    Cudd_Deref(V);
357    FREE(i);
358    FREE(nodes);
359    FREE(one);
360    return(V);
361
362} /* end of ntrBellman */
363
364
365/**Function********************************************************************
366
367  Synopsis    [Floyd-Warshall algorithm for all-pair shortest paths.]
368
369  Description []
370
371  SideEffects []
372
373  SeeAlso     []
374
375******************************************************************************/
376static DdNode *
377ntrWarshall(
378  DdManager *dd,
379  DdNode *D,
380  DdNode **x,
381  DdNode **y,
382  int vars,
383  int pr)
384{
385    DdNode *one, *zero;
386    DdNode *xminterm,  *w, *V, *V2;
387    DdNode *P, *R;
388    int i;
389    int nodes;
390    int k,u;
391    long start_time;
392    if (vars > 30)
393        nodes = 1000000000;
394    else
395        nodes = 1 << vars;
396
397    one = DD_ONE(dd);
398    zero = DD_ZERO(dd);
399    Cudd_Ref(R = D);                        /* make copy of original matrix */
400
401    /* Extract pivot row and column from D */
402    start_time = util_cpu_time();
403    for (k = 0; k < nodes; k++) {
404        if (k % 10000 == 0) {
405            (void) printf("Starting iteration  %d  at time %s\n",
406                          k,util_print_time(util_cpu_time() - start_time));
407        }
408        Cudd_Ref(xminterm = one);
409        u = k;
410        for (i = vars-1; i >= 0; i--) {
411            if (u&1) {
412                Cudd_Ref(w = Cudd_addIte(dd,x[i],xminterm,zero));
413            } else {
414                Cudd_Ref(w = Cudd_addIte(dd,x[i],zero,xminterm));
415            }
416            Cudd_RecursiveDeref(dd,xminterm);
417            xminterm = w;
418            u >>= 1;
419        }
420
421        Cudd_Ref(V = Cudd_Cofactor(dd,R,xminterm));
422        Cudd_RecursiveDeref(dd,xminterm);
423        if (pr>2) {(void) printf("V"); Cudd_PrintDebug(dd,V,vars,pr);}
424
425
426        Cudd_Ref(xminterm = one);
427        u = k;
428        for (i = vars-1; i >= 0; i--) {
429            if (u&1) {
430                Cudd_Ref(w = Cudd_addIte(dd,y[i],xminterm,zero));
431            } else {
432                Cudd_Ref(w = Cudd_addIte(dd,y[i],zero,xminterm));
433            }
434            Cudd_RecursiveDeref(dd,xminterm);
435            xminterm = w;
436            u >>= 1;
437        }
438
439        Cudd_Ref(V2 = Cudd_Cofactor(dd,R,xminterm));
440        Cudd_RecursiveDeref(dd,xminterm);
441        if (pr>2) {(void) printf("V2"); Cudd_PrintDebug(dd,V2,vars,pr);}
442
443        Cudd_Ref(P = Cudd_addOuterSum(dd,R,V,V2));
444
445        Cudd_RecursiveDeref(dd,V);
446        Cudd_RecursiveDeref(dd,V2);
447        Cudd_RecursiveDeref(dd,R);
448        R = P;
449        if (pr>2) {(void) printf("R"); Cudd_PrintDebug(dd,R,vars,pr);}
450    }
451
452    Cudd_Deref(R);
453    return(R);
454
455} /* end of ntrWarshall */
456
457
458/**Function********************************************************************
459
460  Synopsis    [Repeated squaring algorithm for all-pairs shortest paths.]
461
462  Description []
463
464  SideEffects []
465
466  SeeAlso     []
467
468******************************************************************************/
469static DdNode *
470ntrSquare(
471  DdManager *dd /* manager */,
472  DdNode *D /* D(z,y): distance matrix */,
473  DdNode **x /* array of x variables */,
474  DdNode **y /* array of y variables */,
475  DdNode **z /* array of z variables */,
476  int vars /* number of variables in each of the three arrays */,
477  int pr /* verbosity level */,
478  int st /* use the selective trace algorithm */)
479{
480    DdNode *zero;
481    DdNode *I;              /* identity matirix */
482    DdNode *w, *V, *P, *M, *R, *RT;
483    DdNode *diff, *min, *minDiag;
484    int n;
485    int neg;
486    long start_time;
487
488    zero = Cudd_ReadZero(dd);
489    /* Make a working copy of the original matrix. */
490    R = D;
491    Cudd_Ref(R);
492    I = Cudd_addXeqy(dd,vars,z,y);    /* identity matrix */
493    Cudd_Ref(I);
494
495    /* Make a copy of the matrix for the selective trace algorithm. */
496    diff = R;
497    Cudd_Ref(diff);
498
499    start_time = util_cpu_time();
500    for (n = vars; n >= 0; n--) {
501        printf("Starting iteration %d at time %s\n",vars-n,
502               util_print_time(util_cpu_time() - start_time));
503
504        /* Check for negative cycles: They are identified by negative
505        ** elements on the diagonal.
506        */
507
508        /* Extract values from the diagonal. */
509        Cudd_Ref(w = Cudd_addIte(dd,I,R,zero));
510        minDiag = Cudd_addFindMin(dd,w);        /* no need to ref */
511        neg = Cudd_V(minDiag) < 0;
512        Cudd_RecursiveDeref(dd,w);
513        if (neg) {
514            Cudd_RecursiveDeref(dd,diff);
515            (void) printf("Negative cycle after %d iterations!\n",vars-n);
516            break;
517        }
518
519        /* Prepare the first operand of matrix multiplication:
520        **   diff(z,y) -> RT(x,y) -> V(x,z)
521        */
522
523        /* RT(x,y) */
524        Cudd_Ref(RT = Cudd_addSwapVariables(dd,diff,x,z,vars));
525        Cudd_RecursiveDeref(dd,diff);
526        /* V(x,z) */
527        Cudd_Ref(V = Cudd_addSwapVariables(dd,RT,y,z,vars));
528        Cudd_RecursiveDeref(dd,RT);
529        if (pr > 0) {
530            double pathcount;
531            (void) printf("V"); Cudd_PrintDebug(dd,V,2*vars,pr);
532            pathcount = Cudd_CountPath(V);
533            (void) printf("Path count = %g\n", pathcount);
534        }
535
536        /* V(x,z) * R(z,y) -> P(x,y) */
537        Cudd_Ref(P = Cudd_addTriangle(dd,V,R,z,vars));
538        Cudd_RecursiveDeref(dd,V);
539        /* P(x,y) => M(z,y) */
540        Cudd_Ref(M = Cudd_addSwapVariables(dd,P,x,z,vars));
541        Cudd_RecursiveDeref(dd,P);
542        if (pr>0) {(void) printf("M"); Cudd_PrintDebug(dd,M,2*vars,pr);}
543
544        /* min(z,y) */
545        Cudd_Ref(min = Cudd_addApply(dd,Cudd_addMinimum,R,M));
546        Cudd_RecursiveDeref(dd,M);
547
548        if (R == min) {
549            Cudd_RecursiveDeref(dd,min);
550            if (pr>0) {printf("Done after %d iterations\n",vars-n+1); }
551            break;
552        }
553        /* diff(z,y) */
554        if (st) {
555            Cudd_Ref(diff = Cudd_addApply(dd,Cudd_addDiff,min,R));
556        } else {
557            Cudd_Ref(diff = min);
558        }
559        Cudd_RecursiveDeref(dd,R);
560        R = min;                  /* keep a copy of matrix at current iter. */
561        if (pr > 0) {
562            double pathcount;
563            (void) printf("R"); Cudd_PrintDebug(dd,R,2*vars,pr);
564            pathcount = Cudd_CountPath(R);
565            (void) printf("Path count = %g\n", pathcount);
566        }
567
568        if (n == 0) {
569            (void) printf("Negative cycle!\n");
570            break;
571        }
572
573    }
574    Cudd_RecursiveDeref(dd,I);
575    Cudd_Deref(R);
576    return(R);
577
578} /* end of ntrSquare */
Note: See TracBrowser for help on using the repository browser.