#include "util_hack.h"
#include "cuddInt.h"
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********************************************************************
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
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 */
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 */
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 */
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 */
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 */
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.