Version abc70930

1 files changed, 0 insertions, 680 deletions

diff --git a/src/bdd/cudd/cuddMatMult.c b/src/bdd/cudd/cuddMatMult.c
deleted file mode 100644
index 345e7921..00000000
--- a/src/bdd/cudd/cuddMatMult.c
+++ /dev/null
@@ -1,680 +0,0 @@
-/**CFile***********************************************************************
-
-  FileName    [cuddMatMult.c]
-
-  PackageName [cudd]
-
-  Synopsis    [Matrix multiplication functions.]
-
-  Description [External procedures included in this module:
-        <ul>
-        <li> Cudd_addMatrixMultiply()
-        <li> Cudd_addTimesPlus()
-        <li> Cudd_addTriangle()
-        <li> Cudd_addOuterSum()
-        </ul>
-    Static procedures included in this module:
-        <ul>
-        <li> addMMRecur()
-        <li> addTriangleRecur()
-        <li> cuddAddOuterSumRecur()
-        </ul>]
-
-  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.]
-
-******************************************************************************/
-
-#include "util_hack.h"
-#include "cuddInt.h"
-
-
-/*---------------------------------------------------------------------------*/
-/* Constant declarations                                                     */
-/*---------------------------------------------------------------------------*/
-
-
-/*---------------------------------------------------------------------------*/
-/* Stucture declarations                                                     */
-/*---------------------------------------------------------------------------*/
-
-
-/*---------------------------------------------------------------------------*/
-/* Type declarations                                                         */
-/*---------------------------------------------------------------------------*/
-
-
-/*---------------------------------------------------------------------------*/
-/* Variable declarations                                                     */
-/*---------------------------------------------------------------------------*/
-
-#ifndef lint
-static char rcsid[] DD_UNUSED = "$Id: cuddMatMult.c,v 1.1.1.1 2003/02/24 22:23:52 wjiang Exp $";
-#endif
-
-/*---------------------------------------------------------------------------*/
-/* Macro declarations                                                        */
-/*---------------------------------------------------------------------------*/
-
-
-/**AutomaticStart*************************************************************/
-
-/*---------------------------------------------------------------------------*/
-/* Static function prototypes                                                */
-/*---------------------------------------------------------------------------*/
-
-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));
-
-/**AutomaticEnd***************************************************************/
-
-
-/*---------------------------------------------------------------------------*/
-/* Definition of exported functions                                          */
-/*---------------------------------------------------------------------------*/
-
-/**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]
-
-******************************************************************************/
-DdNode *
-Cudd_addMatrixMultiply(
-  DdManager * dd,
-  DdNode * A,
-  DdNode * B,
-  DdNode ** z,
-  int  nz)
-{
-    int i, nvars, *vars;
-    DdNode *res; 
-
-    /* Array vars says what variables are "summation" variables. */
-    nvars = dd->size;
-    vars = ALLOC(int,nvars);
-    if (vars == NULL) {
-    dd->errorCode = CUDD_MEMORY_OUT;
-    return(NULL);
-    }
-    for (i = 0; i < nvars; i++) {
-        vars[i] = 0;
-    }
-    for (i = 0; i < nz; i++) {
-        vars[z[i]->index] = 1;
-    }
-
-    do {
-    dd->reordered = 0;
-    res = addMMRecur(dd,A,B,-1,vars);
-    } while (dd->reordered == 1);
-    FREE(vars);
-    return(res);
-
-} /* end of Cudd_addMatrixMultiply */
-
-
-/**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]
-
-******************************************************************************/
-DdNode *
-Cudd_addTimesPlus(
-  DdManager * dd,
-  DdNode * A,
-  DdNode * B,
-  DdNode ** z,
-  int  nz)
-{
-    DdNode *w, *cube, *tmp, *res; 
-    int i;
-    tmp = Cudd_addApply(dd,Cudd_addTimes,A,B);
-    if (tmp == NULL) return(NULL);
-    Cudd_Ref(tmp);
-    Cudd_Ref(cube = DD_ONE(dd));
-    for (i = nz-1; i >= 0; i--) {
-     w = Cudd_addIte(dd,z[i],cube,DD_ZERO(dd));
-     if (w == NULL) {
-        Cudd_RecursiveDeref(dd,tmp);
-        return(NULL);
-     }
-     Cudd_Ref(w);
-     Cudd_RecursiveDeref(dd,cube);
-     cube = w;
-    }
-    res = Cudd_addExistAbstract(dd,tmp,cube);
-    if (res == NULL) {
-    Cudd_RecursiveDeref(dd,tmp);
-    Cudd_RecursiveDeref(dd,cube);
-    return(NULL);
-    }
-    Cudd_Ref(res);
-    Cudd_RecursiveDeref(dd,cube);
-    Cudd_RecursiveDeref(dd,tmp);
-    Cudd_Deref(res);
-    return(res);
-
-} /* 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]
-
-******************************************************************************/
-DdNode *
-Cudd_addTriangle(
-  DdManager * dd,
-  DdNode * f,
-  DdNode * g,
-  DdNode ** z,
-  int  nz)
-{
-    int    i, nvars, *vars;
-    DdNode *res, *cube;
-
-    nvars = dd->size;
-    vars = ALLOC(int, nvars);
-    if (vars == NULL) {
-    dd->errorCode = CUDD_MEMORY_OUT;
-    return(NULL);
-    }
-    for (i = 0; i < nvars; i++) vars[i] = -1;
-    for (i = 0; i < nz; i++) vars[z[i]->index] = i;
-    cube = Cudd_addComputeCube(dd, z, NULL, nz);
-    if (cube == NULL) {
-    FREE(vars);
-    return(NULL);
-    }
-    cuddRef(cube);
-
-    do {
-    dd->reordered = 0;
-    res = addTriangleRecur(dd, f, g, vars, cube);
-    } while (dd->reordered == 1);
-    if (res != NULL) cuddRef(res);
-    Cudd_RecursiveDeref(dd,cube);
-    if (res != NULL) cuddDeref(res);
-    FREE(vars);
-    return(res);
-
-} /* end of Cudd_addTriangle */
-
-
-/**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     []
-
-******************************************************************************/
-DdNode *
-Cudd_addOuterSum(
-  DdManager *dd,
-  DdNode *M,
-  DdNode *r,
-  DdNode *c)
-{
-    DdNode *res;
-
-    do {
-    dd->reordered = 0;
-    res = cuddAddOuterSumRecur(dd, M, r, c);
-    } while (dd->reordered == 1);
-    return(res);
-
-} /* end of Cudd_addOuterSum */
-
-
-/*---------------------------------------------------------------------------*/
-/* Definition of internal functions                                          */
-/*---------------------------------------------------------------------------*/
-
-
-/*---------------------------------------------------------------------------*/
-/* Definition of static functions                                            */
-/*---------------------------------------------------------------------------*/
-
-/**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]
-
-******************************************************************************/
-static DdNode *
-addMMRecur(
-  DdManager * dd,
-  DdNode * A,
-  DdNode * B,
-  int  topP,
-  int * vars)
-{
-    DdNode *zero,
-           *At,        /* positive cofactor of first operand */
-       *Ae,        /* negative cofactor of first operand */
-       *Bt,        /* positive cofactor of second operand */
-       *Be,        /* negative cofactor of second operand */
-       *t,        /* positive cofactor of result */
-       *e,        /* negative cofactor of result */
-       *scaled,    /* scaled result */
-       *add_scale,    /* ADD representing the scaling factor */
-       *res;
-    int    i;        /* loop index */
-    double scale;    /* scaling factor */
-    int index;        /* index of the top variable */
-    CUDD_VALUE_TYPE value;
-    unsigned int topA, topB, topV;
-    DdNode *(*cacheOp)(DdManager *, DdNode *, DdNode *);
-
-    statLine(dd);
-    zero = DD_ZERO(dd);
-
-    if (A == zero || B == zero) {
-        return(zero);
-    }
-
-    if (cuddIsConstant(A) && cuddIsConstant(B)) {
-    /* Compute the scaling factor. It is 2^k, where k is the
-    ** number of summation variables below the current variable.
-    ** Indeed, these constants represent blocks of 2^k identical
-    ** constant values in both A and B.
-    */
-    value = cuddV(A) * cuddV(B);
-    for (i = 0; i < dd->size; i++) {
-        if (vars[i]) {
-        if (dd->perm[i] > topP) {
-            value *= (CUDD_VALUE_TYPE) 2;
-        }
-        }
-    }
-    res = cuddUniqueConst(dd, value);
-    return(res);
-    }
-
-    /* Standardize to increase cache efficiency. Clearly, A*B != B*A
-    ** in matrix multiplication. However, which matrix is which is
-    ** determined by the variables appearing in the ADDs and not by
-    ** which one is passed as first argument.
-    */
-    if (A > B) {
-    DdNode *tmp = A;
-    A = B;
-    B = tmp;
-    }
-
-    topA = cuddI(dd,A->index); topB = cuddI(dd,B->index);
-    topV = ddMin(topA,topB);
-
-    cacheOp = (DdNode *(*)(DdManager *, DdNode *, DdNode *)) addMMRecur;
-    res = cuddCacheLookup2(dd,cacheOp,A,B);
-    if (res != NULL) {
-    /* If the result is 0, there is no need to normalize.
-    ** Otherwise we count the number of z variables between
-    ** the current depth and the top of the ADDs. These are
-    ** the missing variables that determine the size of the
-    ** constant blocks.
-    */
-    if (res == zero) return(res);
-    scale = 1.0;
-    for (i = 0; i < dd->size; i++) {
-        if (vars[i]) {
-        if (dd->perm[i] > topP && (unsigned) dd->perm[i] < topV) {
-            scale *= 2;
-        }
-        }
-    }
-    if (scale > 1.0) {
-        cuddRef(res);
-        add_scale = cuddUniqueConst(dd,(CUDD_VALUE_TYPE)scale);
-        if (add_scale == NULL) {
-        Cudd_RecursiveDeref(dd, res);
-        return(NULL);
-        }
-        cuddRef(add_scale);
-        scaled = cuddAddApplyRecur(dd,Cudd_addTimes,res,add_scale);
-        if (scaled == NULL) {
-        Cudd_RecursiveDeref(dd, add_scale);
-        Cudd_RecursiveDeref(dd, res);
-        return(NULL);
-        }
-        cuddRef(scaled);
-        Cudd_RecursiveDeref(dd, add_scale);
-        Cudd_RecursiveDeref(dd, res);
-        res = scaled;
-        cuddDeref(res);
-    }
-        return(res);
-    }
-
-    /* compute the cofactors */
-    if (topV == topA) {
-    At = cuddT(A);
-    Ae = cuddE(A);
-    } else {
-    At = Ae = A;
-    }
-    if (topV == topB) {
-    Bt = cuddT(B);
-    Be = cuddE(B);
-    } else {
-    Bt = Be = B;
-    }
-
-    t = addMMRecur(dd, At, Bt, (int)topV, vars);
-    if (t == NULL) return(NULL);
-    cuddRef(t);
-    e = addMMRecur(dd, Ae, Be, (int)topV, vars);
-    if (e == NULL) {
-    Cudd_RecursiveDeref(dd, t);
-    return(NULL);
-    }
-    cuddRef(e);
-
-    index = dd->invperm[topV];
-    if (vars[index] == 0) {
-    /* We have split on either the rows of A or the columns
-    ** of B. We just need to connect the two subresults,
-    ** which correspond to two submatrices of the result.
-    */
-    res = (t == e) ? t : cuddUniqueInter(dd,index,t,e);
-    if (res == NULL) {
-        Cudd_RecursiveDeref(dd, t);
-        Cudd_RecursiveDeref(dd, e);
-        return(NULL);
-    }
-    cuddRef(res);
-    cuddDeref(t);
-    cuddDeref(e);
-    } else {
-    /* we have simultaneously split on the columns of A and
-    ** the rows of B. The two subresults must be added.
-    */
-    res = cuddAddApplyRecur(dd,Cudd_addPlus,t,e);
-    if (res == NULL) {
-        Cudd_RecursiveDeref(dd, t);
-        Cudd_RecursiveDeref(dd, e);
-        return(NULL);
-    }
-    cuddRef(res);
-    Cudd_RecursiveDeref(dd, t);
-    Cudd_RecursiveDeref(dd, e);
-    }
-
-    cuddCacheInsert2(dd,cacheOp,A,B,res);
-
-    /* We have computed (and stored in the computed table) a minimal
-    ** result; that is, a result that assumes no summation variables
-    ** between the current depth of the recursion and its top
-    ** variable. We now take into account the z variables by properly
-    ** scaling the result.
-    */
-    if (res != zero) {
-    scale = 1.0;
-    for (i = 0; i < dd->size; i++) {
-        if (vars[i]) {
-        if (dd->perm[i] > topP && (unsigned) dd->perm[i] < topV) {
-            scale *= 2;
-        }
-        }
-    }
-    if (scale > 1.0) {
-        add_scale = cuddUniqueConst(dd,(CUDD_VALUE_TYPE)scale);
-        if (add_scale == NULL) {
-        Cudd_RecursiveDeref(dd, res);
-        return(NULL);
-        }
-        cuddRef(add_scale);
-        scaled = cuddAddApplyRecur(dd,Cudd_addTimes,res,add_scale);
-        if (scaled == NULL) {
-        Cudd_RecursiveDeref(dd, res);
-        Cudd_RecursiveDeref(dd, add_scale);
-        return(NULL);
-        }
-        cuddRef(scaled);
-        Cudd_RecursiveDeref(dd, add_scale);
-        Cudd_RecursiveDeref(dd, res);
-        res = scaled;
-    }
-    }
-    cuddDeref(res);
-    return(res);
-
-} /* end of addMMRecur */
-
-
-/**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]
-
-******************************************************************************/
-static DdNode *
-addTriangleRecur(
-  DdManager * dd,
-  DdNode * f,
-  DdNode * g,
-  int * vars,
-  DdNode *cube)
-{
-    DdNode *fv, *fvn, *gv, *gvn, *t, *e, *res;
-    CUDD_VALUE_TYPE value;
-    int top, topf, topg, index;
-
-    statLine(dd);
-    if (f == DD_PLUS_INFINITY(dd) || g == DD_PLUS_INFINITY(dd)) {
-    return(DD_PLUS_INFINITY(dd));
-    }
-
-    if (cuddIsConstant(f) && cuddIsConstant(g)) {
-    value = cuddV(f) + cuddV(g);
-    res = cuddUniqueConst(dd, value);
-    return(res);
-    }
-    if (f < g) {
-    DdNode *tmp = f;
-    f = g;
-    g = tmp;
-    }
-
-    if (f->ref != 1 || g->ref != 1) {
-    res = cuddCacheLookup(dd, DD_ADD_TRIANGLE_TAG, f, g, cube);
-    if (res != NULL) {
-        return(res);
-    }
-    }
-
-    topf = cuddI(dd,f->index); topg = cuddI(dd,g->index);
-    top = ddMin(topf,topg);
-
-    if (top == topf) {fv = cuddT(f); fvn = cuddE(f);} else {fv = fvn = f;}
-    if (top == topg) {gv = cuddT(g); gvn = cuddE(g);} else {gv = gvn = g;}
-
-    t = addTriangleRecur(dd, fv, gv, vars, cube);
-    if (t == NULL) return(NULL);
-    cuddRef(t);
-    e = addTriangleRecur(dd, fvn, gvn, vars, cube);
-    if (e == NULL) {
-    Cudd_RecursiveDeref(dd, t);
-    return(NULL);
-    }
-    cuddRef(e);
-
-    index = dd->invperm[top];
-    if (vars[index] < 0) {
-    res = (t == e) ? t : cuddUniqueInter(dd,index,t,e);
-    if (res == NULL) {
-        Cudd_RecursiveDeref(dd, t);
-        Cudd_RecursiveDeref(dd, e);
-        return(NULL);
-    }
-    cuddDeref(t);
-    cuddDeref(e);
-    } else {
-    res = cuddAddApplyRecur(dd,Cudd_addMinimum,t,e);
-    if (res == NULL) {
-        Cudd_RecursiveDeref(dd, t);
-        Cudd_RecursiveDeref(dd, e);
-        return(NULL);
-    }
-    cuddRef(res);
-    Cudd_RecursiveDeref(dd, t);
-    Cudd_RecursiveDeref(dd, e);
-    cuddDeref(res);
-    }
-
-    if (f->ref != 1 || g->ref != 1) {
-    cuddCacheInsert(dd, DD_ADD_TRIANGLE_TAG, f, g, cube, res);
-    }
-
-    return(res);
-
-} /* end of addTriangleRecur */
-
-
-/**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     []
-
-******************************************************************************/
-static DdNode *
-cuddAddOuterSumRecur(
-  DdManager *dd,
-  DdNode *M,
-  DdNode *r,
-  DdNode *c)
-{
-    DdNode *P, *R, *Mt, *Me, *rt, *re, *ct, *ce, *Rt, *Re;
-    int topM, topc, topr;
-    int v, index;
-
-    statLine(dd);
-    /* Check special cases. */
-    if (r == DD_PLUS_INFINITY(dd) || c == DD_PLUS_INFINITY(dd)) return(M); 
-
-    if (cuddIsConstant(c) && cuddIsConstant(r)) {
-    R = cuddUniqueConst(dd,Cudd_V(c)+Cudd_V(r));
-    cuddRef(R);
-    if (cuddIsConstant(M)) {
-        if (cuddV(R) <= cuddV(M)) {
-        cuddDeref(R);
-            return(R);
-        } else {
-            Cudd_RecursiveDeref(dd,R);       
-        return(M);
-        }
-    } else {
-        P = Cudd_addApply(dd,Cudd_addMinimum,R,M);
-        cuddRef(P);
-        Cudd_RecursiveDeref(dd,R);
-        cuddDeref(P);
-        return(P);
-    }
-    }
-
-    /* Check the cache. */
-    R = cuddCacheLookup(dd,DD_ADD_OUT_SUM_TAG,M,r,c);
-    if (R != NULL) return(R);
-
-    topM = cuddI(dd,M->index); topr = cuddI(dd,r->index);
-    topc = cuddI(dd,c->index);
-    v = ddMin(topM,ddMin(topr,topc));
-
-    /* Compute cofactors. */
-    if (topM == v) { Mt = cuddT(M); Me = cuddE(M); } else { Mt = Me = M; }
-    if (topr == v) { rt = cuddT(r); re = cuddE(r); } else { rt = re = r; }
-    if (topc == v) { ct = cuddT(c); ce = cuddE(c); } else { ct = ce = c; }
-
-    /* Recursively solve. */
-    Rt = cuddAddOuterSumRecur(dd,Mt,rt,ct);
-    if (Rt == NULL) return(NULL);
-    cuddRef(Rt);
-    Re = cuddAddOuterSumRecur(dd,Me,re,ce);
-    if (Re == NULL) {
-    Cudd_RecursiveDeref(dd, Rt);
-    return(NULL);
-    }
-    cuddRef(Re);
-    index = dd->invperm[v];
-    R = (Rt == Re) ? Rt : cuddUniqueInter(dd,index,Rt,Re);
-    if (R == NULL) {
-    Cudd_RecursiveDeref(dd, Rt);
-    Cudd_RecursiveDeref(dd, Re);
-    return(NULL);
-    }
-    cuddDeref(Rt);
-    cuddDeref(Re);
-
-    /* Store the result in the cache. */
-    cuddCacheInsert(dd,DD_ADD_OUT_SUM_TAG,M,r,c,R);
-
-    return(R);
-
-} /* end of cuddAddOuterSumRecur */