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

  FileName    [darRefact.c]

  SystemName  [ABC: Logic synthesis and verification system.]

  PackageName [DAG-aware AIG rewriting.]

  Synopsis    [Refactoring.]

  Author      [Alan Mishchenko]
  
  Affiliation [UC Berkeley]

  Date        [Ver. 1.0. Started - April 28, 2007.]

  Revision    [$Id: darRefact.c,v 1.00 2007/04/28 00:00:00 alanmi Exp $]

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

#include "darInt.h"
#include "bool/kit/kit.h"

#include "bool/bdc/bdc.h"
#include "bool/bdc/bdcInt.h"

ABC_NAMESPACE_IMPL_START


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

// the refactoring manager
typedef struct Ref_Man_t_            Ref_Man_t;
struct Ref_Man_t_
{
    // input data
    Dar_RefPar_t *   pPars;          // rewriting parameters
    Aig_Man_t *      pAig;           // AIG manager 
    // computed cuts
    Vec_Vec_t *      vCuts;          // the storage for cuts
    // truth table and ISOP
    Vec_Ptr_t *      vTruthElem;     // elementary truth tables
    Vec_Ptr_t *      vTruthStore;    // storage for truth tables
    Vec_Int_t *      vMemory;        // storage for ISOP
    Vec_Ptr_t *      vCutNodes;      // storage for internal nodes of the cut
    // various data members
    Vec_Ptr_t *      vLeavesBest;    // the best set of leaves
    Kit_Graph_t *    pGraphBest;     // the best factored form
    int              GainBest;       // the best gain
    int              LevelBest;      // the level of node with the best gain
    // bi-decomposition
    Bdc_Par_t        DecPars;        // decomposition parameters
    Bdc_Man_t *      pManDec;        // decomposition manager
    // node statistics
    int              nNodesInit;     // the initial number of nodes
    int              nNodesTried;    // the number of nodes tried
    int              nNodesBelow;    // the number of nodes below the level limit
    int              nNodesExten;    // the number of nodes with extended cut
    int              nCutsUsed;      // the number of rewriting steps
    int              nCutsTried;     // the number of cuts tries
    // timing statistics
    abctime          timeCuts;
    abctime          timeEval;
    abctime          timeOther;
    abctime          timeTotal;
};

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

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

  Synopsis    [Returns the structure with default assignment of parameters.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
void Dar_ManDefaultRefParams( Dar_RefPar_t * pPars )
{
    memset( pPars, 0, sizeof(Dar_RefPar_t) );
    pPars->nMffcMin     =  2;  // the min MFFC size for which refactoring is used
    pPars->nLeafMax     = 12;  // the max number of leaves of a cut
    pPars->nCutsMax     =  5;  // the max number of cuts to consider  
    pPars->fUpdateLevel =  0;
    pPars->fUseZeros    =  0;
    pPars->fVerbose     =  0;
    pPars->fVeryVerbose =  0;
}

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

  Synopsis    [Starts the rewriting manager.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
Ref_Man_t * Dar_ManRefStart( Aig_Man_t * pAig, Dar_RefPar_t * pPars )
{
    Ref_Man_t * p;
    // start the manager
    p = ABC_ALLOC( Ref_Man_t, 1 );
    memset( p, 0, sizeof(Ref_Man_t) );
    p->pAig         = pAig;
    p->pPars        = pPars;
    // other data
    p->vCuts        = Vec_VecStart( pPars->nCutsMax );
    p->vTruthElem   = Vec_PtrAllocTruthTables( pPars->nLeafMax );
    p->vTruthStore  = Vec_PtrAllocSimInfo( 1024, Kit_TruthWordNum(pPars->nLeafMax) );
    p->vMemory      = Vec_IntAlloc( 1 << 16 );
    p->vCutNodes    = Vec_PtrAlloc( 256 );
    p->vLeavesBest  = Vec_PtrAlloc( pPars->nLeafMax );
    // alloc bi-decomposition manager
    p->DecPars.nVarsMax = pPars->nLeafMax;
    p->DecPars.fVerbose = pPars->fVerbose;
    p->DecPars.fVeryVerbose = 0;
//    p->pManDec = Bdc_ManAlloc( &p->DecPars );
    return p;
}

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

  Synopsis    [Prints out the statistics of the manager.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
void Dar_ManRefPrintStats( Ref_Man_t * p )
{
    int Gain = p->nNodesInit - Aig_ManNodeNum(p->pAig);
    printf( "NodesBeg = %8d. NodesEnd = %8d. Gain = %6d. (%6.2f %%).\n", 
        p->nNodesInit, Aig_ManNodeNum(p->pAig), Gain, 100.0*Gain/p->nNodesInit );
    printf( "Tried = %6d. Below = %5d. Extended = %5d.  Used = %5d.  Levels = %4d.\n", 
        p->nNodesTried, p->nNodesBelow, p->nNodesExten, p->nCutsUsed, Aig_ManLevels(p->pAig) );
    ABC_PRT( "Cuts  ", p->timeCuts );
    ABC_PRT( "Eval  ", p->timeEval );
    ABC_PRT( "Other ", p->timeOther );
    ABC_PRT( "TOTAL ", p->timeTotal );
}

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

  Synopsis    [Stops the rewriting manager.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
void Dar_ManRefStop( Ref_Man_t * p )
{
    if ( p->pManDec )
        Bdc_ManFree( p->pManDec );
    if ( p->pPars->fVerbose )
        Dar_ManRefPrintStats( p );
    Vec_VecFree( p->vCuts );
    Vec_PtrFree( p->vTruthElem );
    Vec_PtrFree( p->vTruthStore );
    Vec_PtrFree( p->vLeavesBest );
    Vec_IntFree( p->vMemory );
    Vec_PtrFree( p->vCutNodes );
    ABC_FREE( p );
}

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

  Synopsis    []

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
void Ref_ObjComputeCuts( Aig_Man_t * pAig, Aig_Obj_t * pRoot, Vec_Vec_t * vCuts )
{
}

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

  Synopsis    []

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
void Ref_ObjPrint( Aig_Obj_t * pObj )
{
    printf( "%d", pObj? Aig_Regular(pObj)->Id : -1 );
    if ( pObj )
        printf( "(%d) ", Aig_IsComplement(pObj) );
}

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

  Synopsis    [Counts the number of new nodes added when using this graph.]

  Description [AIG nodes for the fanins should be assigned to pNode->pFunc 
  of the leaves of the graph before calling this procedure. 
  Returns -1 if the number of nodes and levels exceeded the given limit or 
  the number of levels exceeded the maximum allowed level.]
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
int Dar_RefactTryGraph( Aig_Man_t * pAig, Aig_Obj_t * pRoot, Vec_Ptr_t * vCut, Kit_Graph_t * pGraph, int NodeMax, int LevelMax )
{
    Kit_Node_t * pNode, * pNode0, * pNode1;
    Aig_Obj_t * pAnd, * pAnd0, * pAnd1;
    int i, Counter, LevelNew, LevelOld;
    // check for constant function or a literal
    if ( Kit_GraphIsConst(pGraph) || Kit_GraphIsVar(pGraph) )
        return 0;
    // set the levels of the leaves
    Kit_GraphForEachLeaf( pGraph, pNode, i )
    {
        pNode->pFunc = Vec_PtrEntry(vCut, i);
        pNode->Level = Aig_Regular((Aig_Obj_t *)pNode->pFunc)->Level;
        assert( Aig_Regular((Aig_Obj_t *)pNode->pFunc)->Level < (1<<24)-1 );
    }
//printf( "Trying:\n" );
    // compute the AIG size after adding the internal nodes
    Counter = 0;
    Kit_GraphForEachNode( pGraph, pNode, i )
    {
        // get the children of this node
        pNode0 = Kit_GraphNode( pGraph, pNode->eEdge0.Node );
        pNode1 = Kit_GraphNode( pGraph, pNode->eEdge1.Node );
        // get the AIG nodes corresponding to the children 
        pAnd0 = (Aig_Obj_t *)pNode0->pFunc; 
        pAnd1 = (Aig_Obj_t *)pNode1->pFunc; 
        if ( pAnd0 && pAnd1 )
        {
            // if they are both present, find the resulting node
            pAnd0 = Aig_NotCond( pAnd0, pNode->eEdge0.fCompl );
            pAnd1 = Aig_NotCond( pAnd1, pNode->eEdge1.fCompl );
            pAnd  = Aig_TableLookupTwo( pAig, pAnd0, pAnd1 );
            // return -1 if the node is the same as the original root
            if ( Aig_Regular(pAnd) == pRoot )
                return -1;
        }
        else
            pAnd = NULL;
        // count the number of added nodes
        if ( pAnd == NULL || Aig_ObjIsTravIdCurrent(pAig, Aig_Regular(pAnd)) )
        {
            if ( ++Counter > NodeMax )
                return -1;
        }
        // count the number of new levels
        LevelNew = 1 + Abc_MaxInt( pNode0->Level, pNode1->Level );
        if ( pAnd )
        {
            if ( Aig_Regular(pAnd) == Aig_ManConst1(pAig) )
                LevelNew = 0;
            else if ( Aig_Regular(pAnd) == Aig_Regular(pAnd0) )
                LevelNew = (int)Aig_Regular(pAnd0)->Level;
            else if ( Aig_Regular(pAnd) == Aig_Regular(pAnd1) )
                LevelNew = (int)Aig_Regular(pAnd1)->Level;
            LevelOld = (int)Aig_Regular(pAnd)->Level;
//            assert( LevelNew == LevelOld );
        }
        if ( LevelNew > LevelMax )
            return -1;
        pNode->pFunc = pAnd;
        pNode->Level = LevelNew;
/*
printf( "Checking " );
Ref_ObjPrint( pAnd0 );
printf( " and " );
Ref_ObjPrint( pAnd1 );
printf( "  Result " );
Ref_ObjPrint( pNode->pFunc );
printf( "\n" );
*/
    }
    return Counter;
}

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

  Synopsis    []

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
Aig_Obj_t * Dar_RefactBuildGraph( Aig_Man_t * pAig, Vec_Ptr_t * vCut, Kit_Graph_t * pGraph )
{
    Aig_Obj_t * pAnd0, * pAnd1;
    Kit_Node_t * pNode = NULL;
    int i;
    // check for constant function
    if ( Kit_GraphIsConst(pGraph) )
        return Aig_NotCond( Aig_ManConst1(pAig), Kit_GraphIsComplement(pGraph) );
    // set the leaves
    Kit_GraphForEachLeaf( pGraph, pNode, i )
        pNode->pFunc = Vec_PtrEntry(vCut, i);
    // check for a literal
    if ( Kit_GraphIsVar(pGraph) )
        return Aig_NotCond( (Aig_Obj_t *)Kit_GraphVar(pGraph)->pFunc, Kit_GraphIsComplement(pGraph) );
    // build the AIG nodes corresponding to the AND gates of the graph
//printf( "Building (current number %d):\n", Aig_ManObjNumMax(pAig) );
    Kit_GraphForEachNode( pGraph, pNode, i )
    {
        pAnd0 = Aig_NotCond( (Aig_Obj_t *)Kit_GraphNode(pGraph, pNode->eEdge0.Node)->pFunc, pNode->eEdge0.fCompl ); 
        pAnd1 = Aig_NotCond( (Aig_Obj_t *)Kit_GraphNode(pGraph, pNode->eEdge1.Node)->pFunc, pNode->eEdge1.fCompl ); 
        pNode->pFunc = Aig_And( pAig, pAnd0, pAnd1 );
/*
printf( "Checking " );
Ref_ObjPrint( pAnd0 );
printf( " and " );
Ref_ObjPrint( pAnd1 );
printf( "  Result " );
Ref_ObjPrint( pNode->pFunc );
printf( "\n" );
*/
    }
    // complement the result if necessary
    return Aig_NotCond( (Aig_Obj_t *)pNode->pFunc, Kit_GraphIsComplement(pGraph) );
}

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

  Synopsis    []

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
int Dar_ManRefactorTryCuts( Ref_Man_t * p, Aig_Obj_t * pObj, int nNodesSaved, int Required )
{
    Vec_Ptr_t * vCut;
    Kit_Graph_t * pGraphCur;
    int k, RetValue, GainCur, nNodesAdded;
    unsigned * pTruth;

    p->GainBest = -1;
    p->pGraphBest = NULL;
    Vec_VecForEachLevel( p->vCuts, vCut, k )
    {
        if ( Vec_PtrSize(vCut) == 0 )
            continue;
//        if ( Vec_PtrSize(vCut) != 0 && Vec_PtrSize(Vec_VecEntry(p->vCuts, k+1)) != 0 )
//            continue;

        p->nCutsTried++;
        // get the cut nodes
        Aig_ObjCollectCut( pObj, vCut, p->vCutNodes );
        // get the truth table
        pTruth = Aig_ManCutTruth( pObj, vCut, p->vCutNodes, p->vTruthElem, p->vTruthStore );
        if ( Kit_TruthIsConst0(pTruth, Vec_PtrSize(vCut)) )
        {
            p->GainBest = Aig_NodeMffcSupp( p->pAig, pObj, 0, NULL );
            p->pGraphBest = Kit_GraphCreateConst0();
            Vec_PtrCopy( p->vLeavesBest, vCut );
            return p->GainBest;
        }
        if ( Kit_TruthIsConst1(pTruth, Vec_PtrSize(vCut)) )
        {
            p->GainBest = Aig_NodeMffcSupp( p->pAig, pObj, 0, NULL );
            p->pGraphBest = Kit_GraphCreateConst1();
            Vec_PtrCopy( p->vLeavesBest, vCut );
            return p->GainBest;
        }

        // try the positive phase
        RetValue = Kit_TruthIsop( pTruth, Vec_PtrSize(vCut), p->vMemory, 0 );
        if ( RetValue > -1 )
        {
            pGraphCur = Kit_SopFactor( p->vMemory, 0, Vec_PtrSize(vCut), p->vMemory );
/*
{
    int RetValue;
    RetValue = Bdc_ManDecompose( p->pManDec, pTruth, NULL, Vec_PtrSize(vCut), NULL, 1000 );
    printf( "Graph = %d. Bidec = %d.\n", Kit_GraphNodeNum(pGraphCur), RetValue );
}
*/
            nNodesAdded = Dar_RefactTryGraph( p->pAig, pObj, vCut, pGraphCur, nNodesSaved - !p->pPars->fUseZeros, Required );
            if ( nNodesAdded > -1 )
            {
                GainCur = nNodesSaved - nNodesAdded;
                if ( p->GainBest < GainCur || (p->GainBest == GainCur && 
                    (Kit_GraphIsConst(pGraphCur) || Kit_GraphRootLevel(pGraphCur) < Kit_GraphRootLevel(p->pGraphBest))) )
                {
                    p->GainBest = GainCur;
                    if ( p->pGraphBest )
                        Kit_GraphFree( p->pGraphBest );
                    p->pGraphBest = pGraphCur;
                    Vec_PtrCopy( p->vLeavesBest, vCut );
                }
                else
                    Kit_GraphFree( pGraphCur );
            }
            else
                Kit_GraphFree( pGraphCur );
        }
        // try negative phase
        Kit_TruthNot( pTruth, pTruth, Vec_PtrSize(vCut) );
        RetValue = Kit_TruthIsop( pTruth, Vec_PtrSize(vCut), p->vMemory, 0 );
//        Kit_TruthNot( pTruth, pTruth, Vec_PtrSize(vCut) );
        if ( RetValue > -1 )
        {
            pGraphCur = Kit_SopFactor( p->vMemory, 1, Vec_PtrSize(vCut), p->vMemory );
/*
{
    int RetValue;
    RetValue = Bdc_ManDecompose( p->pManDec, pTruth, NULL, Vec_PtrSize(vCut), NULL, 1000 );
    printf( "Graph = %d. Bidec = %d.\n", Kit_GraphNodeNum(pGraphCur), RetValue );
}
*/
            nNodesAdded = Dar_RefactTryGraph( p->pAig, pObj, vCut, pGraphCur, nNodesSaved - !p->pPars->fUseZeros, Required );
            if ( nNodesAdded > -1 )
            {
                GainCur = nNodesSaved - nNodesAdded;
                if ( p->GainBest < GainCur || (p->GainBest == GainCur && 
                    (Kit_GraphIsConst(pGraphCur) || Kit_GraphRootLevel(pGraphCur) < Kit_GraphRootLevel(p->pGraphBest))) )
                {
                    p->GainBest = GainCur;
                    if ( p->pGraphBest )
                        Kit_GraphFree( p->pGraphBest );
                    p->pGraphBest = pGraphCur;
                    Vec_PtrCopy( p->vLeavesBest, vCut );
                }
                else
                    Kit_GraphFree( pGraphCur );
            }
            else
                Kit_GraphFree( pGraphCur );
        }
    }

    return p->GainBest;
}

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

  Synopsis    [Returns 1 if a non-PI node has nLevelMin or below.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
int Dar_ObjCutLevelAchieved( Vec_Ptr_t * vCut, int nLevelMin )
{
    Aig_Obj_t * pObj;
    int i;
    Vec_PtrForEachEntry( Aig_Obj_t *, vCut, pObj, i )
        if ( !Aig_ObjIsCi(pObj) && (int)pObj->Level <= nLevelMin )
            return 1;
    return 0;
}

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

  Synopsis    []

  Description []
               
  SideEffects []

  SeeAlso     []
 
***********************************************************************/
int Dar_ManRefactor( Aig_Man_t * pAig, Dar_RefPar_t * pPars )
{
//    Bar_Progress_t * pProgress;
    Ref_Man_t * p;
    Vec_Ptr_t * vCut, * vCut2;
    Aig_Obj_t * pObj, * pObjNew;
    int nNodesOld, nNodeBefore, nNodeAfter, nNodesSaved, nNodesSaved2;
    int i, Required, nLevelMin;
    abctime clkStart, clk;

    // start the manager
    p = Dar_ManRefStart( pAig, pPars );
    // remove dangling nodes
    Aig_ManCleanup( pAig );
    // if updating levels is requested, start fanout and timing
    Aig_ManFanoutStart( pAig );
    if ( p->pPars->fUpdateLevel )
        Aig_ManStartReverseLevels( pAig, 0 );

    // resynthesize each node once
    clkStart = Abc_Clock();
    vCut = Vec_VecEntry( p->vCuts, 0 );
    vCut2 = Vec_VecEntry( p->vCuts, 1 );
    p->nNodesInit = Aig_ManNodeNum(pAig);
    nNodesOld = Vec_PtrSize( pAig->vObjs );
//    pProgress = Bar_ProgressStart( stdout, nNodesOld );
    Aig_ManForEachObj( pAig, pObj, i )
    {
//        Bar_ProgressUpdate( pProgress, i, NULL );
        if ( !Aig_ObjIsNode(pObj) )
            continue;
        if ( i > nNodesOld )
            break;
        if ( pAig->Time2Quit && !(i & 256) && Abc_Clock() > pAig->Time2Quit )
            break;
        Vec_VecClear( p->vCuts );

//printf( "\nConsidering node %d.\n", pObj->Id );
        // get the bounded MFFC size
clk = Abc_Clock();
        nLevelMin = Abc_MaxInt( 0, Aig_ObjLevel(pObj) - 10 );
        nNodesSaved = Aig_NodeMffcSupp( pAig, pObj, nLevelMin, vCut );
        if ( nNodesSaved < p->pPars->nMffcMin ) // too small to consider
        {
p->timeCuts += Abc_Clock() - clk;
            continue; 
        }
        p->nNodesTried++;
        if ( Vec_PtrSize(vCut) > p->pPars->nLeafMax ) // get one reconv-driven cut
        {
            Aig_ManFindCut( pObj, vCut, p->vCutNodes, p->pPars->nLeafMax, 50 );
            nNodesSaved = Aig_NodeMffcLabelCut( p->pAig, pObj, vCut );
        }
        else if ( Vec_PtrSize(vCut) < p->pPars->nLeafMax - 2 && p->pPars->fExtend )
        {
            if ( !Dar_ObjCutLevelAchieved(vCut, nLevelMin) )
            {
                if ( Aig_NodeMffcExtendCut( pAig, pObj, vCut, vCut2 ) )
                {
                    nNodesSaved2 = Aig_NodeMffcLabelCut( p->pAig, pObj, vCut );
                    assert( nNodesSaved2 == nNodesSaved );
                }
                if ( Vec_PtrSize(vCut2) > p->pPars->nLeafMax )
                    Vec_PtrClear(vCut2);
                if ( Vec_PtrSize(vCut2) > 0 )
                {
                    p->nNodesExten++;
//                    printf( "%d(%d) ", Vec_PtrSize(vCut), Vec_PtrSize(vCut2) );
                }
            }
            else
                p->nNodesBelow++;
        }
p->timeCuts += Abc_Clock() - clk;

        // try the cuts
clk = Abc_Clock();
        Required = pAig->vLevelR? Aig_ObjRequiredLevel(pAig, pObj) : ABC_INFINITY;
        Dar_ManRefactorTryCuts( p, pObj, nNodesSaved, Required );
p->timeEval += Abc_Clock() - clk;

        // check the best gain
        if ( !(p->GainBest > 0 || (p->GainBest == 0 && p->pPars->fUseZeros)) )
        {
            if ( p->pGraphBest )
                Kit_GraphFree( p->pGraphBest );
            continue;
        }
//printf( "\n" );

        // if we end up here, a rewriting step is accepted
        nNodeBefore = Aig_ManNodeNum( pAig );
        pObjNew = Dar_RefactBuildGraph( pAig, p->vLeavesBest, p->pGraphBest );
        assert( (int)Aig_Regular(pObjNew)->Level <= Required );
        // replace the node
        Aig_ObjReplace( pAig, pObj, pObjNew, p->pPars->fUpdateLevel );
        // compare the gains
        nNodeAfter = Aig_ManNodeNum( pAig );
        assert( p->GainBest <= nNodeBefore - nNodeAfter );
        Kit_GraphFree( p->pGraphBest );
        p->nCutsUsed++;
//        break;
    }
p->timeTotal = Abc_Clock() - clkStart;
p->timeOther = p->timeTotal - p->timeCuts - p->timeEval;

//    Bar_ProgressStop( pProgress );
    // put the nodes into the DFS order and reassign their IDs
//    Aig_NtkReassignIds( p );
    // fix the levels
    Aig_ManFanoutStop( pAig );
    if ( p->pPars->fUpdateLevel )
        Aig_ManStopReverseLevels( pAig );
/*
    Aig_ManForEachObj( p->pAig, pObj, i )
        if ( Aig_ObjIsNode(pObj) && Aig_ObjRefs(pObj) == 0 )
        {
            printf( "Unreferenced " );
            Aig_ObjPrintVerbose( pObj, 0 );
            printf( "\n" );
        }
*/
    // remove dangling nodes (they should not be here!)
    Aig_ManCleanup( pAig );

    // stop the rewriting manager
    Dar_ManRefStop( p );
//    Aig_ManCheckPhase( pAig );
    if ( !Aig_ManCheck( pAig ) )
    {
        printf( "Dar_ManRefactor: The network check has failed.\n" );
        return 0;
    }
    return 1;

}

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


ABC_NAMESPACE_IMPL_END