/**CFile***********************************************************************

  FileName    [cuddZddPort.c]

  PackageName [cudd]

  Synopsis    [Functions that translate BDDs to ZDDs.]

  Description [External procedures included in this module:
            <ul>
            <li> Cudd_zddPortFromBdd()
            <li> Cudd_zddPortToBdd()
            </ul>
           Internal procedures included in this module:
            <ul>
            </ul>
           Static procedures included in this module:
            <ul>
            <li> zddPortFromBddStep()
            <li> zddPortToBddStep()
            </ul>
          ]

  SeeAlso     []

  Author      [Hyong-kyoon Shin, In-Ho Moon]

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

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


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


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


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

#ifndef lint
static char rcsid[] DD_UNUSED = "$Id: cuddZddPort.c,v 1.1.1.1 2003/02/24 22:23:54 wjiang Exp $";
#endif

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


/**AutomaticStart*************************************************************/

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

static DdNode * zddPortFromBddStep ARGS((DdManager *dd, DdNode *B, int expected));
static DdNode * zddPortToBddStep ARGS((DdManager *dd, DdNode *f, int depth));

/**AutomaticEnd***************************************************************/


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


/**Function********************************************************************

  Synopsis [Converts a BDD into a ZDD.]

  Description [Converts a BDD into a ZDD. This function assumes that
  there is a one-to-one correspondence between the BDD variables and the
  ZDD variables, and that the variable order is the same for both types
  of variables. These conditions are established if the ZDD variables
  are created by one call to Cudd_zddVarsFromBddVars with multiplicity =
  1. Returns a pointer to the resulting ZDD if successful; NULL otherwise.]

  SideEffects [None]

  SeeAlso     [Cudd_zddVarsFromBddVars]

******************************************************************************/
DdNode *
Cudd_zddPortFromBdd(
  DdManager * dd,
  DdNode * B)
{
    DdNode *res;

    do {
    dd->reordered = 0;
    res = zddPortFromBddStep(dd,B,0);
    } while (dd->reordered == 1);

    return(res);

} /* end of Cudd_zddPortFromBdd */


/**Function********************************************************************

  Synopsis [Converts a ZDD into a BDD.]

  Description [Converts a ZDD into a BDD. Returns a pointer to the resulting
  ZDD if successful; NULL otherwise.]

  SideEffects [None]

  SeeAlso     [Cudd_zddPortFromBdd]

******************************************************************************/
DdNode *
Cudd_zddPortToBdd(
  DdManager * dd,
  DdNode * f)
{
    DdNode *res;

    do {
    dd->reordered = 0;
    res = zddPortToBddStep(dd,f,0);
    } while (dd->reordered == 1);

    return(res);

} /* end of Cudd_zddPortToBdd */


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

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


/**Function********************************************************************

  Synopsis [Performs the recursive step of Cudd_zddPortFromBdd.]

  Description []

  SideEffects [None]

  SeeAlso     []

******************************************************************************/
static DdNode *
zddPortFromBddStep(
  DdManager * dd,
  DdNode * B,
  int  expected)
{
    DdNode    *res, *prevZdd, *t, *e;
    DdNode    *Breg, *Bt, *Be;
    int        id, level;

    statLine(dd);
    /* Terminal cases. */
    if (B == Cudd_Not(DD_ONE(dd)))
    return(DD_ZERO(dd));
    if (B == DD_ONE(dd)) {
    if (expected >= dd->sizeZ) {
        return(DD_ONE(dd));
    } else {
        return(dd->univ[expected]);
    }
    }

    Breg = Cudd_Regular(B);

    /* Computed table look-up. */
    res = cuddCacheLookup1Zdd(dd,Cudd_zddPortFromBdd,B);
    if (res != NULL) {
    level = cuddI(dd,Breg->index);
    /* Adding DC vars. */
    if (expected < level) {
        /* Add suppressed variables. */
        cuddRef(res);
        for (level--; level >= expected; level--) {
        prevZdd = res;
        id = dd->invperm[level];
        res = cuddZddGetNode(dd, id, prevZdd, prevZdd);
        if (res == NULL) {
            Cudd_RecursiveDerefZdd(dd, prevZdd);
            return(NULL);
        }
        cuddRef(res);
        Cudd_RecursiveDerefZdd(dd, prevZdd);
        }
        cuddDeref(res);
    }
    return(res);
    }    /* end of cache look-up */

    if (Cudd_IsComplement(B)) {
    Bt = Cudd_Not(cuddT(Breg));
    Be = Cudd_Not(cuddE(Breg));
    } else {
    Bt = cuddT(Breg);
    Be = cuddE(Breg);
    }

    id = Breg->index;
    level = cuddI(dd,id);
    t = zddPortFromBddStep(dd, Bt, level+1);
    if (t == NULL) return(NULL);
    cuddRef(t);
    e = zddPortFromBddStep(dd, Be, level+1);
    if (e == NULL) {
    Cudd_RecursiveDerefZdd(dd, t);
    return(NULL);
    }
    cuddRef(e);
    res = cuddZddGetNode(dd, id, t, e);
    if (res == NULL) {
    Cudd_RecursiveDerefZdd(dd, t);
    Cudd_RecursiveDerefZdd(dd, e);
    return(NULL);
    }
    cuddRef(res);
    Cudd_RecursiveDerefZdd(dd, t);
    Cudd_RecursiveDerefZdd(dd, e);

    cuddCacheInsert1(dd,Cudd_zddPortFromBdd,B,res);

    for (level--; level >= expected; level--) {
    prevZdd = res;
    id = dd->invperm[level];
    res = cuddZddGetNode(dd, id, prevZdd, prevZdd);
    if (res == NULL) {
        Cudd_RecursiveDerefZdd(dd, prevZdd);
        return(NULL);
    }
    cuddRef(res);
    Cudd_RecursiveDerefZdd(dd, prevZdd);
    }

    cuddDeref(res);
    return(res);

} /* end of zddPortFromBddStep */


/**Function********************************************************************

  Synopsis [Performs the recursive step of Cudd_zddPortToBdd.]

  Description []

  SideEffects [None]

  SeeAlso     []

******************************************************************************/
static DdNode *
zddPortToBddStep(
  DdManager * dd /* manager */,
  DdNode * f /* ZDD to be converted */,
  int  depth /* recursion depth */)
{
    DdNode *one, *zero, *T, *E, *res, *var;
    unsigned int index;
    unsigned int level;

    statLine(dd);
    one = DD_ONE(dd);
    zero = DD_ZERO(dd);
    if (f == zero) return(Cudd_Not(one));

    if (depth == dd->sizeZ) return(one);

    index = dd->invpermZ[depth];
    level = cuddIZ(dd,f->index);
    var = cuddUniqueInter(dd,index,one,Cudd_Not(one));
    if (var == NULL) return(NULL);
    cuddRef(var);

    if (level > (unsigned) depth) {
    E = zddPortToBddStep(dd,f,depth+1);
    if (E == NULL) {
        Cudd_RecursiveDeref(dd,var);
        return(NULL);
    }
    cuddRef(E);
    res = cuddBddIteRecur(dd,var,Cudd_Not(one),E);
    if (res == NULL) {
        Cudd_RecursiveDeref(dd,var);
        Cudd_RecursiveDeref(dd,E);
        return(NULL);
    }
    cuddRef(res);
    Cudd_RecursiveDeref(dd,var);
    Cudd_RecursiveDeref(dd,E);
    cuddDeref(res);
    return(res);
    }

    res = cuddCacheLookup1(dd,Cudd_zddPortToBdd,f);
    if (res != NULL) {
    Cudd_RecursiveDeref(dd,var);
    return(res);
    }

    T = zddPortToBddStep(dd,cuddT(f),depth+1);
    if (T == NULL) {
    Cudd_RecursiveDeref(dd,var);
    return(NULL);
    }
    cuddRef(T);
    E = zddPortToBddStep(dd,cuddE(f),depth+1);
    if (E == NULL) {
    Cudd_RecursiveDeref(dd,var);
    Cudd_RecursiveDeref(dd,T);
    return(NULL);
    }
    cuddRef(E);

    res = cuddBddIteRecur(dd,var,T,E);
    if (res == NULL) {
    Cudd_RecursiveDeref(dd,var);
    Cudd_RecursiveDeref(dd,T);
    Cudd_RecursiveDeref(dd,E);
    return(NULL);
    }
    cuddRef(res);
    Cudd_RecursiveDeref(dd,var);
    Cudd_RecursiveDeref(dd,T);
    Cudd_RecursiveDeref(dd,E);
    cuddDeref(res);

    cuddCacheInsert1(dd,Cudd_zddPortToBdd,f,res);

    return(res);

} /* end of zddPortToBddStep */