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

  FileName    [abcMv.c]

  SystemName  [ABC: Logic synthesis and verification system.]

  PackageName [Network and node package.]

  Synopsis    [Multi-valued decomposition.]

  Author      [Alan Mishchenko]
  
  Affiliation [UC Berkeley]

  Date        [Ver. 1.0. Started - June 20, 2005.]

  Revision    [$Id: abcMv.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]

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

#include "base/abc/abc.h"
#include "misc/extra/extraBdd.h"

ABC_NAMESPACE_IMPL_START


////////////////////////////////////////////////////////////////////////
///                        DECLARATIONS                              ///
////////////////////////////////////////////////////////////////////////

typedef struct Mv_Man_t_ Mv_Man_t;
struct Mv_Man_t_
{
    int         nInputs;          // the number of 4-valued input variables
    int         nFuncs;           // the number of 4-valued functions
    DdManager * dd;               // representation of functions
    DdNode *    bValues[15][4];   // representation of i-sets
    DdNode *    bValueDcs[15][4]; // representation of i-sets don't-cares
    DdNode *    bFuncs[15];       // representation of functions
};

static void     Abc_MvDecompose( Mv_Man_t * p );
static void     Abc_MvPrintStats( Mv_Man_t * p );
static void     Abc_MvRead( Mv_Man_t * p );
static void     Abc_MvDeref( Mv_Man_t * p );
static DdNode * Abc_MvReadCube( DdManager * dd, char * pLine, int nVars );

////////////////////////////////////////////////////////////////////////
///                     FUNCTION DEFINITIONS                         ///
////////////////////////////////////////////////////////////////////////

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

  Synopsis    []

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
void Abc_MvExperiment()
{
    Mv_Man_t * p;
    // get the functions
    p = ABC_ALLOC( Mv_Man_t, 1 );
    memset( p, 0, sizeof(Mv_Man_t) );
    p->dd = Cudd_Init( 32, 0, CUDD_UNIQUE_SLOTS, CUDD_CACHE_SLOTS, 0 );
    p->nFuncs  = 15;
    p->nInputs =  9;
    Abc_MvRead( p );
    // process the functions
    Abc_MvPrintStats( p );
//    Cudd_ReduceHeap( p->dd, CUDD_REORDER_SYMM_SIFT, 1 );
//    Abc_MvPrintStats( p );
    // try detecting support reducing bound set
    Abc_MvDecompose( p );

    // remove the manager
    Abc_MvDeref( p );
    Extra_StopManager( p->dd );
    ABC_FREE( p );
}

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

  Synopsis    []

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
void Abc_MvPrintStats( Mv_Man_t * p )
{
    int i, v;
    for ( i = 0; i < 15; i++ )
    {
        printf( "%2d : ", i );
        printf( "%3d (%2d)    ", Cudd_DagSize(p->bFuncs[i])-1, Cudd_SupportSize(p->dd, p->bFuncs[i]) );
        for ( v = 0; v < 4; v++ )
            printf( "%d = %3d (%2d)  ", v, Cudd_DagSize(p->bValues[i][v])-1, Cudd_SupportSize(p->dd, p->bValues[i][v]) );
        printf( "\n" );
    }
}

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

  Synopsis    []

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
DdNode * Abc_MvReadCube( DdManager * dd, char * pLine, int nVars )
{
    DdNode * bCube, * bVar, * bTemp;
    int i;
    bCube = Cudd_ReadOne(dd);  Cudd_Ref( bCube );
    for ( i = 0; i < nVars; i++ )
    {
        if ( pLine[i] == '-' )
            continue;
        else if ( pLine[i] == '0' ) // 0
            bVar = Cudd_Not( Cudd_bddIthVar(dd, 29-i) );
        else if ( pLine[i] == '1' ) // 1
            bVar = Cudd_bddIthVar(dd, 29-i);
        else assert(0);
        bCube = Cudd_bddAnd( dd, bTemp = bCube, bVar );  Cudd_Ref( bCube );
        Cudd_RecursiveDeref( dd, bTemp );
    }
    Cudd_Deref( bCube );
    return bCube;
}

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

  Synopsis    []

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
void Abc_MvRead( Mv_Man_t * p )
{
    FILE * pFile;
    char Buffer[1000], * pLine;
    DdNode * bCube, * bTemp, * bProd, * bVar0, * bVar1, * bCubeSum;
    int i, v;

    // start the cube
    bCubeSum = Cudd_ReadLogicZero(p->dd);  Cudd_Ref( bCubeSum );

    // start the values
    for ( i = 0; i < 15; i++ )
    for ( v = 0; v < 4; v++ )
    {
        p->bValues[i][v]   = Cudd_ReadLogicZero(p->dd);  Cudd_Ref( p->bValues[i][v] );
        p->bValueDcs[i][v] = Cudd_ReadLogicZero(p->dd);  Cudd_Ref( p->bValueDcs[i][v] );
    }

    // read the file
    pFile = fopen( "input.pla", "r" );
    while ( fgets( Buffer, 1000, pFile ) )
    {
        if ( Buffer[0] == '#' )
            continue;
        if ( Buffer[0] == '.' )
        {
            if ( Buffer[1] == 'e' )
                break;
            continue;
        }

        // get the cube 
        bCube = Abc_MvReadCube( p->dd, Buffer, 18 );  Cudd_Ref( bCube );

        // add it to the values of the output functions
        pLine = Buffer + 19;
        for ( i = 0; i < 15; i++ )
        {
            if ( pLine[2*i] == '-' && pLine[2*i+1] == '-' )
            {
                for ( v = 0; v < 4; v++ )
                {
                    p->bValueDcs[i][v] = Cudd_bddOr( p->dd, bTemp = p->bValueDcs[i][v], bCube );  Cudd_Ref( p->bValueDcs[i][v] );
                    Cudd_RecursiveDeref( p->dd, bTemp );
                }
                continue;
            }
            else if ( pLine[2*i] == '0' && pLine[2*i+1] == '0' ) // 0
                v = 0;
            else if ( pLine[2*i] == '1' && pLine[2*i+1] == '0' ) // 1
                v = 1;
            else if ( pLine[2*i] == '0' && pLine[2*i+1] == '1' ) // 2
                v = 2;
            else if ( pLine[2*i] == '1' && pLine[2*i+1] == '1' ) // 3
                v = 3;
            else assert( 0 );
            // add the value
            p->bValues[i][v] = Cudd_bddOr( p->dd, bTemp = p->bValues[i][v], bCube );  Cudd_Ref( p->bValues[i][v] );
            Cudd_RecursiveDeref( p->dd, bTemp );
        }

        // add the cube
        bCubeSum = Cudd_bddOr( p->dd, bTemp = bCubeSum, bCube );  Cudd_Ref( bCubeSum );
        Cudd_RecursiveDeref( p->dd, bTemp );
        Cudd_RecursiveDeref( p->dd, bCube );
    }

    // add the complement of the domain to all values
    for ( i = 0; i < 15; i++ )
        for ( v = 0; v < 4; v++ )
        {
            if ( p->bValues[i][v] == Cudd_Not(Cudd_ReadOne(p->dd)) )
                continue;
            p->bValues[i][v] = Cudd_bddOr( p->dd, bTemp = p->bValues[i][v], p->bValueDcs[i][v] );  Cudd_Ref( p->bValues[i][v] );
            Cudd_RecursiveDeref( p->dd, bTemp );
            p->bValues[i][v] = Cudd_bddOr( p->dd, bTemp = p->bValues[i][v], Cudd_Not(bCubeSum) );  Cudd_Ref( p->bValues[i][v] );
            Cudd_RecursiveDeref( p->dd, bTemp );
        }
    printf( "Domain = %5.2f %%.\n", 100.0*Cudd_CountMinterm(p->dd, bCubeSum, 32)/Cudd_CountMinterm(p->dd, Cudd_ReadOne(p->dd), 32) ); 
    Cudd_RecursiveDeref( p->dd, bCubeSum );

    // create each output function
    for ( i = 0; i < 15; i++ )
    {
        p->bFuncs[i] = Cudd_ReadLogicZero(p->dd);  Cudd_Ref( p->bFuncs[i] );
        for ( v = 0; v < 4; v++ )
        {
            bVar0 = Cudd_NotCond( Cudd_bddIthVar(p->dd, 30), ((v & 1) == 0) );
            bVar1 = Cudd_NotCond( Cudd_bddIthVar(p->dd, 31), ((v & 2) == 0) );
            bCube = Cudd_bddAnd( p->dd, bVar0, bVar1 );             Cudd_Ref( bCube );
            bProd = Cudd_bddAnd( p->dd, p->bValues[i][v], bCube );  Cudd_Ref( bProd );
            Cudd_RecursiveDeref( p->dd, bCube );
            // add the value
            p->bFuncs[i] = Cudd_bddOr( p->dd, bTemp = p->bFuncs[i], bProd );  Cudd_Ref( p->bFuncs[i] );
            Cudd_RecursiveDeref( p->dd, bTemp );
            Cudd_RecursiveDeref( p->dd, bProd );
        }
    }
}

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

  Synopsis    []

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
void Abc_MvDeref( Mv_Man_t * p )
{
    int i, v;
    for ( i = 0; i < 15; i++ )
    for ( v = 0; v < 4; v++ )
    {
        Cudd_RecursiveDeref( p->dd, p->bValues[i][v] );
        Cudd_RecursiveDeref( p->dd, p->bValueDcs[i][v] );
    }
    for ( i = 0; i < 15; i++ )
        Cudd_RecursiveDeref( p->dd, p->bFuncs[i] );
}



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

  Synopsis    []

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
void Abc_MvDecompose( Mv_Man_t * p )
{
    DdNode * bCofs[16], * bVarCube1, * bVarCube2, * bVarCube, * bCube, * bVar0, * bVar1;//, * bRes;
    int k, i1, i2, v1, v2;//, c1, c2, Counter;

    bVar0 = Cudd_bddIthVar(p->dd, 30);
    bVar1 = Cudd_bddIthVar(p->dd, 31);
    bCube = Cudd_bddAnd( p->dd, bVar0, bVar1 );  Cudd_Ref( bCube );

    for ( k = 0; k < p->nFuncs; k++ )
    {
        printf( "FUNCTION %d\n", k );
        for ( i1 = 0; i1 < p->nFuncs; i1++ )
        for ( i2 = i1+1; i2 < p->nFuncs; i2++ )
        {
            Vec_Ptr_t * vCofs;

            for ( v1 = 0; v1 < 4; v1++ )
            {
                bVar0 = Cudd_NotCond( Cudd_bddIthVar(p->dd, 29-2*i1  ), ((v1 & 1) == 0) );
                bVar1 = Cudd_NotCond( Cudd_bddIthVar(p->dd, 29-2*i1-1), ((v1 & 2) == 0) );
                bVarCube1 = Cudd_bddAnd( p->dd, bVar0, bVar1 );  Cudd_Ref( bVarCube1 );
                for ( v2 = 0; v2 < 4; v2++ )
                {
                    bVar0 = Cudd_NotCond( Cudd_bddIthVar(p->dd, 29-2*i2  ), ((v2 & 1) == 0) );
                    bVar1 = Cudd_NotCond( Cudd_bddIthVar(p->dd, 29-2*i2-1), ((v2 & 2) == 0) );
                    bVarCube2 = Cudd_bddAnd( p->dd, bVar0, bVar1 );         Cudd_Ref( bVarCube2 );
                    bVarCube = Cudd_bddAnd( p->dd, bVarCube1, bVarCube2 );  Cudd_Ref( bVarCube );
                    bCofs[v1 * 4 + v2] = Cudd_Cofactor( p->dd, p->bFuncs[k], bVarCube );  Cudd_Ref( bCofs[v1 * 4 + v2] );
                    Cudd_RecursiveDeref( p->dd, bVarCube );
                    Cudd_RecursiveDeref( p->dd, bVarCube2 );
                }
                Cudd_RecursiveDeref( p->dd, bVarCube1 );
            }
/*
            // check the compatibility of cofactors
            Counter = 0;
            for ( c1 = 0; c1 < 16; c1++ )
            {
                for ( c2 = 0; c2 <= c1; c2++ )
                    printf( " " );
                for ( c2 = c1+1; c2 < 16; c2++ )
                {
                    bRes = Cudd_bddAndAbstract( p->dd, bCofs[c1], bCofs[c2], bCube );  Cudd_Ref( bRes );
                    if ( bRes == Cudd_ReadOne(p->dd) )
                    {
                        printf( "+" );
                        Counter++;
                    }
                    else
                    {
                        printf( " " );
                    }
                    Cudd_RecursiveDeref( p->dd, bRes );
                }
                printf( "\n" );
            }
*/

            vCofs = Vec_PtrAlloc( 16 );
            for ( v1 = 0; v1 < 4; v1++ )
            for ( v2 = 0; v2 < 4; v2++ )
                Vec_PtrPushUnique( vCofs, bCofs[v1 * 4 + v2] );
            printf( "%d ", Vec_PtrSize(vCofs) );
            Vec_PtrFree( vCofs );

            // free the cofactors
            for ( v1 = 0; v1 < 4; v1++ )
            for ( v2 = 0; v2 < 4; v2++ )
                Cudd_RecursiveDeref( p->dd, bCofs[v1 * 4 + v2] );

            printf( "\n" );
//            printf( "%2d, %2d : %3d\n", i1, i2, Counter );
        }
    }

    Cudd_RecursiveDeref( p->dd, bCube );
}

////////////////////////////////////////////////////////////////////////
///                       END OF FILE                                ///
////////////////////////////////////////////////////////////////////////


ABC_NAMESPACE_IMPL_END