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

  FileName    [abcFunc.c]

  SystemName  [ABC: Logic synthesis and verification system.]

  PackageName [Network and node package.]

  Synopsis    [Transformations between different functionality representations.]

  Author      [Alan Mishchenko]
  
  Affiliation [UC Berkeley]

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

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

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

#include "abc.h"
#include "main.h"
#include "mio.h"

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

#define ABC_MUX_CUBES   100000

static int Abc_ConvertZddToSop( DdManager * dd, DdNode * zCover, char * pSop, int nFanins, Vec_Str_t * vCube, int fPhase );
static DdNode * Abc_ConvertAigToBdd( DdManager * dd, Hop_Obj_t * pRoot);
static Hop_Obj_t * Abc_ConvertSopToAig( Hop_Man_t * pMan, char * pSop );

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

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

  Synopsis    [Converts the network from SOP to BDD representation.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
int Abc_NtkSopToBdd( Abc_Ntk_t * pNtk )
{
    Abc_Obj_t * pNode;
    DdManager * dd;
    int nFaninsMax, i;
 
    assert( Abc_NtkHasSop(pNtk) ); 

    // start the functionality manager
    nFaninsMax = Abc_NtkGetFaninMax( pNtk );
    if ( nFaninsMax == 0 )
        fprintf(outStream,  "Warning: The network has only constant nodes.\n" );

    dd = Cudd_Init( nFaninsMax, 0, CUDD_UNIQUE_SLOTS, CUDD_CACHE_SLOTS, 0 );

    // convert each node from SOP to BDD
    Abc_NtkForEachNode( pNtk, pNode, i )
    {
        assert( pNode->pData );
        pNode->pData = Abc_ConvertSopToBdd( dd, pNode->pData );
        if ( pNode->pData == NULL )
        {
            fprintf(outStream,  "Abc_NtkSopToBdd: Error while converting SOP into BDD.\n" );
            return 0;
        }
        Cudd_Ref( pNode->pData );
    }

    Extra_MmFlexStop( pNtk->pManFunc );
    pNtk->pManFunc = dd;

    // update the network type
    pNtk->ntkFunc = ABC_FUNC_BDD;
    return 1;
}

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

  Synopsis    [Converts the node from SOP to BDD representation.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
DdNode * Abc_ConvertSopToBdd( DdManager * dd, char * pSop )
{
    DdNode * bSum, * bCube, * bTemp, * bVar;
    char * pCube;
    int nVars, Value, v;

    // start the cover
    nVars = Abc_SopGetVarNum(pSop);
    bSum = Cudd_ReadLogicZero(dd);   Cudd_Ref( bSum );
    if ( Abc_SopIsExorType(pSop) )
    {
        for ( v = 0; v < nVars; v++ )
        {
            bSum  = Cudd_bddXor( dd, bTemp = bSum, Cudd_bddIthVar(dd, v) );   Cudd_Ref( bSum );
            Cudd_RecursiveDeref( dd, bTemp );
        }
    }
    else
    {
        // check the logic function of the node
        Abc_SopForEachCube( pSop, nVars, pCube )
        {
            bCube = Cudd_ReadOne(dd);   Cudd_Ref( bCube );
            Abc_CubeForEachVar( pCube, Value, v )
            {
                if ( Value == '0' )
                    bVar = Cudd_Not( Cudd_bddIthVar( dd, v ) );
                else if ( Value == '1' )
                    bVar = Cudd_bddIthVar( dd, v );
                else
                    continue;
                bCube  = Cudd_bddAnd( dd, bTemp = bCube, bVar );   Cudd_Ref( bCube );
                Cudd_RecursiveDeref( dd, bTemp );
            }
            bSum = Cudd_bddOr( dd, bTemp = bSum, bCube );   
            Cudd_Ref( bSum );
            Cudd_RecursiveDeref( dd, bTemp );
            Cudd_RecursiveDeref( dd, bCube );
        }
    }
    // complement the result if necessary
    bSum = Cudd_NotCond( bSum, !Abc_SopGetPhase(pSop) );
    Cudd_Deref( bSum );
    return bSum;
}

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

  Synopsis    [Removes complemented SOP covers.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
void Abc_NtkLogicMakeDirectSops( Abc_Ntk_t * pNtk )
{
    DdManager * dd;
    DdNode * bFunc;
    Vec_Str_t * vCube;
    Abc_Obj_t * pNode;
    int nFaninsMax, fFound, i;

    assert( Abc_NtkHasSop(pNtk) );

    // check if there are nodes with complemented SOPs
    fFound = 0;
    Abc_NtkForEachNode( pNtk, pNode, i )
        if ( Abc_SopIsComplement(pNode->pData) )
        {
            fFound = 1;
            break;
        }
    if ( !fFound )
        return;

    // start the BDD package
    nFaninsMax = Abc_NtkGetFaninMax( pNtk );
    if ( nFaninsMax == 0 )
        fprintf(outStream,  "Warning: The network has only constant nodes.\n" );
    dd = Cudd_Init( nFaninsMax, 0, CUDD_UNIQUE_SLOTS, CUDD_CACHE_SLOTS, 0 );

    // change the cover of negated nodes
    vCube = Vec_StrAlloc( 100 );
    Abc_NtkForEachNode( pNtk, pNode, i )
        if ( Abc_SopIsComplement(pNode->pData) )
        {
            bFunc = Abc_ConvertSopToBdd( dd, pNode->pData );  Cudd_Ref( bFunc );
            pNode->pData = Abc_ConvertBddToSop( pNtk->pManFunc, dd, bFunc, bFunc, Abc_ObjFaninNum(pNode), 0, vCube, 1 );
            Cudd_RecursiveDeref( dd, bFunc );
            assert( !Abc_SopIsComplement(pNode->pData) );
        }
    Vec_StrFree( vCube );
    Extra_StopManager( dd );
}





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

  Synopsis    [Converts the network from BDD to SOP representation.]

  Description [If the flag is set to 1, forces the direct phase of all covers.]
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
int Abc_NtkBddToSop( Abc_Ntk_t * pNtk, int fDirect )
{
    Abc_Obj_t * pNode;
    Extra_MmFlex_t * pManNew;
    DdManager * dd = pNtk->pManFunc;
    DdNode * bFunc;
    Vec_Str_t * vCube;
    int i, fMode;

    if ( fDirect )
        fMode = 1;
    else
        fMode = -1;

    assert( Abc_NtkHasBdd(pNtk) );
    if ( dd->size > 0 )
    Cudd_zddVarsFromBddVars( dd, 2 );
    // create the new manager
    pManNew = Extra_MmFlexStart();

    // go through the objects
    vCube = Vec_StrAlloc( 100 );
    Abc_NtkForEachNode( pNtk, pNode, i )
    {
        assert( pNode->pData );
        bFunc = pNode->pData;
        pNode->pNext = (Abc_Obj_t *)Abc_ConvertBddToSop( pManNew, dd, bFunc, bFunc, Abc_ObjFaninNum(pNode), 0, vCube, fMode );
        if ( pNode->pNext == NULL )
        {
            Extra_MmFlexStop( pManNew );
            Abc_NtkCleanNext( pNtk );
//            fprintf(outStream,  "Converting from BDDs to SOPs has failed.\n" );
            Vec_StrFree( vCube );
            return 0;
        }
    }
    Vec_StrFree( vCube );

    // update the network type
    pNtk->ntkFunc = ABC_FUNC_SOP;
    // set the new manager
    pNtk->pManFunc = pManNew;
    // transfer from next to data
    Abc_NtkForEachNode( pNtk, pNode, i )
    {
        Cudd_RecursiveDeref( dd, pNode->pData );
        pNode->pData = pNode->pNext;
        pNode->pNext = NULL;
    }

    // check for remaining references in the package
    Extra_StopManager( dd );
    return 1;
}

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

  Synopsis    [Converts the node from BDD to SOP representation.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
char * Abc_ConvertBddToSop( Extra_MmFlex_t * pMan, DdManager * dd, DdNode * bFuncOn, DdNode * bFuncOnDc, int nFanins, int fAllPrimes, Vec_Str_t * vCube, int fMode )
{
    int fVerify = 0;
    char * pSop;
    DdNode * bFuncNew, * bCover, * zCover, * zCover0, * zCover1;
    int nCubes, nCubes0, nCubes1, fPhase;

    assert( bFuncOn == bFuncOnDc || Cudd_bddLeq( dd, bFuncOn, bFuncOnDc ) );
    if ( Cudd_IsConstant(bFuncOn) || Cudd_IsConstant(bFuncOnDc) )
    {
        if ( fMode == -1 ) // if the phase is not known, write constant 1
            fMode = 1;
        Vec_StrFill( vCube, nFanins, '-' );
        Vec_StrPush( vCube, '\0' );
        if ( pMan )
            pSop = Extra_MmFlexEntryFetch( pMan, nFanins + 4 );
        else
            pSop = ALLOC( char, nFanins + 4 );
        if ( bFuncOn == Cudd_ReadOne(dd) )
            sprintf( pSop, "%s %d\n", vCube->pArray, fMode );
        else
            sprintf( pSop, "%s %d\n", vCube->pArray, !fMode );
        return pSop;
    }


    if ( fMode == -1 )
    { // try both phases
        assert( fAllPrimes == 0 );

        // get the ZDD of the negative polarity
        bCover = Cudd_zddIsop( dd, Cudd_Not(bFuncOnDc), Cudd_Not(bFuncOn), &zCover0 );
        Cudd_Ref( zCover0 );
        Cudd_Ref( bCover );
        Cudd_RecursiveDeref( dd, bCover );
        nCubes0 = Abc_CountZddCubes( dd, zCover0 );

        // get the ZDD of the positive polarity
        bCover = Cudd_zddIsop( dd, bFuncOn, bFuncOnDc, &zCover1 );
        Cudd_Ref( zCover1 );
        Cudd_Ref( bCover );
        Cudd_RecursiveDeref( dd, bCover );
        nCubes1 = Abc_CountZddCubes( dd, zCover1 );

        // compare the number of cubes
        if ( nCubes1 <= nCubes0 )
        { // use positive polarity
            nCubes = nCubes1;
            zCover = zCover1;
            Cudd_RecursiveDerefZdd( dd, zCover0 );
            fPhase = 1;
        }
        else
        { // use negative polarity
            nCubes = nCubes0;
            zCover = zCover0;
            Cudd_RecursiveDerefZdd( dd, zCover1 );
            fPhase = 0;
        }
    }
    else if ( fMode == 0 )
    {
        // get the ZDD of the negative polarity
        if ( fAllPrimes )
        {
            zCover = Extra_zddPrimes( dd, Cudd_Not(bFuncOnDc) ); 
            Cudd_Ref( zCover );
        }
        else
        {
            bCover = Cudd_zddIsop( dd, Cudd_Not(bFuncOnDc), Cudd_Not(bFuncOn), &zCover );
            Cudd_Ref( zCover );
            Cudd_Ref( bCover );
            Cudd_RecursiveDeref( dd, bCover );
        }
        nCubes = Abc_CountZddCubes( dd, zCover );
        fPhase = 0;
    }
    else if ( fMode == 1 )
    {
        // get the ZDD of the positive polarity
        if ( fAllPrimes )
        {
            zCover = Extra_zddPrimes( dd, bFuncOnDc ); 
            Cudd_Ref( zCover );
        }
        else
        {
            bCover = Cudd_zddIsop( dd, bFuncOn, bFuncOnDc, &zCover );
            Cudd_Ref( zCover );
            Cudd_Ref( bCover );
            Cudd_RecursiveDeref( dd, bCover );
        }
        nCubes = Abc_CountZddCubes( dd, zCover );
        fPhase = 1;
    }
    else
    {
        assert( 0 );
    }

    if ( nCubes > ABC_MUX_CUBES )
    {
        Cudd_RecursiveDerefZdd( dd, zCover );
        fprintf(outStream,  "The number of cubes exceeded the predefined limit (%d).\n", ABC_MUX_CUBES );
        return NULL;
    }

    // allocate memory for the cover
    if ( pMan )
        pSop = Extra_MmFlexEntryFetch( pMan, (nFanins + 3) * nCubes + 1 );
    else 
        pSop = ALLOC( char, (nFanins + 3) * nCubes + 1 );
    pSop[(nFanins + 3) * nCubes] = 0;
    // create the SOP
    Vec_StrFill( vCube, nFanins, '-' );
    Vec_StrPush( vCube, '\0' );
    Abc_ConvertZddToSop( dd, zCover, pSop, nFanins, vCube, fPhase );
    Cudd_RecursiveDerefZdd( dd, zCover );

    // verify
    if ( fVerify )
    {
        bFuncNew = Abc_ConvertSopToBdd( dd, pSop );  Cudd_Ref( bFuncNew );
        if ( bFuncOn == bFuncOnDc )
        {
            if ( bFuncNew != bFuncOn )
                fprintf(outStream,  "Verification failed.\n" );
        }
        else
        {
            if ( !Cudd_bddLeq(dd, bFuncOn, bFuncNew) || !Cudd_bddLeq(dd, bFuncNew, bFuncOnDc) )
                fprintf(outStream,  "Verification failed.\n" );
        }
        Cudd_RecursiveDeref( dd, bFuncNew );
    }
    return pSop;
}

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

  Synopsis    [Derive the SOP from the ZDD representation of the cubes.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
void Abc_ConvertZddToSop_rec( DdManager * dd, DdNode * zCover, char * pSop, int nFanins, Vec_Str_t * vCube, int fPhase, int * pnCubes )
{
    DdNode * zC0, * zC1, * zC2;
    int Index;

    if ( zCover == dd->zero )
        return;
    if ( zCover == dd->one )
    {
        char * pCube;
        pCube = pSop + (*pnCubes) * (nFanins + 3);
        sprintf( pCube, "%s %d\n", vCube->pArray, fPhase );
        (*pnCubes)++;
        return;
    }
    Index = zCover->index/2;
    assert( Index < nFanins );
    extraDecomposeCover( dd, zCover, &zC0, &zC1, &zC2 );
    vCube->pArray[Index] = '0';
    Abc_ConvertZddToSop_rec( dd, zC0, pSop, nFanins, vCube, fPhase, pnCubes );
    vCube->pArray[Index] = '1';
    Abc_ConvertZddToSop_rec( dd, zC1, pSop, nFanins, vCube, fPhase, pnCubes );
    vCube->pArray[Index] = '-';
    Abc_ConvertZddToSop_rec( dd, zC2, pSop, nFanins, vCube, fPhase, pnCubes );
}

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

  Synopsis    [Derive the BDD for the function in the cut.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
int Abc_ConvertZddToSop( DdManager * dd, DdNode * zCover, char * pSop, int nFanins, Vec_Str_t * vCube, int fPhase )
{
    int nCubes = 0;
    Abc_ConvertZddToSop_rec( dd, zCover, pSop, nFanins, vCube, fPhase, &nCubes );
    return nCubes;
}


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

  Synopsis    [Computes the SOPs of the negative and positive phase of the node.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
void Abc_NodeBddToCnf( Abc_Obj_t * pNode, Extra_MmFlex_t * pMmMan, Vec_Str_t * vCube, int fAllPrimes, char ** ppSop0, char ** ppSop1 )
{
    assert( Abc_NtkHasBdd(pNode->pNtk) ); 
    *ppSop0 = Abc_ConvertBddToSop( pMmMan, pNode->pNtk->pManFunc, pNode->pData, pNode->pData, Abc_ObjFaninNum(pNode), fAllPrimes, vCube, 0 );
    *ppSop1 = Abc_ConvertBddToSop( pMmMan, pNode->pNtk->pManFunc, pNode->pData, pNode->pData, Abc_ObjFaninNum(pNode), fAllPrimes, vCube, 1 );
}




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

  Synopsis    [Count the number of paths in the ZDD.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
void Abc_CountZddCubes_rec( DdManager * dd, DdNode * zCover, int * pnCubes )
{
    DdNode * zC0, * zC1, * zC2;
    if ( zCover == dd->zero )
        return;
    if ( zCover == dd->one )
    {
        (*pnCubes)++;
        return;
    }
    if ( (*pnCubes) > ABC_MUX_CUBES )
        return;
    extraDecomposeCover( dd, zCover, &zC0, &zC1, &zC2 );
    Abc_CountZddCubes_rec( dd, zC0, pnCubes );
    Abc_CountZddCubes_rec( dd, zC1, pnCubes );
    Abc_CountZddCubes_rec( dd, zC2, pnCubes );
}

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

  Synopsis    [Count the number of paths in the ZDD.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
int Abc_CountZddCubes( DdManager * dd, DdNode * zCover )
{
    int nCubes = 0;
    Abc_CountZddCubes_rec( dd, zCover, &nCubes );
    return nCubes;
}


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

  Synopsis    [Converts the network from SOP to AIG representation.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
int Abc_NtkSopToAig( Abc_Ntk_t * pNtk )
{
    Abc_Obj_t * pNode;
    Hop_Man_t * pMan;
    int i;

    assert( Abc_NtkHasSop(pNtk) ); 

    // start the functionality manager
    pMan = Hop_ManStart();

    // convert each node from SOP to BDD
    Abc_NtkForEachNode( pNtk, pNode, i )
    {
        assert( pNode->pData );
        pNode->pData = Abc_ConvertSopToAig( pMan, pNode->pData );
        if ( pNode->pData == NULL )
        {
            fprintf(outStream,  "Abc_NtkSopToAig: Error while converting SOP into AIG.\n" );
            return 0;
        }
    }
    Extra_MmFlexStop( pNtk->pManFunc );
    pNtk->pManFunc = pMan;

    // update the network type
    pNtk->ntkFunc = ABC_FUNC_AIG;
    return 1;
}


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

  Synopsis    [Strashes one logic node using its SOP.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
Hop_Obj_t * Abc_ConvertSopToAigInternal( Hop_Man_t * pMan, char * pSop )
{
    Hop_Obj_t * pAnd, * pSum;
    int i, Value, nFanins;
    char * pCube;
    // get the number of variables
    nFanins = Abc_SopGetVarNum(pSop);
    // go through the cubes of the node's SOP
    pSum = Hop_ManConst0(pMan);
    Abc_SopForEachCube( pSop, nFanins, pCube )
    {
        // create the AND of literals
        pAnd = Hop_ManConst1(pMan);
        Abc_CubeForEachVar( pCube, Value, i )
        {
            if ( Value == '1' )
                pAnd = Hop_And( pMan, pAnd, Hop_IthVar(pMan,i) );
            else if ( Value == '0' )
                pAnd = Hop_And( pMan, pAnd, Hop_Not(Hop_IthVar(pMan,i)) );
        }
        // add to the sum of cubes
        pSum = Hop_Or( pMan, pSum, pAnd );
    }
    // decide whether to complement the result
    if ( Abc_SopIsComplement(pSop) )
        pSum = Hop_Not(pSum);
    return pSum;
}

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

  Synopsis    [Converts the network from AIG to BDD representation.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
Hop_Obj_t * Abc_ConvertSopToAig( Hop_Man_t * pMan, char * pSop )
{
    extern Hop_Obj_t * Dec_GraphFactorSop( Hop_Man_t * pMan, char * pSop );
    int fUseFactor = 1;
    // consider the constant node
    if ( Abc_SopGetVarNum(pSop) == 0 )
        return Hop_NotCond( Hop_ManConst1(pMan), Abc_SopIsConst0(pSop) );
    // consider the special case of EXOR function
    if ( Abc_SopIsExorType(pSop) )
        return Hop_NotCond( Hop_CreateExor(pMan, Abc_SopGetVarNum(pSop)), Abc_SopIsComplement(pSop) );
    // decide when to use factoring
    if ( fUseFactor && Abc_SopGetVarNum(pSop) > 2 && Abc_SopGetCubeNum(pSop) > 1 )
        return Dec_GraphFactorSop( pMan, pSop );
    return Abc_ConvertSopToAigInternal( pMan, pSop );
}

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

  Synopsis    [Converts the network from AIG to BDD representation.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
int Abc_NtkAigToBdd( Abc_Ntk_t * pNtk )
{
    Abc_Obj_t * pNode;
    Hop_Man_t * pMan;
    DdManager * dd;
    int nFaninsMax, i;

    assert( Abc_NtkHasAig(pNtk) ); 

    // start the functionality manager
    nFaninsMax = Abc_NtkGetFaninMax( pNtk );
    if ( nFaninsMax == 0 )
        fprintf(outStream,  "Warning: The network has only constant nodes.\n" );

    dd = Cudd_Init( nFaninsMax, 0, CUDD_UNIQUE_SLOTS, CUDD_CACHE_SLOTS, 0 );

    // set the mapping of elementary AIG nodes into the elementary BDD nodes
    pMan = pNtk->pManFunc;
    assert( Hop_ManPiNum(pMan) >= nFaninsMax ); 
    for ( i = 0; i < nFaninsMax; i++ )
    {
        Hop_ManPi(pMan, i)->pData = Cudd_bddIthVar(dd, i);
        Cudd_Ref( Hop_ManPi(pMan, i)->pData );
    }

    // convert each node from SOP to BDD
    Abc_NtkForEachNode( pNtk, pNode, i )
    {
        assert( pNode->pData );
        pNode->pData = Abc_ConvertAigToBdd( dd, pNode->pData );
        if ( pNode->pData == NULL )
        {
            fprintf(outStream,  "Abc_NtkSopToBdd: Error while converting SOP into BDD.\n" );
            return 0;
        }
        Cudd_Ref( pNode->pData );
    }

    // dereference intermediate BDD nodes
    for ( i = 0; i < nFaninsMax; i++ )
        Cudd_RecursiveDeref( dd, Hop_ManPi(pMan, i)->pData );

    Hop_ManStop( pNtk->pManFunc );
    pNtk->pManFunc = dd;

    // update the network type
    pNtk->ntkFunc = ABC_FUNC_BDD;
    return 1;
}

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

  Synopsis    [Construct BDDs and mark AIG nodes.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
void Abc_ConvertAigToBdd_rec1( DdManager * dd, Hop_Obj_t * pObj )
{
    assert( !Hop_IsComplement(pObj) );
    if ( !Hop_ObjIsNode(pObj) || Hop_ObjIsMarkA(pObj) )
        return;
    Abc_ConvertAigToBdd_rec1( dd, Hop_ObjFanin0(pObj) ); 
    Abc_ConvertAigToBdd_rec1( dd, Hop_ObjFanin1(pObj) );
    pObj->pData = Cudd_bddAnd( dd, (DdNode *)Hop_ObjChild0Copy(pObj), (DdNode *)Hop_ObjChild1Copy(pObj) ); 
    Cudd_Ref( pObj->pData );
    assert( !Hop_ObjIsMarkA(pObj) ); // loop detection
    Hop_ObjSetMarkA( pObj );
}

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

  Synopsis    [Dereference BDDs and unmark AIG nodes.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
void Abc_ConvertAigToBdd_rec2( DdManager * dd, Hop_Obj_t * pObj )
{
    assert( !Hop_IsComplement(pObj) );
    if ( !Hop_ObjIsNode(pObj) || !Hop_ObjIsMarkA(pObj) )
        return;
    Abc_ConvertAigToBdd_rec2( dd, Hop_ObjFanin0(pObj) ); 
    Abc_ConvertAigToBdd_rec2( dd, Hop_ObjFanin1(pObj) );
    Cudd_RecursiveDeref( dd, pObj->pData );
    pObj->pData = NULL;
    assert( Hop_ObjIsMarkA(pObj) ); // loop detection
    Hop_ObjClearMarkA( pObj );
}

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

  Synopsis    [Converts the network from AIG to BDD representation.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
DdNode * Abc_ConvertAigToBdd( DdManager * dd, Hop_Obj_t * pRoot )
{
    DdNode * bFunc;
    // check the case of a constant
    if ( Hop_ObjIsConst1( Hop_Regular(pRoot) ) )
        return Cudd_NotCond( Cudd_ReadOne(dd), Hop_IsComplement(pRoot) );
    // construct BDD
    Abc_ConvertAigToBdd_rec1( dd, Hop_Regular(pRoot) );
    // hold on to the result
    bFunc = Cudd_NotCond( Hop_Regular(pRoot)->pData, Hop_IsComplement(pRoot) );  Cudd_Ref( bFunc );
    // dereference BDD
    Abc_ConvertAigToBdd_rec2( dd, Hop_Regular(pRoot) );
    // return the result
    Cudd_Deref( bFunc );
    return bFunc;
}



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

  Synopsis    [Construct BDDs and mark AIG nodes.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
int Abc_ConvertAigToTruth_rec1( Hop_Obj_t * pObj )
{
    int Counter = 0;
    assert( !Hop_IsComplement(pObj) );
    if ( !Hop_ObjIsNode(pObj) || Hop_ObjIsMarkA(pObj) )
        return 0;
    Counter += Abc_ConvertAigToTruth_rec1( Hop_ObjFanin0(pObj) ); 
    Counter += Abc_ConvertAigToTruth_rec1( Hop_ObjFanin1(pObj) );
    assert( !Hop_ObjIsMarkA(pObj) ); // loop detection
    Hop_ObjSetMarkA( pObj );
    return Counter + 1;
}

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

  Synopsis    [Computes truth table of the cut.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
unsigned * Abc_ConvertAigToTruth_rec2( Hop_Obj_t * pObj, Vec_Int_t * vTruth, int nWords )
{
    unsigned * pTruth, * pTruth0, * pTruth1;
    int i;
    assert( !Hop_IsComplement(pObj) );
    if ( !Hop_ObjIsNode(pObj) || !Hop_ObjIsMarkA(pObj) )
        return pObj->pData;
    // compute the truth tables of the fanins
    pTruth0 = Abc_ConvertAigToTruth_rec2( Hop_ObjFanin0(pObj), vTruth, nWords );
    pTruth1 = Abc_ConvertAigToTruth_rec2( Hop_ObjFanin1(pObj), vTruth, nWords );
    // creat the truth table of the node
    pTruth  = Vec_IntFetch( vTruth, nWords );
    if ( Hop_ObjIsExor(pObj) )
        for ( i = 0; i < nWords; i++ )
            pTruth[i] = pTruth0[i] ^ pTruth1[i];
    else if ( !Hop_ObjFaninC0(pObj) && !Hop_ObjFaninC1(pObj) )
        for ( i = 0; i < nWords; i++ )
            pTruth[i] = pTruth0[i] & pTruth1[i];
    else if ( !Hop_ObjFaninC0(pObj) && Hop_ObjFaninC1(pObj) )
        for ( i = 0; i < nWords; i++ )
            pTruth[i] = pTruth0[i] & ~pTruth1[i];
    else if ( Hop_ObjFaninC0(pObj) && !Hop_ObjFaninC1(pObj) )
        for ( i = 0; i < nWords; i++ )
            pTruth[i] = ~pTruth0[i] & pTruth1[i];
    else // if ( Hop_ObjFaninC0(pObj) && Hop_ObjFaninC1(pObj) )
        for ( i = 0; i < nWords; i++ )
            pTruth[i] = ~pTruth0[i] & ~pTruth1[i];
    assert( Hop_ObjIsMarkA(pObj) ); // loop detection
    Hop_ObjClearMarkA( pObj );
    pObj->pData = pTruth;
    return pTruth;
}

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

  Synopsis    [Computes truth table of the node.]

  Description [Assumes that the structural support is no more than 8 inputs.
  Uses array vTruth to store temporary truth tables. The returned pointer should 
  be used immediately.]
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
unsigned * Abc_ConvertAigToTruth( Hop_Man_t * p, Hop_Obj_t * pRoot, int nVars, Vec_Int_t * vTruth, int fMsbFirst )
{
    static unsigned uTruths[8][8] = { // elementary truth tables
        { 0xAAAAAAAA,0xAAAAAAAA,0xAAAAAAAA,0xAAAAAAAA,0xAAAAAAAA,0xAAAAAAAA,0xAAAAAAAA,0xAAAAAAAA },
        { 0xCCCCCCCC,0xCCCCCCCC,0xCCCCCCCC,0xCCCCCCCC,0xCCCCCCCC,0xCCCCCCCC,0xCCCCCCCC,0xCCCCCCCC },
        { 0xF0F0F0F0,0xF0F0F0F0,0xF0F0F0F0,0xF0F0F0F0,0xF0F0F0F0,0xF0F0F0F0,0xF0F0F0F0,0xF0F0F0F0 },
        { 0xFF00FF00,0xFF00FF00,0xFF00FF00,0xFF00FF00,0xFF00FF00,0xFF00FF00,0xFF00FF00,0xFF00FF00 },
        { 0xFFFF0000,0xFFFF0000,0xFFFF0000,0xFFFF0000,0xFFFF0000,0xFFFF0000,0xFFFF0000,0xFFFF0000 }, 
        { 0x00000000,0xFFFFFFFF,0x00000000,0xFFFFFFFF,0x00000000,0xFFFFFFFF,0x00000000,0xFFFFFFFF }, 
        { 0x00000000,0x00000000,0xFFFFFFFF,0xFFFFFFFF,0x00000000,0x00000000,0xFFFFFFFF,0xFFFFFFFF }, 
        { 0x00000000,0x00000000,0x00000000,0x00000000,0xFFFFFFFF,0xFFFFFFFF,0xFFFFFFFF,0xFFFFFFFF } 
    };
    Hop_Obj_t * pObj;
    unsigned * pTruth, * pTruth2;
    int i, nWords, nNodes;
    Vec_Ptr_t * vTtElems;

    // if the number of variables is more than 8, allocate truth tables
    if ( nVars > 8 )
        vTtElems = Vec_PtrAllocTruthTables( nVars );
    else
        vTtElems = NULL;

    // clear the data fields and set marks
    nNodes = Abc_ConvertAigToTruth_rec1( pRoot );
    // prepare memory
    nWords = Hop_TruthWordNum( nVars );
    Vec_IntClear( vTruth );
    Vec_IntGrow( vTruth, nWords * (nNodes+1) );
    pTruth = Vec_IntFetch( vTruth, nWords );
    // check the case of a constant
    if ( Hop_ObjIsConst1( Hop_Regular(pRoot) ) )
    {
        assert( nNodes == 0 );
        if ( Hop_IsComplement(pRoot) )
            Extra_TruthClear( pTruth, nVars );
        else
            Extra_TruthFill( pTruth, nVars );
        return pTruth;
    }
    // set elementary truth tables at the leaves
    assert( nVars <= Hop_ManPiNum(p) );
//    assert( Hop_ManPiNum(p) <= 8 ); 
    if ( fMsbFirst )
    {
        Hop_ManForEachPi( p, pObj, i )
        {
            if ( vTtElems )
                pObj->pData = Vec_PtrEntry(vTtElems, nVars-1-i);
            else               
                pObj->pData = (void *)uTruths[nVars-1-i];
        }
    }
    else
    {
        Hop_ManForEachPi( p, pObj, i )
        {
            if ( vTtElems )
                pObj->pData = Vec_PtrEntry(vTtElems, i);
            else               
                pObj->pData = (void *)uTruths[i];
        }
    }
    // clear the marks and compute the truth table
    pTruth2 = Abc_ConvertAigToTruth_rec2( pRoot, vTruth, nWords );
    // copy the result
    Extra_TruthCopy( pTruth, pTruth2, nVars );
    if ( vTtElems )
        Vec_PtrFree( vTtElems );
    return pTruth;
}


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

  Synopsis    [Construct BDDs and mark AIG nodes.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
void Abc_ConvertAigToAig_rec( Abc_Ntk_t * pNtkAig, Hop_Obj_t * pObj )
{
    assert( !Hop_IsComplement(pObj) );
    if ( !Hop_ObjIsNode(pObj) || Hop_ObjIsMarkA(pObj) )
        return;
    Abc_ConvertAigToAig_rec( pNtkAig, Hop_ObjFanin0(pObj) ); 
    Abc_ConvertAigToAig_rec( pNtkAig, Hop_ObjFanin1(pObj) );
    pObj->pData = Abc_AigAnd( pNtkAig->pManFunc, (Abc_Obj_t *)Hop_ObjChild0Copy(pObj), (Abc_Obj_t *)Hop_ObjChild1Copy(pObj) ); 
    assert( !Hop_ObjIsMarkA(pObj) ); // loop detection
    Hop_ObjSetMarkA( pObj );
}

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

  Synopsis    [Converts the network from AIG to BDD representation.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
Abc_Obj_t * Abc_ConvertAigToAig( Abc_Ntk_t * pNtkAig, Abc_Obj_t * pObjOld )
{
    Hop_Man_t * pHopMan;
    Hop_Obj_t * pRoot;
    Abc_Obj_t * pFanin;
    int i;
    // get the local AIG
    pHopMan = pObjOld->pNtk->pManFunc;
    pRoot = pObjOld->pData;
    // check the case of a constant
    if ( Hop_ObjIsConst1( Hop_Regular(pRoot) ) )
        return Abc_ObjNotCond( Abc_AigConst1(pNtkAig), Hop_IsComplement(pRoot) );
    // assign the fanin nodes
    Abc_ObjForEachFanin( pObjOld, pFanin, i )
    {
        assert( pFanin->pCopy != NULL );
        Hop_ManPi(pHopMan, i)->pData = pFanin->pCopy;
    }
    // construct the AIG
    Abc_ConvertAigToAig_rec( pNtkAig, Hop_Regular(pRoot) );
    Hop_ConeUnmark_rec( Hop_Regular(pRoot) );
    // return the result
    return Abc_ObjNotCond( Hop_Regular(pRoot)->pData, Hop_IsComplement(pRoot) );  
}


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

  Synopsis    [Unmaps the network.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
int Abc_NtkMapToSop( Abc_Ntk_t * pNtk )
{
    extern void * Abc_FrameReadLibGen();                    
    Abc_Obj_t * pNode;
    char * pSop;
    int i;

    assert( Abc_NtkHasMapping(pNtk) );
    // update the functionality manager
    assert( pNtk->pManFunc == Abc_FrameReadLibGen() );
    pNtk->pManFunc = Extra_MmFlexStart();
    pNtk->ntkFunc  = ABC_FUNC_SOP;
    // update the nodes
    Abc_NtkForEachNode( pNtk, pNode, i )
    {
        pSop = Mio_GateReadSop(pNode->pData);
        assert( Abc_SopGetVarNum(pSop) == Abc_ObjFaninNum(pNode) );
        pNode->pData = Abc_SopRegister( pNtk->pManFunc, pSop );
    }
    return 1;
}

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

  Synopsis    [Converts SOP functions into BLIF-MV functions.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
int Abc_NtkSopToBlifMv( Abc_Ntk_t * pNtk )
{
    return 1;
}

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

  Synopsis    [Convers logic network to the SOP form.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
int Abc_NtkToSop( Abc_Ntk_t * pNtk, int fDirect )
{
    assert( !Abc_NtkIsStrash(pNtk) );
    if ( Abc_NtkHasSop(pNtk) )
    {
        if ( !fDirect )
            return 1;
        if ( !Abc_NtkSopToBdd(pNtk) )
            return 0;
        return Abc_NtkBddToSop(pNtk, fDirect);
    }
    if ( Abc_NtkHasMapping(pNtk) )
        return Abc_NtkMapToSop(pNtk);
    if ( Abc_NtkHasBdd(pNtk) )
        return Abc_NtkBddToSop(pNtk, fDirect);
    if ( Abc_NtkHasAig(pNtk) )
    {
        if ( !Abc_NtkAigToBdd(pNtk) )
            return 0;
        return Abc_NtkBddToSop(pNtk, fDirect);
    }
    assert( 0 );
    return 0;
}

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

  Synopsis    [Convers logic network to the SOP form.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
int Abc_NtkToBdd( Abc_Ntk_t * pNtk )
{
    assert( !Abc_NtkIsStrash(pNtk) );
    if ( Abc_NtkHasBdd(pNtk) )
        return 1;
    if ( Abc_NtkHasMapping(pNtk) )
    {
        Abc_NtkMapToSop(pNtk);
        return Abc_NtkSopToBdd(pNtk);
    }
    if ( Abc_NtkHasSop(pNtk) )
        return Abc_NtkSopToBdd(pNtk);
    if ( Abc_NtkHasAig(pNtk) )
        return Abc_NtkAigToBdd(pNtk);
    assert( 0 );
    return 0;
}

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

  Synopsis    [Convers logic network to the SOP form.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
int Abc_NtkToAig( Abc_Ntk_t * pNtk )
{
    assert( !Abc_NtkIsStrash(pNtk) );
    if ( Abc_NtkHasAig(pNtk) )
        return 1;
    if ( Abc_NtkHasMapping(pNtk) )
    {
        Abc_NtkMapToSop(pNtk);
        return Abc_NtkSopToAig(pNtk);
    }
    if ( Abc_NtkHasBdd(pNtk) )
    {
        if ( !Abc_NtkBddToSop(pNtk,0) )
            return 0;
        return Abc_NtkSopToAig(pNtk);
    }
    if ( Abc_NtkHasSop(pNtk) )
        return Abc_NtkSopToAig(pNtk);
    assert( 0 );
    return 0;
}


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


