src/cuBdd/cuddRead.c

Go to the documentation of this file.

#include "util.h"
#include "cuddInt.h"


/*---------------------------------------------------------------------------*/
/* Constant declarations                                                     */
/*---------------------------------------------------------------------------*/


/*---------------------------------------------------------------------------*/
/* Stucture declarations                                                     */
/*---------------------------------------------------------------------------*/


/*---------------------------------------------------------------------------*/
/* Type declarations                                                         */
/*---------------------------------------------------------------------------*/


/*---------------------------------------------------------------------------*/
/* Variable declarations                                                     */
/*---------------------------------------------------------------------------*/

#ifndef lint
static char rcsid[] DD_UNUSED = "$Id: cuddRead.c,v 1.6 2004/08/13 18:04:50 fabio Exp $";
#endif

/*---------------------------------------------------------------------------*/
/* Macro declarations                                                        */
/*---------------------------------------------------------------------------*/


/*---------------------------------------------------------------------------*/
/* Static function prototypes                                                */
/*---------------------------------------------------------------------------*/


/*---------------------------------------------------------------------------*/
/* Definition of exported functions                                          */
/*---------------------------------------------------------------------------*/


int
Cudd_addRead(
  FILE * fp /* input file pointer */,
  DdManager * dd /* DD manager */,
  DdNode ** E /* characteristic function of the graph */,
  DdNode *** x /* array of row variables */,
  DdNode *** y /* array of column variables */,
  DdNode *** xn /* array of complemented row variables */,
  DdNode *** yn_ /* array of complemented column variables */,
  int * nx /* number or row variables */,
  int * ny /* number or column variables */,
  int * m /* number of rows */,
  int * n /* number of columns */,
  int  bx /* first index of row variables */,
  int  sx /* step of row variables */,
  int  by /* first index of column variables */,
  int  sy /* step of column variables */)
{
    DdNode *one, *zero;
    DdNode *w, *neW;
    DdNode *minterm1;
    int u, v, err, i, nv;
    int lnx, lny;
    CUDD_VALUE_TYPE val;
    DdNode **lx, **ly, **lxn, **lyn;

    one = DD_ONE(dd);
    zero = DD_ZERO(dd);

    err = fscanf(fp, "%d %d", &u, &v);
    if (err == EOF) {
        return(0);
    } else if (err != 2) {
        return(0);
    }

    *m = u;
    /* Compute the number of x variables. */
    lx = *x; lxn = *xn;
    u--;        /* row and column numbers start from 0 */
    for (lnx=0; u > 0; lnx++) {
        u >>= 1;
    }
    /* Here we rely on the fact that REALLOC of a null pointer is
    ** translates to an ALLOC.
    */
    if (lnx > *nx) {
        *x = lx = REALLOC(DdNode *, *x, lnx);
        if (lx == NULL) {
            dd->errorCode = CUDD_MEMORY_OUT;
            return(0);
        }
        *xn = lxn =  REALLOC(DdNode *, *xn, lnx);
        if (lxn == NULL) {
            dd->errorCode = CUDD_MEMORY_OUT;
            return(0);
        }
    }

    *n = v;
    /* Compute the number of y variables. */
    ly = *y; lyn = *yn_;
    v--;        /* row and column numbers start from 0 */
    for (lny=0; v > 0; lny++) {
        v >>= 1;
    }
    /* Here we rely on the fact that REALLOC of a null pointer is
    ** translates to an ALLOC.
    */
    if (lny > *ny) {
        *y = ly = REALLOC(DdNode *, *y, lny);
        if (ly == NULL) {
            dd->errorCode = CUDD_MEMORY_OUT;
            return(0);
        }
        *yn_ = lyn =  REALLOC(DdNode *, *yn_, lny);
        if (lyn == NULL) {
            dd->errorCode = CUDD_MEMORY_OUT;
            return(0);
        }
    }

    /* Create all new variables. */
    for (i = *nx, nv = bx + (*nx) * sx; i < lnx; i++, nv += sx) {
        do {
            dd->reordered = 0;
            lx[i] = cuddUniqueInter(dd, nv, one, zero);
        } while (dd->reordered == 1);
        if (lx[i] == NULL) return(0);
        cuddRef(lx[i]);
        do {
            dd->reordered = 0;
            lxn[i] = cuddUniqueInter(dd, nv, zero, one);
        } while (dd->reordered == 1);
        if (lxn[i] == NULL) return(0);
        cuddRef(lxn[i]);
    }
    for (i = *ny, nv = by + (*ny) * sy; i < lny; i++, nv += sy) {
        do {
            dd->reordered = 0;
            ly[i] = cuddUniqueInter(dd, nv, one, zero);
        } while (dd->reordered == 1);
        if (ly[i] == NULL) return(0);
        cuddRef(ly[i]);
        do {
            dd->reordered = 0;
            lyn[i] = cuddUniqueInter(dd, nv, zero, one);
        } while (dd->reordered == 1);
        if (lyn[i] == NULL) return(0);
        cuddRef(lyn[i]);
    }
    *nx = lnx;
    *ny = lny;

    *E = dd->background; /* this call will never cause reordering */
    cuddRef(*E);

    while (! feof(fp)) {
        err = fscanf(fp, "%d %d %lf", &u, &v, &val);
        if (err == EOF) {
            break;
        } else if (err != 3) {
            return(0);
        } else if (u >= *m || v >= *n || u < 0 || v < 0) {
            return(0);
        }
 
        minterm1 = one; cuddRef(minterm1);

        /* Build minterm1 corresponding to this arc */
        for (i = lnx - 1; i>=0; i--) {
            if (u & 1) {
                w = Cudd_addApply(dd, Cudd_addTimes, minterm1, lx[i]);
            } else {
                w = Cudd_addApply(dd, Cudd_addTimes, minterm1, lxn[i]);
            }
            if (w == NULL) {
                Cudd_RecursiveDeref(dd, minterm1);
                return(0);
            }
            cuddRef(w);
            Cudd_RecursiveDeref(dd, minterm1);
            minterm1 = w;
            u >>= 1;
        }
        for (i = lny - 1; i>=0; i--) {
            if (v & 1) {
                w = Cudd_addApply(dd, Cudd_addTimes, minterm1, ly[i]);
            } else {
                w = Cudd_addApply(dd, Cudd_addTimes, minterm1, lyn[i]);
            }
            if (w == NULL) {
                Cudd_RecursiveDeref(dd, minterm1);
                return(0);
            }
            cuddRef(w);
            Cudd_RecursiveDeref(dd, minterm1);
            minterm1 = w;
            v >>= 1;
        }
        /* Create new constant node if necessary.
        ** This call will never cause reordering.
        */
        neW = cuddUniqueConst(dd, val);
        if (neW == NULL) {
            Cudd_RecursiveDeref(dd, minterm1);
            return(0);
        }
        cuddRef(neW);

        w = Cudd_addIte(dd, minterm1, neW, *E);
        if (w == NULL) {
            Cudd_RecursiveDeref(dd, minterm1);
            Cudd_RecursiveDeref(dd, neW);
            return(0);
        }
        cuddRef(w);
        Cudd_RecursiveDeref(dd, minterm1);
        Cudd_RecursiveDeref(dd, neW);
        Cudd_RecursiveDeref(dd, *E);
        *E = w;
    }
    return(1);

} /* end of Cudd_addRead */


int
Cudd_bddRead(
  FILE * fp /* input file pointer */,
  DdManager * dd /* DD manager */,
  DdNode ** E /* characteristic function of the graph */,
  DdNode *** x /* array of row variables */,
  DdNode *** y /* array of column variables */,
  int * nx /* number or row variables */,
  int * ny /* number or column variables */,
  int * m /* number of rows */,
  int * n /* number of columns */,
  int  bx /* first index of row variables */,
  int  sx /* step of row variables */,
  int  by /* first index of column variables */,
  int  sy /* step of column variables */)
{
    DdNode *one, *zero;
    DdNode *w;
    DdNode *minterm1;
    int u, v, err, i, nv;
    int lnx, lny;
    DdNode **lx, **ly;

    one = DD_ONE(dd);
    zero = Cudd_Not(one);

    err = fscanf(fp, "%d %d", &u, &v);
    if (err == EOF) {
        return(0);
    } else if (err != 2) {
        return(0);
    }

    *m = u;
    /* Compute the number of x variables. */
    lx = *x;
    u--;        /* row and column numbers start from 0 */
    for (lnx=0; u > 0; lnx++) {
        u >>= 1;
    }
    if (lnx > *nx) {
        *x = lx = REALLOC(DdNode *, *x, lnx);
        if (lx == NULL) {
            dd->errorCode = CUDD_MEMORY_OUT;
            return(0);
        }
    }

    *n = v;
    /* Compute the number of y variables. */
    ly = *y;
    v--;        /* row and column numbers start from 0 */
    for (lny=0; v > 0; lny++) {
        v >>= 1;
    }
    if (lny > *ny) {
        *y = ly = REALLOC(DdNode *, *y, lny);
        if (ly == NULL) {
            dd->errorCode = CUDD_MEMORY_OUT;
            return(0);
        }
    }

    /* Create all new variables. */
    for (i = *nx, nv = bx + (*nx) * sx; i < lnx; i++, nv += sx) {
        do {
            dd->reordered = 0;
            lx[i] = cuddUniqueInter(dd, nv, one, zero);
        } while (dd->reordered == 1);
        if (lx[i] == NULL) return(0);
        cuddRef(lx[i]);
    }
    for (i = *ny, nv = by + (*ny) * sy; i < lny; i++, nv += sy) {
        do {
            dd->reordered = 0;
            ly[i] = cuddUniqueInter(dd, nv, one, zero);
        } while (dd->reordered == 1);
        if (ly[i] == NULL) return(0);
        cuddRef(ly[i]);
    }
    *nx = lnx;
    *ny = lny;

    *E = zero; /* this call will never cause reordering */
    cuddRef(*E);

    while (! feof(fp)) {
        err = fscanf(fp, "%d %d", &u, &v);
        if (err == EOF) {
            break;
        } else if (err != 2) {
            return(0);
        } else if (u >= *m || v >= *n || u < 0 || v < 0) {
            return(0);
        }
 
        minterm1 = one; cuddRef(minterm1);

        /* Build minterm1 corresponding to this arc. */
        for (i = lnx - 1; i>=0; i--) {
            if (u & 1) {
                w = Cudd_bddAnd(dd, minterm1, lx[i]);
            } else {
                w = Cudd_bddAnd(dd, minterm1, Cudd_Not(lx[i]));
            }
            if (w == NULL) {
                Cudd_RecursiveDeref(dd, minterm1);
                return(0);
            }
            cuddRef(w);
            Cudd_RecursiveDeref(dd,minterm1);
            minterm1 = w;
            u >>= 1;
        }
        for (i = lny - 1; i>=0; i--) {
            if (v & 1) {
                w = Cudd_bddAnd(dd, minterm1, ly[i]);
            } else {
                w = Cudd_bddAnd(dd, minterm1, Cudd_Not(ly[i]));
            }
            if (w == NULL) {
                Cudd_RecursiveDeref(dd, minterm1);
                return(0);
            }
            cuddRef(w);
            Cudd_RecursiveDeref(dd, minterm1);
            minterm1 = w;
            v >>= 1;
        }

        w = Cudd_bddAnd(dd, Cudd_Not(minterm1), Cudd_Not(*E));
        if (w == NULL) {
            Cudd_RecursiveDeref(dd, minterm1);
            return(0);
        }
        w = Cudd_Not(w);
        cuddRef(w);
        Cudd_RecursiveDeref(dd, minterm1);
        Cudd_RecursiveDeref(dd, *E);
        *E = w;
    }
    return(1);

} /* end of Cudd_bddRead */

/*---------------------------------------------------------------------------*/
/* Definition of internal functions                                          */
/*---------------------------------------------------------------------------*/


/*---------------------------------------------------------------------------*/
/* Definition of static functions                                            */
/*---------------------------------------------------------------------------*/

---