src/bdd/cudd/cuddMatMult.c File Reference

#include "util_hack.h"
#include "cuddInt.h"
Include dependency graph for cuddMatMult.c:

Go to the source code of this file.

Functions

static DdNode *addMMRecur ARGS ((DdManager *dd, DdNode *A, DdNode *B, int topP, int *vars))
static DdNode *addTriangleRecur ARGS ((DdManager *dd, DdNode *f, DdNode *g, int *vars, DdNode *cube))
static DdNode *cuddAddOuterSumRecur ARGS ((DdManager *dd, DdNode *M, DdNode *r, DdNode *c))
DdNode * Cudd_addMatrixMultiply (DdManager *dd, DdNode *A, DdNode *B, DdNode **z, int nz)
DdNode * Cudd_addTimesPlus (DdManager *dd, DdNode *A, DdNode *B, DdNode **z, int nz)
DdNode * Cudd_addTriangle (DdManager *dd, DdNode *f, DdNode *g, DdNode **z, int nz)
DdNode * Cudd_addOuterSum (DdManager *dd, DdNode *M, DdNode *r, DdNode *c)
static DdNode * addMMRecur (DdManager *dd, DdNode *A, DdNode *B, int topP, int *vars)
static DdNode * addTriangleRecur (DdManager *dd, DdNode *f, DdNode *g, int *vars, DdNode *cube)
static DdNode * cuddAddOuterSumRecur (DdManager *dd, DdNode *M, DdNode *r, DdNode *c)

Variables

static char rcsid[] DD_UNUSED = "$Id: cuddMatMult.c,v 1.1.1.1 2003/02/24 22:23:52 wjiang Exp $"

Function Documentation

static DdNode* addMMRecur ( DdManager *  dd,
DdNode *  A,
DdNode *  B,
int  topP,
int *  vars 
) [static]

Function********************************************************************

Synopsis [Performs the recursive step of Cudd_addMatrixMultiply.]

Description [Performs the recursive step of Cudd_addMatrixMultiply. Returns a pointer to the result if successful; NULL otherwise.]

SideEffects [None]

Definition at line 302 of file cuddMatMult.c.

00308 {
00309     DdNode *zero,
00310            *At,         /* positive cofactor of first operand */
00311            *Ae,         /* negative cofactor of first operand */
00312            *Bt,         /* positive cofactor of second operand */
00313            *Be,         /* negative cofactor of second operand */
00314            *t,          /* positive cofactor of result */
00315            *e,          /* negative cofactor of result */
00316            *scaled,     /* scaled result */
00317            *add_scale,  /* ADD representing the scaling factor */
00318            *res;
00319     int i;              /* loop index */
00320     double scale;       /* scaling factor */
00321     int index;          /* index of the top variable */
00322     CUDD_VALUE_TYPE value;
00323     unsigned int topA, topB, topV;
00324     DdNode *(*cacheOp)(DdManager *, DdNode *, DdNode *);
00325 
00326     statLine(dd);
00327     zero = DD_ZERO(dd);
00328 
00329     if (A == zero || B == zero) {
00330         return(zero);
00331     }
00332 
00333     if (cuddIsConstant(A) && cuddIsConstant(B)) {
00334         /* Compute the scaling factor. It is 2^k, where k is the
00335         ** number of summation variables below the current variable.
00336         ** Indeed, these constants represent blocks of 2^k identical
00337         ** constant values in both A and B.
00338         */
00339         value = cuddV(A) * cuddV(B);
00340         for (i = 0; i < dd->size; i++) {
00341             if (vars[i]) {
00342                 if (dd->perm[i] > topP) {
00343                     value *= (CUDD_VALUE_TYPE) 2;
00344                 }
00345             }
00346         }
00347         res = cuddUniqueConst(dd, value);
00348         return(res);
00349     }
00350 
00351     /* Standardize to increase cache efficiency. Clearly, A*B != B*A
00352     ** in matrix multiplication. However, which matrix is which is
00353     ** determined by the variables appearing in the ADDs and not by
00354     ** which one is passed as first argument.
00355     */
00356     if (A > B) {
00357         DdNode *tmp = A;
00358         A = B;
00359         B = tmp;
00360     }
00361 
00362     topA = cuddI(dd,A->index); topB = cuddI(dd,B->index);
00363     topV = ddMin(topA,topB);
00364 
00365     cacheOp = (DdNode *(*)(DdManager *, DdNode *, DdNode *)) addMMRecur;
00366     res = cuddCacheLookup2(dd,cacheOp,A,B);
00367     if (res != NULL) {
00368         /* If the result is 0, there is no need to normalize.
00369         ** Otherwise we count the number of z variables between
00370         ** the current depth and the top of the ADDs. These are
00371         ** the missing variables that determine the size of the
00372         ** constant blocks.
00373         */
00374         if (res == zero) return(res);
00375         scale = 1.0;
00376         for (i = 0; i < dd->size; i++) {
00377             if (vars[i]) {
00378                 if (dd->perm[i] > topP && (unsigned) dd->perm[i] < topV) {
00379                     scale *= 2;
00380                 }
00381             }
00382         }
00383         if (scale > 1.0) {
00384             cuddRef(res);
00385             add_scale = cuddUniqueConst(dd,(CUDD_VALUE_TYPE)scale);
00386             if (add_scale == NULL) {
00387                 Cudd_RecursiveDeref(dd, res);
00388                 return(NULL);
00389             }
00390             cuddRef(add_scale);
00391             scaled = cuddAddApplyRecur(dd,Cudd_addTimes,res,add_scale);
00392             if (scaled == NULL) {
00393                 Cudd_RecursiveDeref(dd, add_scale);
00394                 Cudd_RecursiveDeref(dd, res);
00395                 return(NULL);
00396             }
00397             cuddRef(scaled);
00398             Cudd_RecursiveDeref(dd, add_scale);
00399             Cudd_RecursiveDeref(dd, res);
00400             res = scaled;
00401             cuddDeref(res);
00402         }
00403         return(res);
00404     }
00405 
00406     /* compute the cofactors */
00407     if (topV == topA) {
00408         At = cuddT(A);
00409         Ae = cuddE(A);
00410     } else {
00411         At = Ae = A;
00412     }
00413     if (topV == topB) {
00414         Bt = cuddT(B);
00415         Be = cuddE(B);
00416     } else {
00417         Bt = Be = B;
00418     }
00419 
00420     t = addMMRecur(dd, At, Bt, (int)topV, vars);
00421     if (t == NULL) return(NULL);
00422     cuddRef(t);
00423     e = addMMRecur(dd, Ae, Be, (int)topV, vars);
00424     if (e == NULL) {
00425         Cudd_RecursiveDeref(dd, t);
00426         return(NULL);
00427     }
00428     cuddRef(e);
00429 
00430     index = dd->invperm[topV];
00431     if (vars[index] == 0) {
00432         /* We have split on either the rows of A or the columns
00433         ** of B. We just need to connect the two subresults,
00434         ** which correspond to two submatrices of the result.
00435         */
00436         res = (t == e) ? t : cuddUniqueInter(dd,index,t,e);
00437         if (res == NULL) {
00438             Cudd_RecursiveDeref(dd, t);
00439             Cudd_RecursiveDeref(dd, e);
00440             return(NULL);
00441         }
00442         cuddRef(res);
00443         cuddDeref(t);
00444         cuddDeref(e);
00445     } else {
00446         /* we have simultaneously split on the columns of A and
00447         ** the rows of B. The two subresults must be added.
00448         */
00449         res = cuddAddApplyRecur(dd,Cudd_addPlus,t,e);
00450         if (res == NULL) {
00451             Cudd_RecursiveDeref(dd, t);
00452             Cudd_RecursiveDeref(dd, e);
00453             return(NULL);
00454         }
00455         cuddRef(res);
00456         Cudd_RecursiveDeref(dd, t);
00457         Cudd_RecursiveDeref(dd, e);
00458     }
00459 
00460     cuddCacheInsert2(dd,cacheOp,A,B,res);
00461 
00462     /* We have computed (and stored in the computed table) a minimal
00463     ** result; that is, a result that assumes no summation variables
00464     ** between the current depth of the recursion and its top
00465     ** variable. We now take into account the z variables by properly
00466     ** scaling the result.
00467     */
00468     if (res != zero) {
00469         scale = 1.0;
00470         for (i = 0; i < dd->size; i++) {
00471             if (vars[i]) {
00472                 if (dd->perm[i] > topP && (unsigned) dd->perm[i] < topV) {
00473                     scale *= 2;
00474                 }
00475             }
00476         }
00477         if (scale > 1.0) {
00478             add_scale = cuddUniqueConst(dd,(CUDD_VALUE_TYPE)scale);
00479             if (add_scale == NULL) {
00480                 Cudd_RecursiveDeref(dd, res);
00481                 return(NULL);
00482             }
00483             cuddRef(add_scale);
00484             scaled = cuddAddApplyRecur(dd,Cudd_addTimes,res,add_scale);
00485             if (scaled == NULL) {
00486                 Cudd_RecursiveDeref(dd, res);
00487                 Cudd_RecursiveDeref(dd, add_scale);
00488                 return(NULL);
00489             }
00490             cuddRef(scaled);
00491             Cudd_RecursiveDeref(dd, add_scale);
00492             Cudd_RecursiveDeref(dd, res);
00493             res = scaled;
00494         }
00495     }
00496     cuddDeref(res);
00497     return(res);
00498 
00499 } /* end of addMMRecur */

static DdNode* addTriangleRecur ( DdManager *  dd,
DdNode *  f,
DdNode *  g,
int *  vars,
DdNode *  cube 
) [static]

Function********************************************************************

Synopsis [Performs the recursive step of Cudd_addTriangle.]

Description [Performs the recursive step of Cudd_addTriangle. Returns a pointer to the result if successful; NULL otherwise.]

SideEffects [None]

Definition at line 513 of file cuddMatMult.c.

00519 {
00520     DdNode *fv, *fvn, *gv, *gvn, *t, *e, *res;
00521     CUDD_VALUE_TYPE value;
00522     int top, topf, topg, index;
00523 
00524     statLine(dd);
00525     if (f == DD_PLUS_INFINITY(dd) || g == DD_PLUS_INFINITY(dd)) {
00526         return(DD_PLUS_INFINITY(dd));
00527     }
00528 
00529     if (cuddIsConstant(f) && cuddIsConstant(g)) {
00530         value = cuddV(f) + cuddV(g);
00531         res = cuddUniqueConst(dd, value);
00532         return(res);
00533     }
00534     if (f < g) {
00535         DdNode *tmp = f;
00536         f = g;
00537         g = tmp;
00538     }
00539 
00540     if (f->ref != 1 || g->ref != 1) {
00541         res = cuddCacheLookup(dd, DD_ADD_TRIANGLE_TAG, f, g, cube);
00542         if (res != NULL) {
00543             return(res);
00544         }
00545     }
00546 
00547     topf = cuddI(dd,f->index); topg = cuddI(dd,g->index);
00548     top = ddMin(topf,topg);
00549 
00550     if (top == topf) {fv = cuddT(f); fvn = cuddE(f);} else {fv = fvn = f;}
00551     if (top == topg) {gv = cuddT(g); gvn = cuddE(g);} else {gv = gvn = g;}
00552 
00553     t = addTriangleRecur(dd, fv, gv, vars, cube);
00554     if (t == NULL) return(NULL);
00555     cuddRef(t);
00556     e = addTriangleRecur(dd, fvn, gvn, vars, cube);
00557     if (e == NULL) {
00558         Cudd_RecursiveDeref(dd, t);
00559         return(NULL);
00560     }
00561     cuddRef(e);
00562 
00563     index = dd->invperm[top];
00564     if (vars[index] < 0) {
00565         res = (t == e) ? t : cuddUniqueInter(dd,index,t,e);
00566         if (res == NULL) {
00567             Cudd_RecursiveDeref(dd, t);
00568             Cudd_RecursiveDeref(dd, e);
00569             return(NULL);
00570         }
00571         cuddDeref(t);
00572         cuddDeref(e);
00573     } else {
00574         res = cuddAddApplyRecur(dd,Cudd_addMinimum,t,e);
00575         if (res == NULL) {
00576             Cudd_RecursiveDeref(dd, t);
00577             Cudd_RecursiveDeref(dd, e);
00578             return(NULL);
00579         }
00580         cuddRef(res);
00581         Cudd_RecursiveDeref(dd, t);
00582         Cudd_RecursiveDeref(dd, e);
00583         cuddDeref(res);
00584     }
00585 
00586     if (f->ref != 1 || g->ref != 1) {
00587         cuddCacheInsert(dd, DD_ADD_TRIANGLE_TAG, f, g, cube, res);
00588     }
00589 
00590     return(res);
00591 
00592 } /* end of addTriangleRecur */

static DdNode* cuddAddOuterSumRecur ARGS ( (DdManager *dd, DdNode *M, DdNode *r, DdNode *c)   )  [static]
static DdNode* addTriangleRecur ARGS ( (DdManager *dd, DdNode *f, DdNode *g, int *vars, DdNode *cube)   )  [static]
static DdNode* addMMRecur ARGS ( (DdManager *dd, DdNode *A, DdNode *B, int topP, int *vars)   )  [static]

AutomaticStart

DdNode* Cudd_addMatrixMultiply ( DdManager *  dd,
DdNode *  A,
DdNode *  B,
DdNode **  z,
int  nz 
)

AutomaticEnd Function********************************************************************

Synopsis [Calculates the product of two matrices represented as ADDs.]

Description [Calculates the product of two matrices, A and B, represented as ADDs. This procedure implements the quasiring multiplication algorithm. A is assumed to depend on variables x (rows) and z (columns). B is assumed to depend on variables z (rows) and y (columns). The product of A and B then depends on x (rows) and y (columns). Only the z variables have to be explicitly identified; they are the "summation" variables. Returns a pointer to the result if successful; NULL otherwise.]

SideEffects [None]

SeeAlso [Cudd_addTimesPlus Cudd_addTriangle Cudd_bddAndAbstract]

Definition at line 101 of file cuddMatMult.c.

00107 {
00108     int i, nvars, *vars;
00109     DdNode *res; 
00110 
00111     /* Array vars says what variables are "summation" variables. */
00112     nvars = dd->size;
00113     vars = ALLOC(int,nvars);
00114     if (vars == NULL) {
00115         dd->errorCode = CUDD_MEMORY_OUT;
00116         return(NULL);
00117     }
00118     for (i = 0; i < nvars; i++) {
00119         vars[i] = 0;
00120     }
00121     for (i = 0; i < nz; i++) {
00122         vars[z[i]->index] = 1;
00123     }
00124 
00125     do {
00126         dd->reordered = 0;
00127         res = addMMRecur(dd,A,B,-1,vars);
00128     } while (dd->reordered == 1);
00129     FREE(vars);
00130     return(res);
00131 
00132 } /* end of Cudd_addMatrixMultiply */

DdNode* Cudd_addOuterSum ( DdManager *  dd,
DdNode *  M,
DdNode *  r,
DdNode *  c 
)

Function********************************************************************

Synopsis [Takes the minimum of a matrix and the outer sum of two vectors.]

Description [Takes the pointwise minimum of a matrix and the outer sum of two vectors. This procedure is used in the Floyd-Warshall all-pair shortest path algorithm. Returns a pointer to the result if successful; NULL otherwise.]

SideEffects [None]

SeeAlso []

Definition at line 265 of file cuddMatMult.c.

00270 {
00271     DdNode *res;
00272 
00273     do {
00274         dd->reordered = 0;
00275         res = cuddAddOuterSumRecur(dd, M, r, c);
00276     } while (dd->reordered == 1);
00277     return(res);
00278 
00279 } /* end of Cudd_addOuterSum */

DdNode* Cudd_addTimesPlus ( DdManager *  dd,
DdNode *  A,
DdNode *  B,
DdNode **  z,
int  nz 
)

Function********************************************************************

Synopsis [Calculates the product of two matrices represented as ADDs.]

Description [Calculates the product of two matrices, A and B, represented as ADDs, using the CMU matrix by matrix multiplication procedure by Clarke et al.. Matrix A has x's as row variables and z's as column variables, while matrix B has z's as row variables and y's as column variables. Returns the pointer to the result if successful; NULL otherwise. The resulting matrix has x's as row variables and y's as column variables.]

SideEffects [None]

SeeAlso [Cudd_addMatrixMultiply]

Definition at line 154 of file cuddMatMult.c.

00160 {
00161     DdNode *w, *cube, *tmp, *res; 
00162     int i;
00163     tmp = Cudd_addApply(dd,Cudd_addTimes,A,B);
00164     if (tmp == NULL) return(NULL);
00165     Cudd_Ref(tmp);
00166     Cudd_Ref(cube = DD_ONE(dd));
00167     for (i = nz-1; i >= 0; i--) {
00168          w = Cudd_addIte(dd,z[i],cube,DD_ZERO(dd));
00169          if (w == NULL) {
00170             Cudd_RecursiveDeref(dd,tmp);
00171             return(NULL);
00172          }
00173          Cudd_Ref(w);
00174          Cudd_RecursiveDeref(dd,cube);
00175          cube = w;
00176     }
00177     res = Cudd_addExistAbstract(dd,tmp,cube);
00178     if (res == NULL) {
00179         Cudd_RecursiveDeref(dd,tmp);
00180         Cudd_RecursiveDeref(dd,cube);
00181         return(NULL);
00182     }
00183     Cudd_Ref(res);
00184     Cudd_RecursiveDeref(dd,cube);
00185     Cudd_RecursiveDeref(dd,tmp);
00186     Cudd_Deref(res);
00187     return(res);
00188 
00189 } /* end of Cudd_addTimesPlus */

DdNode* Cudd_addTriangle ( DdManager *  dd,
DdNode *  f,
DdNode *  g,
DdNode **  z,
int  nz 
)

Function********************************************************************

Synopsis [Performs the triangulation step for the shortest path computation.]

Description [Implements the semiring multiplication algorithm used in the triangulation step for the shortest path computation. f is assumed to depend on variables x (rows) and z (columns). g is assumed to depend on variables z (rows) and y (columns). The product of f and g then depends on x (rows) and y (columns). Only the z variables have to be explicitly identified; they are the "abstraction" variables. Returns a pointer to the result if successful; NULL otherwise. ]

SideEffects [None]

SeeAlso [Cudd_addMatrixMultiply Cudd_bddAndAbstract]

Definition at line 212 of file cuddMatMult.c.

00218 {
00219     int    i, nvars, *vars;
00220     DdNode *res, *cube;
00221 
00222     nvars = dd->size;
00223     vars = ALLOC(int, nvars);
00224     if (vars == NULL) {
00225         dd->errorCode = CUDD_MEMORY_OUT;
00226         return(NULL);
00227     }
00228     for (i = 0; i < nvars; i++) vars[i] = -1;
00229     for (i = 0; i < nz; i++) vars[z[i]->index] = i;
00230     cube = Cudd_addComputeCube(dd, z, NULL, nz);
00231     if (cube == NULL) {
00232         FREE(vars);
00233         return(NULL);
00234     }
00235     cuddRef(cube);
00236 
00237     do {
00238         dd->reordered = 0;
00239         res = addTriangleRecur(dd, f, g, vars, cube);
00240     } while (dd->reordered == 1);
00241     if (res != NULL) cuddRef(res);
00242     Cudd_RecursiveDeref(dd,cube);
00243     if (res != NULL) cuddDeref(res);
00244     FREE(vars);
00245     return(res);
00246 
00247 } /* end of Cudd_addTriangle */

static DdNode* cuddAddOuterSumRecur ( DdManager *  dd,
DdNode *  M,
DdNode *  r,
DdNode *  c 
) [static]

Function********************************************************************

Synopsis [Performs the recursive step of Cudd_addOuterSum.]

Description [Performs the recursive step of Cudd_addOuterSum. Returns a pointer to the result if successful; NULL otherwise.]

SideEffects [None]

SeeAlso []

Definition at line 608 of file cuddMatMult.c.

00613 {
00614     DdNode *P, *R, *Mt, *Me, *rt, *re, *ct, *ce, *Rt, *Re;
00615     int topM, topc, topr;
00616     int v, index;
00617 
00618     statLine(dd);
00619     /* Check special cases. */
00620     if (r == DD_PLUS_INFINITY(dd) || c == DD_PLUS_INFINITY(dd)) return(M); 
00621 
00622     if (cuddIsConstant(c) && cuddIsConstant(r)) {
00623         R = cuddUniqueConst(dd,Cudd_V(c)+Cudd_V(r));
00624         cuddRef(R);
00625         if (cuddIsConstant(M)) {
00626             if (cuddV(R) <= cuddV(M)) {
00627                 cuddDeref(R);
00628                 return(R);
00629             } else {
00630                 Cudd_RecursiveDeref(dd,R);       
00631                 return(M);
00632             }
00633         } else {
00634             P = Cudd_addApply(dd,Cudd_addMinimum,R,M);
00635             cuddRef(P);
00636             Cudd_RecursiveDeref(dd,R);
00637             cuddDeref(P);
00638             return(P);
00639         }
00640     }
00641 
00642     /* Check the cache. */
00643     R = cuddCacheLookup(dd,DD_ADD_OUT_SUM_TAG,M,r,c);
00644     if (R != NULL) return(R);
00645 
00646     topM = cuddI(dd,M->index); topr = cuddI(dd,r->index);
00647     topc = cuddI(dd,c->index);
00648     v = ddMin(topM,ddMin(topr,topc));
00649 
00650     /* Compute cofactors. */
00651     if (topM == v) { Mt = cuddT(M); Me = cuddE(M); } else { Mt = Me = M; }
00652     if (topr == v) { rt = cuddT(r); re = cuddE(r); } else { rt = re = r; }
00653     if (topc == v) { ct = cuddT(c); ce = cuddE(c); } else { ct = ce = c; }
00654 
00655     /* Recursively solve. */
00656     Rt = cuddAddOuterSumRecur(dd,Mt,rt,ct);
00657     if (Rt == NULL) return(NULL);
00658     cuddRef(Rt);
00659     Re = cuddAddOuterSumRecur(dd,Me,re,ce);
00660     if (Re == NULL) {
00661         Cudd_RecursiveDeref(dd, Rt);
00662         return(NULL);
00663     }
00664     cuddRef(Re);
00665     index = dd->invperm[v];
00666     R = (Rt == Re) ? Rt : cuddUniqueInter(dd,index,Rt,Re);
00667     if (R == NULL) {
00668         Cudd_RecursiveDeref(dd, Rt);
00669         Cudd_RecursiveDeref(dd, Re);
00670         return(NULL);
00671     }
00672     cuddDeref(Rt);
00673     cuddDeref(Re);
00674 
00675     /* Store the result in the cache. */
00676     cuddCacheInsert(dd,DD_ADD_OUT_SUM_TAG,M,r,c,R);
00677 
00678     return(R);
00679 
00680 } /* end of cuddAddOuterSumRecur */

Variable Documentation

char rcsid [] DD_UNUSED = "$Id: cuddMatMult.c,v 1.1.1.1 2003/02/24 22:23:52 wjiang Exp $" [static]

CFile***********************************************************************

FileName [cuddMatMult.c]

PackageName [cudd]

Synopsis [Matrix multiplication functions.]

Description [External procedures included in this module:

Static procedures included in this module:

]

Author [Fabio Somenzi]

Copyright [This file was created at the University of Colorado at Boulder. The University of Colorado at Boulder makes no warranty about the suitability of this software for any purpose. It is presented on an AS IS basis.]

Definition at line 56 of file cuddMatMult.c.

Generated on Tue Jan 5 12:18:55 2010 for abc70930 by  doxygen 1.6.1