Version abc71001

1 files changed, 0 insertions, 490 deletions

diff --git a/abc70930/src/bdd/cudd/cuddRead.c b/abc70930/src/bdd/cudd/cuddRead.c
deleted file mode 100644
index 2c4a86d8..00000000
--- a/abc70930/src/bdd/cudd/cuddRead.c
+++ /dev/null
@@ -1,490 +0,0 @@
-/**CFile***********************************************************************
-
-  FileName    [cuddRead.c]
-
-  PackageName [cudd]
-
-  Synopsis    [Functions to read in a matrix]
-
-  Description [External procedures included in this module:
-        <ul>
-        <li> Cudd_addRead()
-        <li> Cudd_bddRead()
-        </ul>]
-
-  SeeAlso     [cudd_addHarwell.c]
-
-  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: cuddRead.c,v 1.1.1.1 2003/02/24 22:23:52 wjiang Exp $";
-#endif
-
-/*---------------------------------------------------------------------------*/
-/* Macro declarations                                                        */
-/*---------------------------------------------------------------------------*/
-
-
-/**AutomaticStart*************************************************************/
-
-/*---------------------------------------------------------------------------*/
-/* Static function prototypes                                                */
-/*---------------------------------------------------------------------------*/
-
-
-/**AutomaticEnd***************************************************************/
-
-
-/*---------------------------------------------------------------------------*/
-/* Definition of exported functions                                          */
-/*---------------------------------------------------------------------------*/
-
-
-/**Function********************************************************************
-
-  Synopsis    [Reads in a sparse matrix.]
-
-  Description [Reads in a sparse matrix specified in a simple format.
-  The first line of the input contains the numbers of rows and columns.
-  The remaining lines contain the elements of the matrix, one per line.
-  Given a background value
-  (specified by the background field of the manager), only the values
-  different from it are explicitly listed.  Each foreground element is
-  described by two integers, i.e., the row and column number, and a
-  real number, i.e., the value.<p>
-  Cudd_addRead produces an ADD that depends on two sets of variables: x
-  and y.  The x variables (x\[0\] ... x\[nx-1\]) encode the row index and
-  the y variables (y\[0\] ... y\[ny-1\]) encode the column index.
-  x\[0\] and y\[0\] are the most significant bits in the indices.
-  The variables may already exist or may be created by the function.
-  The index of x\[i\] is bx+i*sx, and the index of y\[i\] is by+i*sy.<p>
-  On input, nx and ny hold the numbers
-  of row and column variables already in existence. On output, they
-  hold the numbers of row and column variables actually used by the
-  matrix. When Cudd_addRead creates the variable arrays,
-  the index of x\[i\] is bx+i*sx, and the index of y\[i\] is by+i*sy.
-  When some variables already exist Cudd_addRead expects the indices
-  of the existing x variables to be bx+i*sx, and the indices of the
-  existing y variables to be by+i*sy.<p>
-  m and n are set to the numbers of rows and columns of the
-  matrix.  Their values on input are immaterial.
-  The ADD for the
-  sparse matrix is returned in E, and its reference count is > 0.
-  Cudd_addRead returns 1 in case of success; 0 otherwise.]
-
-  SideEffects [nx and ny are set to the numbers of row and column
-  variables. m and n are set to the numbers of rows and columns. x and y
-  are possibly extended to represent the array of row and column
-  variables. Similarly for xn and yn_, which hold on return from
-  Cudd_addRead the complements of the row and column variables.]
-
-  SeeAlso     [Cudd_addHarwell Cudd_bddRead]
-
-******************************************************************************/
-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 */
-
-
-/**Function********************************************************************
-
-  Synopsis    [Reads in a graph (without labels) given as a list of arcs.]
-
-  Description [Reads in a graph (without labels) given as an adjacency
-  matrix.  The first line of the input contains the numbers of rows and
-  columns of the adjacency matrix. The remaining lines contain the arcs
-  of the graph, one per line. Each arc is described by two integers,
-  i.e., the row and column number, or the indices of the two endpoints.
-  Cudd_bddRead produces a BDD that depends on two sets of variables: x
-  and y.  The x variables (x\[0\] ... x\[nx-1\]) encode
-  the row index and the y variables (y\[0\] ... y\[ny-1\]) encode the
-  column index. x\[0\] and y\[0\] are the most significant bits in the
-  indices.
-  The variables may already exist or may be created by the function.
-  The index of x\[i\] is bx+i*sx, and the index of y\[i\] is by+i*sy.<p>
-  On input, nx and ny hold the numbers of row and column variables already
-  in existence. On output, they hold the numbers of row and column
-  variables actually used by the matrix. When Cudd_bddRead creates the
-  variable arrays, the index of x\[i\] is bx+i*sx, and the index of
-  y\[i\] is by+i*sy. When some variables already exist, Cudd_bddRead
-  expects the indices of the existing x variables to be bx+i*sx, and the
-  indices of the existing y variables to be by+i*sy.<p>
-  m and n are set to the numbers of rows and columns of the
-  matrix.  Their values on input are immaterial.  The BDD for the graph
-  is returned in E, and its reference count is > 0. Cudd_bddRead returns
-  1 in case of success; 0 otherwise.]
-
-  SideEffects [nx and ny are set to the numbers of row and column
-  variables. m and n are set to the numbers of rows and columns. x and y
-  are possibly extended to represent the array of row and column
-  variables.]
-
-  SeeAlso     [Cudd_addHarwell 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                                            */
-/*---------------------------------------------------------------------------*/
-