/**CFile****************************************************************
Copyright (c) The Regents of the University of California. All rights reserved.

Permission is hereby granted, without written agreement and without license or
royalty fees, to use, copy, modify, and distribute this software and its
documentation for any purpose, provided that the above copyright notice and
the following two paragraphs appear in all copies of this software.

IN NO EVENT SHALL THE UNIVERSITY OF CALIFORNIA BE LIABLE TO ANY PARTY FOR
DIRECT, INDIRECT, SPECIAL, INCIDENTAL, OR CONSEQUENTIAL DAMAGES ARISING OUT OF
THE USE OF THIS SOFTWARE AND ITS DOCUMENTATION, EVEN IF THE UNIVERSITY OF
CALIFORNIA HAS BEEN ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.

THE UNIVERSITY OF CALIFORNIA SPECIFICALLY DISCLAIMS ANY WARRANTIES, INCLUDING,
BUT NOT LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR
A PARTICULAR PURPOSE. THE SOFTWARE PROVIDED HEREUNDER IS ON AN "AS IS" BASIS,
AND THE UNIVERSITY OF CALIFORNIA HAS NO OBLIGATION TO PROVIDE MAINTENANCE,
SUPPORT, UPDATES, ENHANCEMENTS, OR MODIFICATIONS.


  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 "kit.h"

////////////////////////////////////////////////////////////////////////
///                        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
    // 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
    int              timeCuts;
    int              timeEval;
    int              timeOther;
    int              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 = 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( 256, Kit_TruthWordNum(pPars->nLeafMax) );
    p->vMemory      = Vec_IntAlloc( 1 << 16 );
    p->vCutNodes    = Vec_PtrAlloc( 256 );
    p->vLeavesBest  = Vec_PtrAlloc( pPars->nLeafMax );
    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) );
    PRT( "Cuts  ", p->timeCuts );
    PRT( "Eval  ", p->timeEval );
    PRT( "Other ", p->timeOther );
    PRT( "TOTAL ", p->timeTotal );
}

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

  Synopsis    [Stops the rewriting manager.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
void Dar_ManRefStop( Ref_Man_t * p )
{
    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 );
    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(pNode->pFunc)->Level;
        assert( Aig_Regular(pNode->pFunc)->Level < (1<<14)-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.bits.Node );
        pNode1 = Kit_GraphNode( pGraph, pNode->eEdge1.bits.Node );
        // get the AIG nodes corresponding to the children 
        pAnd0 = pNode0->pFunc; 
        pAnd1 = pNode1->pFunc; 
        if ( pAnd0 && pAnd1 )
        {
            // if they are both present, find the resulting node
            pAnd0 = Aig_NotCond( pAnd0, pNode->eEdge0.bits.fCompl );
            pAnd1 = Aig_NotCond( pAnd1, pNode->eEdge1.bits.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 + AIG_MAX( 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( 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( Kit_GraphNode(pGraph, pNode->eEdge0.bits.Node)->pFunc, pNode->eEdge0.bits.fCompl ); 
        pAnd1 = Aig_NotCond( Kit_GraphNode(pGraph, pNode->eEdge1.bits.Node)->pFunc, pNode->eEdge1.bits.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( pNode->pFunc, Kit_GraphIsComplement(pGraph) );
}

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

  Synopsis    []

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
#if 0
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 = Vec_PtrSize(p->vCutNodes);
            p->pGraphBest = Kit_GraphCreateConst0();
            Vec_PtrCopy( p->vLeavesBest, vCut );
            return p->GainBest;
        }
        if ( Kit_TruthIsConst1(pTruth, Vec_PtrSize(vCut)) )
        {
            p->GainBest = Vec_PtrSize(p->vCutNodes);
            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 );
            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 );
        if ( RetValue > -1 )
        {
            pGraphCur = Kit_SopFactor( p->vMemory, 1, Vec_PtrSize(vCut), p->vMemory );
            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;
}
#endif

/**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( vCut, pObj, i )
        if ( !Aig_ObjIsPi(pObj) && (int)pObj->Level <= nLevelMin )
            return 1;
    return 0;
}

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

  Synopsis    []

  Description []
               
  SideEffects []

  SeeAlso     []
 
***********************************************************************/
#if 0
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, 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 = 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;
        Vec_VecClear( p->vCuts );

//printf( "\nConsidering node %d.\n", pObj->Id );
        // get the bounded MFFC size
clk = clock();
        nLevelMin = AIG_MAX( 0, Aig_ObjLevel(pObj) - 10 );
        nNodesSaved = Aig_NodeMffsSupp( pAig, pObj, nLevelMin, vCut );
        if ( nNodesSaved < p->pPars->nMffcMin ) // too small to consider
        {
p->timeCuts += 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_NodeMffsLabelCut( p->pAig, pObj, vCut );
        }
        else if ( Vec_PtrSize(vCut) < p->pPars->nLeafMax - 2 && p->pPars->fExtend )
        {
            if ( !Dar_ObjCutLevelAchieved(vCut, nLevelMin) )
            {
                if ( Aig_NodeMffsExtendCut( pAig, pObj, vCut, vCut2 ) )
                {
                    nNodesSaved2 = Aig_NodeMffsLabelCut( 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 += clock() - clk;

        // try the cuts
clk = clock();
        Required = pAig->vLevelR? Aig_ObjRequiredLevel(pAig, pObj) : AIG_INFINITY;
        Dar_ManRefactorTryCuts( p, pObj, nNodesSaved, Required );
p->timeEval += 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, 1, p->pPars->fUpdateLevel );
        // compare the gains
        nNodeAfter = Aig_ManNodeNum( pAig );
        assert( p->GainBest <= nNodeBefore - nNodeAfter );
        Kit_GraphFree( p->pGraphBest );
        p->nCutsUsed++;
//        break;
    }
p->timeTotal = 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 );

    // 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;

}
#endif

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