cudd  3.0.0
The University of Colorado Decision Diagram Package
Functions
cuddMatMult.c File Reference

Matrix multiplication functions. More...

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

Functions

DdNodeCudd_addMatrixMultiply (DdManager *dd, DdNode *A, DdNode *B, DdNode **z, int nz)
 Calculates the product of two matrices represented as ADDs. More...
 
DdNodeCudd_addTimesPlus (DdManager *dd, DdNode *A, DdNode *B, DdNode **z, int nz)
 Calculates the product of two matrices represented as ADDs. More...
 
DdNodeCudd_addTriangle (DdManager *dd, DdNode *f, DdNode *g, DdNode **z, int nz)
 Performs the triangulation step for the shortest path computation. More...
 
DdNodeCudd_addOuterSum (DdManager *dd, DdNode *M, DdNode *r, DdNode *c)
 Takes the minimum of a matrix and the outer sum of two vectors. More...
 
static DdNodeaddMMRecur (DdManager *dd, DdNode *A, DdNode *B, int topP, int *vars)
 Performs the recursive step of Cudd_addMatrixMultiply. More...
 
static DdNodeaddTriangleRecur (DdManager *dd, DdNode *f, DdNode *g, int *vars, DdNode *cube)
 Performs the recursive step of Cudd_addTriangle. More...
 
static DdNodecuddAddOuterSumRecur (DdManager *dd, DdNode *M, DdNode *r, DdNode *c)
 Performs the recursive step of Cudd_addOuterSum. More...
 

Detailed Description

Matrix multiplication functions.

Author
Fabio Somenzi

Function Documentation

◆ addMMRecur()

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

Performs the recursive step of Cudd_addMatrixMultiply.

Returns
a pointer to the result if successful; NULL otherwise.
Side effects None

◆ addTriangleRecur()

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

Performs the recursive step of Cudd_addTriangle.

Returns
a pointer to the result if successful; NULL otherwise.
Side effects None

◆ Cudd_addMatrixMultiply()

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

Calculates the product of two matrices 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.
Side effects None
See also
Cudd_addTimesPlus Cudd_addTriangle Cudd_bddAndAbstract

◆ Cudd_addOuterSum()

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

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

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.
Side effects None

◆ Cudd_addTimesPlus()

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

Calculates the product of two matrices represented as ADDs.

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. The resulting matrix has x's as row variables and y's as column variables.

Returns
the pointer to the result if successful; NULL otherwise.
Side effects None
See also
Cudd_addMatrixMultiply

◆ Cudd_addTriangle()

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

Performs the triangulation step for the shortest path computation.

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.
Side effects None
See also
Cudd_addMatrixMultiply Cudd_bddAndAbstract

◆ cuddAddOuterSumRecur()

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

Performs the recursive step of Cudd_addOuterSum.

Returns
a pointer to the result if successful; NULL otherwise.
Side effects None