Version abc71001

1 files changed, 0 insertions, 591 deletions

diff --git a/abc70930/src/aig/dar/darRefact.c b/abc70930/src/aig/dar/darRefact.c
deleted file mode 100644
index a765ec30..00000000
--- a/abc70930/src/aig/dar/darRefact.c
+++ /dev/null
@@ -1,591 +0,0 @@
-/**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 "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.Node );
-        pNode1 = Kit_GraphNode( pGraph, pNode->eEdge1.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.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 + 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.Node)->pFunc, pNode->eEdge0.fCompl ); 
-        pAnd1 = Aig_NotCond( 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( 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 = 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;
-}
-
-/**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     []
- 
-***********************************************************************/
-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;
-
-}
-
-////////////////////////////////////////////////////////////////////////
-///                       END OF FILE                                ///
-////////////////////////////////////////////////////////////////////////
-
-