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

  FileName    [extraBddUnate.c]

  PackageName [extra]

  Synopsis    [Efficient methods to compute the information about
  unate variables using an algorithm that is conceptually similar to
  the algorithm for two-variable symmetry computation presented in:
  A. Mishchenko. Fast Computation of Symmetries in Boolean Functions. 
  Transactions on CAD, Nov. 2003.]

  Author      [Alan Mishchenko]
  
  Affiliation [UC Berkeley]

  Date        [Ver. 2.0. Started - September 1, 2003.]

  Revision    [$Id: extraBddUnate.c,v 1.0 2003/09/01 00:00:00 alanmi Exp $]

***********************************************************************/

#include "extraBdd.h"

ABC_NAMESPACE_IMPL_START


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

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

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

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

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

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

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

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

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


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

  Synopsis    [Computes the classical symmetry information for the function.]

  Description [Returns the symmetry information in the form of Extra_UnateInfo_t structure.]

  SideEffects [If the ZDD variables are not derived from BDD variables with
  multiplicity 2, this function may derive them in a wrong way.]

  SeeAlso     []

******************************************************************************/
Extra_UnateInfo_t * Extra_UnateComputeFast( 
  DdManager * dd,   /* the manager */
  DdNode * bFunc)   /* the function whose symmetries are computed */
{
    DdNode * bSupp;
    DdNode * zRes;
    Extra_UnateInfo_t * p;

    bSupp = Cudd_Support( dd, bFunc );                      Cudd_Ref( bSupp );
    zRes  = Extra_zddUnateInfoCompute( dd, bFunc, bSupp );  Cudd_Ref( zRes );

    p = Extra_UnateInfoCreateFromZdd( dd, zRes, bSupp );

    Cudd_RecursiveDeref( dd, bSupp );
    Cudd_RecursiveDerefZdd( dd, zRes );

    return p;

} /* end of Extra_UnateInfoCompute */


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

  Synopsis    [Computes the classical symmetry information as a ZDD.]

  Description []

  SideEffects []

  SeeAlso     []

******************************************************************************/
DdNode * Extra_zddUnateInfoCompute( 
  DdManager * dd,   /* the DD manager */
  DdNode * bF,
  DdNode * bVars) 
{
    DdNode * res;
    do {
        dd->reordered = 0;
        res = extraZddUnateInfoCompute( dd, bF, bVars );
    } while (dd->reordered == 1);
    return(res);

} /* end of Extra_zddUnateInfoCompute */


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

  Synopsis    [Converts a set of variables into a set of singleton subsets.]

  Description []

  SideEffects []

  SeeAlso     []

******************************************************************************/
DdNode * Extra_zddGetSingletonsBoth( 
  DdManager * dd,    /* the DD manager */
  DdNode * bVars)    /* the set of variables */
{
    DdNode * res;
    do {
        dd->reordered = 0;
        res = extraZddGetSingletonsBoth( dd, bVars );
    } while (dd->reordered == 1);
    return(res);

} /* end of Extra_zddGetSingletonsBoth */

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

  Synopsis    [Allocates unateness information structure.]

  Description []

  SideEffects []

  SeeAlso     []

******************************************************************************/
Extra_UnateInfo_t *  Extra_UnateInfoAllocate( int nVars )
{
    Extra_UnateInfo_t * p;
    // allocate and clean the storage for unateness info
    p = ABC_ALLOC( Extra_UnateInfo_t, 1 );
    memset( p, 0, sizeof(Extra_UnateInfo_t) );
    p->nVars     = nVars;
    p->pVars     = ABC_ALLOC( Extra_UnateVar_t, nVars );  
    memset( p->pVars, 0, nVars * sizeof(Extra_UnateVar_t) );
    return p;
} /* end of Extra_UnateInfoAllocate */

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

  Synopsis    [Deallocates symmetry information structure.]

  Description []

  SideEffects []

  SeeAlso     []

******************************************************************************/
void Extra_UnateInfoDissolve( Extra_UnateInfo_t * p )
{
    ABC_FREE( p->pVars );
    ABC_FREE( p );
} /* end of Extra_UnateInfoDissolve */

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

  Synopsis    [Allocates symmetry information structure.]

  Description []

  SideEffects []

  SeeAlso     []

******************************************************************************/
void Extra_UnateInfoPrint( Extra_UnateInfo_t * p )
{
    char * pBuffer;
    int i;
    pBuffer = ABC_ALLOC( char, p->nVarsMax+1 );
    memset( pBuffer, ' ', p->nVarsMax );
    pBuffer[p->nVarsMax] = 0;
    for ( i = 0; i < p->nVars; i++ )
        if ( p->pVars[i].Neg )
            pBuffer[ p->pVars[i].iVar ] = 'n';
        else if ( p->pVars[i].Pos )
            pBuffer[ p->pVars[i].iVar ] = 'p';
        else
            pBuffer[ p->pVars[i].iVar ] = '.';
    printf( "%s\n", pBuffer );
    ABC_FREE( pBuffer );
} /* end of Extra_UnateInfoPrint */


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

  Synopsis    [Creates the symmetry information structure from ZDD.]

  Description [ZDD representation of symmetries is the set of cubes, each
  of which has two variables in the positive polarity. These variables correspond
  to the symmetric variable pair.]

  SideEffects []

  SeeAlso     []

******************************************************************************/
Extra_UnateInfo_t * Extra_UnateInfoCreateFromZdd( DdManager * dd, DdNode * zPairs, DdNode * bSupp )
{
    Extra_UnateInfo_t * p;
    DdNode * bTemp, * zSet, * zCube, * zTemp;
    int * pMapVars2Nums;
    int i, nSuppSize;

    nSuppSize = Extra_bddSuppSize( dd, bSupp );

    // allocate and clean the storage for symmetry info
    p = Extra_UnateInfoAllocate( nSuppSize );

    // allocate the storage for the temporary map
    pMapVars2Nums = ABC_ALLOC( int, dd->size );
    memset( pMapVars2Nums, 0, dd->size * sizeof(int) );

    // assign the variables
    p->nVarsMax = dd->size;
    for ( i = 0, bTemp = bSupp; bTemp != b1; bTemp = cuddT(bTemp), i++ )
    {
        p->pVars[i].iVar = bTemp->index;
        pMapVars2Nums[bTemp->index] = i;
    }

    // write the symmetry info into the structure
    zSet = zPairs;   Cudd_Ref( zSet );
//    Cudd_zddPrintCover( dd, zPairs );    printf( "\n" );
    while ( zSet != z0 )
    {
        // get the next cube
        zCube  = Extra_zddSelectOneSubset( dd, zSet );    Cudd_Ref( zCube );

        // add this var to the data structure
        assert( cuddT(zCube) == z1 && cuddE(zCube) == z0 );
        if ( zCube->index & 1 ) // neg
            p->pVars[ pMapVars2Nums[zCube->index/2] ].Neg = 1;
        else
            p->pVars[ pMapVars2Nums[zCube->index/2] ].Pos = 1;
        // count the unate vars
        p->nUnate++;

        // update the cuver and deref the cube
        zSet = Cudd_zddDiff( dd, zTemp = zSet, zCube );     Cudd_Ref( zSet );
        Cudd_RecursiveDerefZdd( dd, zTemp );
        Cudd_RecursiveDerefZdd( dd, zCube );

    } // for each cube 
    Cudd_RecursiveDerefZdd( dd, zSet );
    ABC_FREE( pMapVars2Nums );
    return p;

} /* end of Extra_UnateInfoCreateFromZdd */


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

  Synopsis    [Computes the classical unateness information for the function.]

  Description [Uses the naive way of comparing cofactors.]

  SideEffects []

  SeeAlso     []

******************************************************************************/
Extra_UnateInfo_t * Extra_UnateComputeSlow( DdManager * dd, DdNode * bFunc )
{
    int nSuppSize;
    DdNode * bSupp, * bTemp;
    Extra_UnateInfo_t * p;
    int i, Res;

    // compute the support
    bSupp = Cudd_Support( dd, bFunc );   Cudd_Ref( bSupp );
    nSuppSize = Extra_bddSuppSize( dd, bSupp );
//printf( "Support = %d. ", nSuppSize );
//Extra_bddPrint( dd, bSupp );
//printf( "%d ", nSuppSize );

    // allocate the storage for symmetry info
    p = Extra_UnateInfoAllocate( nSuppSize );

    // assign the variables
    p->nVarsMax = dd->size;
    for ( i = 0, bTemp = bSupp; bTemp != b1; bTemp = cuddT(bTemp), i++ )
    {
        Res = Extra_bddCheckUnateNaive( dd, bFunc, bTemp->index );
        p->pVars[i].iVar = bTemp->index;
        if ( Res == -1 )
            p->pVars[i].Neg = 1;
        else if ( Res == 1 )
            p->pVars[i].Pos = 1;
        p->nUnate += (Res != 0);
    }
    Cudd_RecursiveDeref( dd, bSupp );
    return p;

} /* end of Extra_UnateComputeSlow */

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

  Synopsis    [Checks if the two variables are symmetric.]

  Description [Returns 0 if vars are not unate. Return -1/+1 if the var is neg/pos unate.]

  SideEffects []

  SeeAlso     []

******************************************************************************/
int Extra_bddCheckUnateNaive( 
  DdManager * dd,   /* the DD manager */
  DdNode * bF,
  int iVar) 
{
    DdNode * bCof0, * bCof1;
    int Res;

    assert( iVar < dd->size );

    bCof0 = Cudd_Cofactor( dd, bF, Cudd_Not(Cudd_bddIthVar(dd,iVar)) );  Cudd_Ref( bCof0 );
    bCof1 = Cudd_Cofactor( dd, bF, Cudd_bddIthVar(dd,iVar) );            Cudd_Ref( bCof1 );

    if ( Cudd_bddLeq( dd, bCof0, bCof1 ) )
        Res = 1;
    else if ( Cudd_bddLeq( dd, bCof1, bCof0 ) )
        Res =-1;
    else
        Res = 0;

    Cudd_RecursiveDeref( dd, bCof0 );
    Cudd_RecursiveDeref( dd, bCof1 );
    return Res;
} /* end of Extra_bddCheckUnateNaive */


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

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

  Synopsis    [Performs a recursive step of Extra_UnateInfoCompute.]

  Description [Returns the set of symmetric variable pairs represented as a set 
  of two-literal ZDD cubes. Both variables always appear in the positive polarity
  in the cubes. This function works without building new BDD nodes. Some relatively 
  small number of ZDD nodes may be built to ensure proper bookkeeping of the 
  symmetry information.]

  SideEffects []

  SeeAlso     []

******************************************************************************/
DdNode * 
extraZddUnateInfoCompute( 
  DdManager * dd,   /* the manager */
  DdNode * bFunc,   /* the function whose symmetries are computed */
  DdNode * bVars )  /* the set of variables on which this function depends */
{
    DdNode * zRes;
    DdNode * bFR = Cudd_Regular(bFunc); 

    if ( cuddIsConstant(bFR) )
    {
        if ( cuddIsConstant(bVars) )
            return z0;
        return extraZddGetSingletonsBoth( dd, bVars );
    }
    assert( bVars != b1 );

    if ( (zRes = cuddCacheLookup2Zdd(dd, extraZddUnateInfoCompute, bFunc, bVars)) )
        return zRes;
    else
    {
        DdNode * zRes0, * zRes1;
        DdNode * zTemp, * zPlus;             
        DdNode * bF0, * bF1;             
        DdNode * bVarsNew;
        int nVarsExtra;
        int LevelF;
        int AddVar;

        // every variable in bF should be also in bVars, therefore LevelF cannot be above LevelV
        // if LevelF is below LevelV, scroll through the vars in bVars to the same level as F
        // count how many extra vars are there in bVars
        nVarsExtra = 0;
        LevelF = dd->perm[bFR->index];
        for ( bVarsNew = bVars; LevelF > dd->perm[bVarsNew->index]; bVarsNew = cuddT(bVarsNew) )
            nVarsExtra++; 
        // the indexes (level) of variables should be synchronized now
        assert( bFR->index == bVarsNew->index );

        // cofactor the function
        if ( bFR != bFunc ) // bFunc is complemented 
        {
            bF0 = Cudd_Not( cuddE(bFR) );
            bF1 = Cudd_Not( cuddT(bFR) );
        }
        else
        {
            bF0 = cuddE(bFR);
            bF1 = cuddT(bFR);
        }

        // solve subproblems
        zRes0 = extraZddUnateInfoCompute( dd, bF0, cuddT(bVarsNew) );
        if ( zRes0 == NULL )
            return NULL;
        cuddRef( zRes0 );

        // if there is no symmetries in the negative cofactor
        // there is no need to test the positive cofactor
        if ( zRes0 == z0 )
            zRes = zRes0;  // zRes takes reference
        else
        {
            zRes1 = extraZddUnateInfoCompute( dd, bF1, cuddT(bVarsNew) );
            if ( zRes1 == NULL )
            {
                Cudd_RecursiveDerefZdd( dd, zRes0 );
                return NULL;
            }
            cuddRef( zRes1 );

            // only those variables are pair-wise symmetric 
            // that are pair-wise symmetric in both cofactors
            // therefore, intersect the solutions
            zRes = cuddZddIntersect( dd, zRes0, zRes1 );
            if ( zRes == NULL )
            {
                Cudd_RecursiveDerefZdd( dd, zRes0 );
                Cudd_RecursiveDerefZdd( dd, zRes1 );
                return NULL;
            }
            cuddRef( zRes );
            Cudd_RecursiveDerefZdd( dd, zRes0 );
            Cudd_RecursiveDerefZdd( dd, zRes1 );
        }

        // consider the current top-most variable
        AddVar = -1;
        if ( Cudd_bddLeq( dd, bF0, bF1 ) ) // pos
            AddVar = 0;
        else if ( Cudd_bddLeq( dd, bF1, bF0 ) ) // neg
            AddVar = 1;
        if ( AddVar >= 0 )
        {
            // create the singleton
            zPlus = cuddZddGetNode( dd, 2*bFR->index + AddVar, z1, z0 );
            if ( zPlus == NULL ) 
            {
                Cudd_RecursiveDerefZdd( dd, zRes );
                return NULL;
            }
            cuddRef( zPlus );

            // add these to the result
            zRes = cuddZddUnion( dd, zTemp = zRes, zPlus );
            if ( zRes == NULL )
            {
                Cudd_RecursiveDerefZdd( dd, zTemp );
                Cudd_RecursiveDerefZdd( dd, zPlus );
                return NULL;
            }
            cuddRef( zRes );
            Cudd_RecursiveDerefZdd( dd, zTemp );
            Cudd_RecursiveDerefZdd( dd, zPlus );
        }
        // only zRes is referenced at this point

        // if we skipped some variables, these variables cannot be symmetric with
        // any variables that are currently in the support of bF, but they can be 
        // symmetric with the variables that are in bVars but not in the support of bF
        for ( bVarsNew = bVars; LevelF > dd->perm[bVarsNew->index]; bVarsNew = cuddT(bVarsNew) )
        {
            // create the negative singleton
            zPlus = cuddZddGetNode( dd, 2*bVarsNew->index+1, z1, z0 );
            if ( zPlus == NULL ) 
            {
                Cudd_RecursiveDerefZdd( dd, zRes );
                return NULL;
            }
            cuddRef( zPlus );

            // add these to the result
            zRes = cuddZddUnion( dd, zTemp = zRes, zPlus );
            if ( zRes == NULL )
            {
                Cudd_RecursiveDerefZdd( dd, zTemp );
                Cudd_RecursiveDerefZdd( dd, zPlus );
                return NULL;
            }
            cuddRef( zRes );
            Cudd_RecursiveDerefZdd( dd, zTemp );
            Cudd_RecursiveDerefZdd( dd, zPlus );
        

            // create the positive singleton
            zPlus = cuddZddGetNode( dd, 2*bVarsNew->index, z1, z0 );
            if ( zPlus == NULL ) 
            {
                Cudd_RecursiveDerefZdd( dd, zRes );
                return NULL;
            }
            cuddRef( zPlus );

            // add these to the result
            zRes = cuddZddUnion( dd, zTemp = zRes, zPlus );
            if ( zRes == NULL )
            {
                Cudd_RecursiveDerefZdd( dd, zTemp );
                Cudd_RecursiveDerefZdd( dd, zPlus );
                return NULL;
            }
            cuddRef( zRes );
            Cudd_RecursiveDerefZdd( dd, zTemp );
            Cudd_RecursiveDerefZdd( dd, zPlus );
        }
        cuddDeref( zRes );

        /* insert the result into cache */
        cuddCacheInsert2(dd, extraZddUnateInfoCompute, bFunc, bVars, zRes);
        return zRes;
    }
} /* end of extraZddUnateInfoCompute */


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

  Synopsis    [Performs a recursive step of Extra_zddGetSingletons.]

  Description [Returns the set of ZDD singletons, containing those pos/neg 
  polarity ZDD variables that correspond to the BDD variables in bVars.]

  SideEffects []

  SeeAlso     []

******************************************************************************/
DdNode * extraZddGetSingletonsBoth( 
  DdManager * dd,    /* the DD manager */
  DdNode * bVars)    /* the set of variables */
{
    DdNode * zRes;

    if ( bVars == b1 )
        return z1;

    if ( (zRes = cuddCacheLookup1Zdd(dd, extraZddGetSingletonsBoth, bVars)) )
        return zRes;
    else
    {
        DdNode * zTemp, * zPlus;          

        // solve subproblem
        zRes = extraZddGetSingletonsBoth( dd, cuddT(bVars) );
        if ( zRes == NULL ) 
            return NULL;
        cuddRef( zRes );

        
        // create the negative singleton
        zPlus = cuddZddGetNode( dd, 2*bVars->index+1, z1, z0 );
        if ( zPlus == NULL ) 
        {
            Cudd_RecursiveDerefZdd( dd, zRes );
            return NULL;
        }
        cuddRef( zPlus );

        // add these to the result
        zRes = cuddZddUnion( dd, zTemp = zRes, zPlus );
        if ( zRes == NULL )
        {
            Cudd_RecursiveDerefZdd( dd, zTemp );
            Cudd_RecursiveDerefZdd( dd, zPlus );
            return NULL;
        }
        cuddRef( zRes );
        Cudd_RecursiveDerefZdd( dd, zTemp );
        Cudd_RecursiveDerefZdd( dd, zPlus );
        

        // create the positive singleton
        zPlus = cuddZddGetNode( dd, 2*bVars->index, z1, z0 );
        if ( zPlus == NULL ) 
        {
            Cudd_RecursiveDerefZdd( dd, zRes );
            return NULL;
        }
        cuddRef( zPlus );

        // add these to the result
        zRes = cuddZddUnion( dd, zTemp = zRes, zPlus );
        if ( zRes == NULL )
        {
            Cudd_RecursiveDerefZdd( dd, zTemp );
            Cudd_RecursiveDerefZdd( dd, zPlus );
            return NULL;
        }
        cuddRef( zRes );
        Cudd_RecursiveDerefZdd( dd, zTemp );
        Cudd_RecursiveDerefZdd( dd, zPlus );

        cuddDeref( zRes );
        cuddCacheInsert1( dd, extraZddGetSingletonsBoth, bVars, zRes );
        return zRes;
    }
}   /* end of extraZddGetSingletonsBoth */


/*---------------------------------------------------------------------------*/
/* Definition of static Functions                                            */
/*---------------------------------------------------------------------------*/
ABC_NAMESPACE_IMPL_END