From e54d9691616b9a0326e2fdb3156bb4eeb8abfcd7 Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Sun, 30 Sep 2007 08:01:00 -0700 Subject: Version abc70930 --- src/aig/dar/darLib.c | 980 --------------------------------------------------- 1 file changed, 980 deletions(-) delete mode 100644 src/aig/dar/darLib.c (limited to 'src/aig/dar/darLib.c') diff --git a/src/aig/dar/darLib.c b/src/aig/dar/darLib.c deleted file mode 100644 index 14a47cee..00000000 --- a/src/aig/dar/darLib.c +++ /dev/null @@ -1,980 +0,0 @@ -/**CFile**************************************************************** - - FileName [darLib.c] - - SystemName [ABC: Logic synthesis and verification system.] - - PackageName [DAG-aware AIG rewriting.] - - Synopsis [Library of AIG subgraphs used for rewriting.] - - Author [Alan Mishchenko] - - Affiliation [UC Berkeley] - - Date [Ver. 1.0. Started - April 28, 2007.] - - Revision [$Id: darLib.c,v 1.00 2007/04/28 00:00:00 alanmi Exp $] - -***********************************************************************/ - -#include "darInt.h" - -//////////////////////////////////////////////////////////////////////// -/// DECLARATIONS /// -//////////////////////////////////////////////////////////////////////// - -typedef struct Dar_Lib_t_ Dar_Lib_t; -typedef struct Dar_LibObj_t_ Dar_LibObj_t; -typedef struct Dar_LibDat_t_ Dar_LibDat_t; - -struct Dar_LibObj_t_ // library object (2 words) -{ - unsigned Fan0 : 16; // the first fanin - unsigned Fan1 : 16; // the second fanin - unsigned fCompl0 : 1; // the first compl attribute - unsigned fCompl1 : 1; // the second compl attribute - unsigned fPhase : 1; // the phase of the node - unsigned fTerm : 1; // indicates a PI - unsigned Num : 28; // internal use -}; - -struct Dar_LibDat_t_ // library object data -{ - Aig_Obj_t * pFunc; // the corresponding AIG node if it exists - int Level; // level of this node after it is constructured - int TravId; // traversal ID of the library object data - unsigned char fMffc; // set to one if node is part of MFFC - unsigned char nLats[3]; // the number of latches on the input/output stem -}; - -struct Dar_Lib_t_ // library -{ - // objects - Dar_LibObj_t * pObjs; // the set of library objects - int nObjs; // the number of objects used - int iObj; // the current object - // structures by class - int nSubgr[222]; // the number of subgraphs by class - int * pSubgr[222]; // the subgraphs for each class - int * pSubgrMem; // memory for subgraph pointers - int nSubgrTotal; // the total number of subgraph - // structure priorities - int * pPriosMem; // memory for priority of structures - int * pPrios[222]; // pointers to the priority numbers - // structure places in the priorities - int * pPlaceMem; // memory for places of structures in the priority lists - int * pPlace[222]; // pointers to the places numbers - // structure scores - int * pScoreMem; // memory for scores of structures - int * pScore[222]; // pointers to the scores numbers - // nodes by class - int nNodes[222]; // the number of nodes by class - int * pNodes[222]; // the nodes for each class - int * pNodesMem; // memory for nodes pointers - int nNodesTotal; // the total number of nodes - // prepared library - int nSubgraphs; - int nNodes0Max; - // nodes by class - int nNodes0[222]; // the number of nodes by class - int * pNodes0[222]; // the nodes for each class - int * pNodes0Mem; // memory for nodes pointers - int nNodes0Total; // the total number of nodes - // structures by class - int nSubgr0[222]; // the number of subgraphs by class - int * pSubgr0[222]; // the subgraphs for each class - int * pSubgr0Mem; // memory for subgraph pointers - int nSubgr0Total; // the total number of subgraph - // object data - Dar_LibDat_t * pDatas; - int nDatas; - // information about NPN classes - char ** pPerms4; - unsigned short * puCanons; - char * pPhases; - char * pPerms; - unsigned char * pMap; -}; - -static Dar_Lib_t * s_DarLib = NULL; - -static inline Dar_LibObj_t * Dar_LibObj( Dar_Lib_t * p, int Id ) { return p->pObjs + Id; } -static inline int Dar_LibObjTruth( Dar_LibObj_t * pObj ) { return pObj->Num < (0xFFFF & ~pObj->Num) ? pObj->Num : (0xFFFF & ~pObj->Num); } - -//////////////////////////////////////////////////////////////////////// -/// FUNCTION DEFINITIONS /// -//////////////////////////////////////////////////////////////////////// - -/**Function************************************************************* - - Synopsis [Starts the library.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -Dar_Lib_t * Dar_LibAlloc( int nObjs ) -{ - unsigned uTruths[4] = { 0xAAAA, 0xCCCC, 0xF0F0, 0xFF00 }; - Dar_Lib_t * p; - int i, clk = clock(); - p = ALLOC( Dar_Lib_t, 1 ); - memset( p, 0, sizeof(Dar_Lib_t) ); - // allocate objects - p->nObjs = nObjs; - p->pObjs = ALLOC( Dar_LibObj_t, nObjs ); - memset( p->pObjs, 0, sizeof(Dar_LibObj_t) * nObjs ); - // allocate canonical data - p->pPerms4 = Dar_Permutations( 4 ); - Dar_Truth4VarNPN( &p->puCanons, &p->pPhases, &p->pPerms, &p->pMap ); - // start the elementary objects - p->iObj = 4; - for ( i = 0; i < 4; i++ ) - { - p->pObjs[i].fTerm = 1; - p->pObjs[i].Num = uTruths[i]; - } -// PRT( "Library start", clock() - clk ); - return p; -} - -/**Function************************************************************* - - Synopsis [Frees the library.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void Dar_LibFree( Dar_Lib_t * p ) -{ - free( p->pObjs ); - free( p->pDatas ); - free( p->pNodesMem ); - free( p->pNodes0Mem ); - free( p->pSubgrMem ); - free( p->pSubgr0Mem ); - free( p->pPriosMem ); - FREE( p->pPlaceMem ); - FREE( p->pScoreMem ); - free( p->pPerms4 ); - free( p->puCanons ); - free( p->pPhases ); - free( p->pPerms ); - free( p->pMap ); - free( p ); -} - -/**Function************************************************************* - - Synopsis [Returns canonical truth tables.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void Dar_LibReturnCanonicals( unsigned * pCanons ) -{ - int Visits[222] = {0}; - int i, k; - // find canonical truth tables - for ( i = k = 0; i < (1<<16); i++ ) - if ( !Visits[s_DarLib->pMap[i]] ) - { - Visits[s_DarLib->pMap[i]] = 1; - pCanons[k++] = ((i<<16) | i); - } - assert( k == 222 ); -} - -/**Function************************************************************* - - Synopsis [Adds one AND to the library.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void Dar_LibAddNode( Dar_Lib_t * p, int Id0, int Id1, int fCompl0, int fCompl1 ) -{ - Dar_LibObj_t * pFan0 = Dar_LibObj( p, Id0 ); - Dar_LibObj_t * pFan1 = Dar_LibObj( p, Id1 ); - Dar_LibObj_t * pObj = p->pObjs + p->iObj++; - pObj->Fan0 = Id0; - pObj->Fan1 = Id1; - pObj->fCompl0 = fCompl0; - pObj->fCompl1 = fCompl1; - pObj->fPhase = (fCompl0 ^ pFan0->fPhase) & (fCompl1 ^ pFan1->fPhase); - pObj->Num = 0xFFFF & (fCompl0? ~pFan0->Num : pFan0->Num) & (fCompl1? ~pFan1->Num : pFan1->Num); -} - -/**Function************************************************************* - - Synopsis [Adds one AND to the library.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void Dar_LibSetup_rec( Dar_Lib_t * p, Dar_LibObj_t * pObj, int Class, int fCollect ) -{ - if ( pObj->fTerm || (int)pObj->Num == Class ) - return; - pObj->Num = Class; - Dar_LibSetup_rec( p, Dar_LibObj(p, pObj->Fan0), Class, fCollect ); - Dar_LibSetup_rec( p, Dar_LibObj(p, pObj->Fan1), Class, fCollect ); - if ( fCollect ) - p->pNodes[Class][ p->nNodes[Class]++ ] = pObj-p->pObjs; - else - p->nNodes[Class]++; -} - -/**Function************************************************************* - - Synopsis [Adds one AND to the library.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void Dar_LibSetup( Dar_Lib_t * p, Vec_Int_t * vOuts, Vec_Int_t * vPrios ) -{ - int fTraining = 0; - Dar_LibObj_t * pObj; - int nNodesTotal, uTruth, Class, Out, i, k; - assert( p->iObj == p->nObjs ); - - // count the number of representatives of each class - for ( i = 0; i < 222; i++ ) - p->nSubgr[i] = p->nNodes[i] = 0; - Vec_IntForEachEntry( vOuts, Out, i ) - { - pObj = Dar_LibObj( p, Out ); - uTruth = Dar_LibObjTruth( pObj ); - Class = p->pMap[uTruth]; - p->nSubgr[Class]++; - } - // allocate memory for the roots of each class - p->pSubgrMem = ALLOC( int, Vec_IntSize(vOuts) ); - p->pSubgr0Mem = ALLOC( int, Vec_IntSize(vOuts) ); - p->nSubgrTotal = 0; - for ( i = 0; i < 222; i++ ) - { - p->pSubgr[i] = p->pSubgrMem + p->nSubgrTotal; - p->pSubgr0[i] = p->pSubgr0Mem + p->nSubgrTotal; - p->nSubgrTotal += p->nSubgr[i]; - p->nSubgr[i] = 0; - } - assert( p->nSubgrTotal == Vec_IntSize(vOuts) ); - // add the outputs to storage - Vec_IntForEachEntry( vOuts, Out, i ) - { - pObj = Dar_LibObj( p, Out ); - uTruth = Dar_LibObjTruth( pObj ); - Class = p->pMap[uTruth]; - p->pSubgr[Class][ p->nSubgr[Class]++ ] = Out; - } - - if ( fTraining ) - { - // allocate memory for the priority of roots of each class - p->pPriosMem = ALLOC( int, Vec_IntSize(vOuts) ); - p->nSubgrTotal = 0; - for ( i = 0; i < 222; i++ ) - { - p->pPrios[i] = p->pPriosMem + p->nSubgrTotal; - p->nSubgrTotal += p->nSubgr[i]; - for ( k = 0; k < p->nSubgr[i]; k++ ) - p->pPrios[i][k] = k; - - } - assert( p->nSubgrTotal == Vec_IntSize(vOuts) ); - - // allocate memory for the priority of roots of each class - p->pPlaceMem = ALLOC( int, Vec_IntSize(vOuts) ); - p->nSubgrTotal = 0; - for ( i = 0; i < 222; i++ ) - { - p->pPlace[i] = p->pPlaceMem + p->nSubgrTotal; - p->nSubgrTotal += p->nSubgr[i]; - for ( k = 0; k < p->nSubgr[i]; k++ ) - p->pPlace[i][k] = k; - - } - assert( p->nSubgrTotal == Vec_IntSize(vOuts) ); - - // allocate memory for the priority of roots of each class - p->pScoreMem = ALLOC( int, Vec_IntSize(vOuts) ); - p->nSubgrTotal = 0; - for ( i = 0; i < 222; i++ ) - { - p->pScore[i] = p->pScoreMem + p->nSubgrTotal; - p->nSubgrTotal += p->nSubgr[i]; - for ( k = 0; k < p->nSubgr[i]; k++ ) - p->pScore[i][k] = 0; - - } - assert( p->nSubgrTotal == Vec_IntSize(vOuts) ); - } - else - { - int Counter = 0; - // allocate memory for the priority of roots of each class - p->pPriosMem = ALLOC( int, Vec_IntSize(vOuts) ); - p->nSubgrTotal = 0; - for ( i = 0; i < 222; i++ ) - { - p->pPrios[i] = p->pPriosMem + p->nSubgrTotal; - p->nSubgrTotal += p->nSubgr[i]; - for ( k = 0; k < p->nSubgr[i]; k++ ) - p->pPrios[i][k] = Vec_IntEntry(vPrios, Counter++); - - } - assert( p->nSubgrTotal == Vec_IntSize(vOuts) ); - assert( Counter == Vec_IntSize(vPrios) ); - } - - // create traversal IDs - for ( i = 0; i < p->iObj; i++ ) - Dar_LibObj(p, i)->Num = 0xff; - // count nodes in each class - for ( i = 0; i < 222; i++ ) - for ( k = 0; k < p->nSubgr[i]; k++ ) - Dar_LibSetup_rec( p, Dar_LibObj(p, p->pSubgr[i][k]), i, 0 ); - // count the total number of nodes - p->nNodesTotal = 0; - for ( i = 0; i < 222; i++ ) - p->nNodesTotal += p->nNodes[i]; - // allocate memory for the nodes of each class - p->pNodesMem = ALLOC( int, p->nNodesTotal ); - p->pNodes0Mem = ALLOC( int, p->nNodesTotal ); - p->nNodesTotal = 0; - for ( i = 0; i < 222; i++ ) - { - p->pNodes[i] = p->pNodesMem + p->nNodesTotal; - p->pNodes0[i] = p->pNodes0Mem + p->nNodesTotal; - p->nNodesTotal += p->nNodes[i]; - p->nNodes[i] = 0; - } - // create traversal IDs - for ( i = 0; i < p->iObj; i++ ) - Dar_LibObj(p, i)->Num = 0xff; - // add the nodes to storage - nNodesTotal = 0; - for ( i = 0; i < 222; i++ ) - { - for ( k = 0; k < p->nSubgr[i]; k++ ) - Dar_LibSetup_rec( p, Dar_LibObj(p, p->pSubgr[i][k]), i, 1 ); - nNodesTotal += p->nNodes[i]; -//printf( "Class %3d : Subgraphs = %4d. Nodes = %5d.\n", i, p->nSubgr[i], p->nNodes[i] ); - } - assert( nNodesTotal == p->nNodesTotal ); - // prepare the number of the PI nodes - for ( i = 0; i < 4; i++ ) - Dar_LibObj(p, i)->Num = i; -} - -/**Function************************************************************* - - Synopsis [Starts the library.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void Dar_LibCreateData( Dar_Lib_t * p, int nDatas ) -{ - if ( p->nDatas == nDatas ) - return; - FREE( p->pDatas ); - // allocate datas - p->nDatas = nDatas; - p->pDatas = ALLOC( Dar_LibDat_t, nDatas ); - memset( p->pDatas, 0, sizeof(Dar_LibDat_t) * nDatas ); -} - -/**Function************************************************************* - - Synopsis [Adds one AND to the library.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void Dar_LibSetup0_rec( Dar_Lib_t * p, Dar_LibObj_t * pObj, int Class, int fCollect ) -{ - if ( pObj->fTerm || (int)pObj->Num == Class ) - return; - pObj->Num = Class; - Dar_LibSetup0_rec( p, Dar_LibObj(p, pObj->Fan0), Class, fCollect ); - Dar_LibSetup0_rec( p, Dar_LibObj(p, pObj->Fan1), Class, fCollect ); - if ( fCollect ) - p->pNodes0[Class][ p->nNodes0[Class]++ ] = pObj-p->pObjs; - else - p->nNodes0[Class]++; -} - -/**Function************************************************************* - - Synopsis [Starts the library.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void Dar_LibPrepare( int nSubgraphs ) -{ - Dar_Lib_t * p = s_DarLib; - int i, k, nNodes0Total; - if ( p->nSubgraphs == nSubgraphs ) - return; - - // favor special classes: - // 1 : F = (!d*!c*!b*!a) - // 4 : F = (!d*!c*!(b*a)) - // 12 : F = (!d*!(c*!(!b*!a))) - // 20 : F = (!d*!(c*b*a)) - - // set the subgraph counters - p->nSubgr0Total = 0; - for ( i = 0; i < 222; i++ ) - { -// if ( i == 1 || i == 4 || i == 12 || i == 20 ) // special classes - if ( i == 1 ) // special classes - p->nSubgr0[i] = p->nSubgr[i]; - else - p->nSubgr0[i] = AIG_MIN( p->nSubgr[i], nSubgraphs ); - p->nSubgr0Total += p->nSubgr0[i]; - for ( k = 0; k < p->nSubgr0[i]; k++ ) - p->pSubgr0[i][k] = p->pSubgr[i][ p->pPrios[i][k] ]; - } - - // count the number of nodes - // clean node counters - for ( i = 0; i < 222; i++ ) - p->nNodes0[i] = 0; - // create traversal IDs - for ( i = 0; i < p->iObj; i++ ) - Dar_LibObj(p, i)->Num = 0xff; - // count nodes in each class - // count the total number of nodes and the largest class - p->nNodes0Total = 0; - p->nNodes0Max = 0; - for ( i = 0; i < 222; i++ ) - { - for ( k = 0; k < p->nSubgr0[i]; k++ ) - Dar_LibSetup0_rec( p, Dar_LibObj(p, p->pSubgr0[i][k]), i, 0 ); - p->nNodes0Total += p->nNodes0[i]; - p->nNodes0Max = AIG_MAX( p->nNodes0Max, p->nNodes0[i] ); - } - - // clean node counters - for ( i = 0; i < 222; i++ ) - p->nNodes0[i] = 0; - // create traversal IDs - for ( i = 0; i < p->iObj; i++ ) - Dar_LibObj(p, i)->Num = 0xff; - // add the nodes to storage - nNodes0Total = 0; - for ( i = 0; i < 222; i++ ) - { - for ( k = 0; k < p->nSubgr0[i]; k++ ) - Dar_LibSetup0_rec( p, Dar_LibObj(p, p->pSubgr0[i][k]), i, 1 ); - nNodes0Total += p->nNodes0[i]; - } - assert( nNodes0Total == p->nNodes0Total ); - // prepare the number of the PI nodes - for ( i = 0; i < 4; i++ ) - Dar_LibObj(p, i)->Num = i; - - // realloc the datas - Dar_LibCreateData( p, p->nNodes0Max + 32 ); - // allocated more because Dar_LibBuildBest() sometimes requires more entries -} - -/**Function************************************************************* - - Synopsis [Reads library from array.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -Dar_Lib_t * Dar_LibRead() -{ - Vec_Int_t * vObjs, * vOuts, * vPrios; - Dar_Lib_t * p; - int i; - // read nodes and outputs - vObjs = Dar_LibReadNodes(); - vOuts = Dar_LibReadOuts(); - vPrios = Dar_LibReadPrios(); - // create library - p = Dar_LibAlloc( Vec_IntSize(vObjs)/2 + 4 ); - // create nodes - for ( i = 0; i < vObjs->nSize; i += 2 ) - Dar_LibAddNode( p, vObjs->pArray[i] >> 1, vObjs->pArray[i+1] >> 1, - vObjs->pArray[i] & 1, vObjs->pArray[i+1] & 1 ); - // create outputs - Dar_LibSetup( p, vOuts, vPrios ); - Vec_IntFree( vObjs ); - Vec_IntFree( vOuts ); - Vec_IntFree( vPrios ); - return p; -} - -/**Function************************************************************* - - Synopsis [Starts the library.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void Dar_LibStart() -{ - int clk = clock(); - assert( s_DarLib == NULL ); - s_DarLib = Dar_LibRead(); -// printf( "The 4-input library started with %d nodes and %d subgraphs. ", s_DarLib->nObjs - 4, s_DarLib->nSubgrTotal ); -// PRT( "Time", clock() - clk ); -} - -/**Function************************************************************* - - Synopsis [Stops the library.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void Dar_LibStop() -{ - assert( s_DarLib != NULL ); - Dar_LibFree( s_DarLib ); - s_DarLib = NULL; -} - -/**Function************************************************************* - - Synopsis [Updates the score of the class and adjusts the priority of this class.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void Dar_LibIncrementScore( int Class, int Out, int Gain ) -{ - int * pPrios = s_DarLib->pPrios[Class]; // pPrios[i] = Out - int * pPlace = s_DarLib->pPlace[Class]; // pPlace[Out] = i - int * pScore = s_DarLib->pScore[Class]; // score of Out - int Out2; - assert( Class >= 0 && Class < 222 ); - assert( Out >= 0 && Out < s_DarLib->nSubgr[Class] ); - assert( pPlace[pPrios[Out]] == Out ); - // increment the score - pScore[Out] += Gain; - // move the out in the order - while ( pPlace[Out] > 0 && pScore[Out] > pScore[ pPrios[pPlace[Out]-1] ] ) - { - // get the previous output in the priority list - Out2 = pPrios[pPlace[Out]-1]; - // swap Out and Out2 - pPlace[Out]--; - pPlace[Out2]++; - pPrios[pPlace[Out]] = Out; - pPrios[pPlace[Out2]] = Out2; - } -} - -/**Function************************************************************* - - Synopsis [Prints out the priorities into the file.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void Dar_LibDumpPriorities() -{ - int i, k, Out, Out2, Counter = 0, Printed = 0; - printf( "\nOutput priorities (total = %d):\n", s_DarLib->nSubgrTotal ); - for ( i = 0; i < 222; i++ ) - { -// printf( "Class%d: ", i ); - for ( k = 0; k < s_DarLib->nSubgr[i]; k++ ) - { - Out = s_DarLib->pPrios[i][k]; - Out2 = k == 0 ? Out : s_DarLib->pPrios[i][k-1]; - assert( s_DarLib->pScore[i][Out2] >= s_DarLib->pScore[i][Out] ); -// printf( "%d(%d), ", Out, s_DarLib->pScore[i][Out] ); - printf( "%d, ", Out ); - Printed++; - if ( ++Counter == 15 ) - { - printf( "\n" ); - Counter = 0; - } - } - } - printf( "\n" ); - assert( Printed == s_DarLib->nSubgrTotal ); -} - - -/**Function************************************************************* - - Synopsis [Matches the cut with its canonical form.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -int Dar_LibCutMatch( Dar_Man_t * p, Dar_Cut_t * pCut ) -{ - Aig_Obj_t * pFanin; - unsigned uPhase; - char * pPerm; - int i; - assert( pCut->nLeaves == 4 ); - // get the fanin permutation - uPhase = s_DarLib->pPhases[pCut->uTruth]; - pPerm = s_DarLib->pPerms4[ s_DarLib->pPerms[pCut->uTruth] ]; - // collect fanins with the corresponding permutation/phase - for ( i = 0; i < (int)pCut->nLeaves; i++ ) - { - pFanin = Aig_ManObj( p->pAig, pCut->pLeaves[pPerm[i]] ); - if ( pFanin == NULL ) - { - p->nCutsBad++; - return 0; - } - pFanin = Aig_NotCond(pFanin, ((uPhase >> i) & 1) ); - s_DarLib->pDatas[i].pFunc = pFanin; - s_DarLib->pDatas[i].Level = Aig_Regular(pFanin)->Level; - } - p->nCutsGood++; - return 1; -} - - - -/**Function************************************************************* - - Synopsis [Marks the MFFC of the node.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -int Dar_LibCutMarkMffc( Aig_Man_t * p, Aig_Obj_t * pRoot, int nLeaves ) -{ - int i, nNodes; - // mark the cut leaves - for ( i = 0; i < nLeaves; i++ ) - Aig_Regular(s_DarLib->pDatas[i].pFunc)->nRefs++; - // label MFFC with current ID - nNodes = Aig_NodeMffsLabel( p, pRoot ); - // unmark the cut leaves - for ( i = 0; i < nLeaves; i++ ) - Aig_Regular(s_DarLib->pDatas[i].pFunc)->nRefs--; - return nNodes; -} - -/**Function************************************************************* - - Synopsis [Evaluates one cut.] - - Description [Returns the best gain.] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void Dar_LibObjPrint_rec( Dar_LibObj_t * pObj ) -{ - if ( pObj->fTerm ) - { - printf( "%c", 'a' + pObj - s_DarLib->pObjs ); - return; - } - printf( "(" ); - Dar_LibObjPrint_rec( Dar_LibObj(s_DarLib, pObj->Fan0) ); - if ( pObj->fCompl0 ) - printf( "\'" ); - Dar_LibObjPrint_rec( Dar_LibObj(s_DarLib, pObj->Fan1) ); - if ( pObj->fCompl0 ) - printf( "\'" ); - printf( ")" ); -} - - -/**Function************************************************************* - - Synopsis [Assigns numbers to the nodes of one class.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void Dar_LibEvalAssignNums( Dar_Man_t * p, int Class ) -{ - Dar_LibObj_t * pObj; - Dar_LibDat_t * pData, * pData0, * pData1; - Aig_Obj_t * pFanin0, * pFanin1; - int i; - for ( i = 0; i < s_DarLib->nNodes0[Class]; i++ ) - { - // get one class node, assign its temporary number and set its data - pObj = Dar_LibObj(s_DarLib, s_DarLib->pNodes0[Class][i]); - pObj->Num = 4 + i; - assert( (int)pObj->Num < s_DarLib->nNodes0Max + 4 ); - pData = s_DarLib->pDatas + pObj->Num; - pData->fMffc = 0; - pData->pFunc = NULL; - pData->TravId = 0xFFFF; - - // explore the fanins - assert( (int)Dar_LibObj(s_DarLib, pObj->Fan0)->Num < s_DarLib->nNodes0Max + 4 ); - assert( (int)Dar_LibObj(s_DarLib, pObj->Fan1)->Num < s_DarLib->nNodes0Max + 4 ); - pData0 = s_DarLib->pDatas + Dar_LibObj(s_DarLib, pObj->Fan0)->Num; - pData1 = s_DarLib->pDatas + Dar_LibObj(s_DarLib, pObj->Fan1)->Num; - pData->Level = 1 + AIG_MAX(pData0->Level, pData1->Level); - if ( pData0->pFunc == NULL || pData1->pFunc == NULL ) - continue; - pFanin0 = Aig_NotCond( pData0->pFunc, pObj->fCompl0 ); - pFanin1 = Aig_NotCond( pData1->pFunc, pObj->fCompl1 ); - pData->pFunc = Aig_TableLookupTwo( p->pAig, pFanin0, pFanin1 ); - if ( pData->pFunc ) - { - // update the level to be more accurate - pData->Level = Aig_Regular(pData->pFunc)->Level; - // mark the node if it is part of MFFC - pData->fMffc = Aig_ObjIsTravIdCurrent(p->pAig, pData->pFunc); - } - } -} - -/**Function************************************************************* - - Synopsis [Evaluates one cut.] - - Description [Returns the best gain.] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -int Dar_LibEval_rec( Dar_LibObj_t * pObj, int Out, int nNodesSaved, int Required ) -{ - Dar_LibDat_t * pData; - int Area; - if ( pObj->fTerm ) - return 0; - assert( pObj->Num > 3 ); - pData = s_DarLib->pDatas + pObj->Num; - if ( pData->Level > Required ) - return 0xff; - if ( pData->pFunc && !pData->fMffc ) - return 0; - if ( pData->TravId == Out ) - return 0; - pData->TravId = Out; - // this is a new node - get a bound on the area of its branches - nNodesSaved--; - Area = Dar_LibEval_rec( Dar_LibObj(s_DarLib, pObj->Fan0), Out, nNodesSaved, Required+1 ); - if ( Area > nNodesSaved ) - return 0xff; - Area += Dar_LibEval_rec( Dar_LibObj(s_DarLib, pObj->Fan1), Out, nNodesSaved, Required+1 ); - if ( Area > nNodesSaved ) - return 0xff; - return Area + 1; -} - -/**Function************************************************************* - - Synopsis [Evaluates one cut.] - - Description [Returns the best gain.] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void Dar_LibEval( Dar_Man_t * p, Aig_Obj_t * pRoot, Dar_Cut_t * pCut, int Required ) -{ - int fTraining = 0; - Dar_LibObj_t * pObj; - int Out, k, Class, nNodesSaved, nNodesAdded, nNodesGained, clk; - clk = clock(); - if ( pCut->nLeaves != 4 ) - return; - // check if the cut exits and assigns leaves and their levels - if ( !Dar_LibCutMatch(p, pCut) ) - return; - // mark MFFC of the node - nNodesSaved = Dar_LibCutMarkMffc( p->pAig, pRoot, pCut->nLeaves ); - // evaluate the cut - Class = s_DarLib->pMap[pCut->uTruth]; - Dar_LibEvalAssignNums( p, Class ); - // profile outputs by their savings - p->nTotalSubgs += s_DarLib->nSubgr0[Class]; - p->ClassSubgs[Class] += s_DarLib->nSubgr0[Class]; - for ( Out = 0; Out < s_DarLib->nSubgr0[Class]; Out++ ) - { - pObj = Dar_LibObj(s_DarLib, s_DarLib->pSubgr0[Class][Out]); - if ( Aig_Regular(s_DarLib->pDatas[pObj->Num].pFunc) == pRoot ) - continue; - nNodesAdded = Dar_LibEval_rec( pObj, Out, nNodesSaved - !p->pPars->fUseZeros, Required ); - nNodesGained = nNodesSaved - nNodesAdded; - if ( fTraining && nNodesGained >= 0 ) - Dar_LibIncrementScore( Class, Out, nNodesGained + 1 ); - if ( nNodesGained < 0 || (nNodesGained == 0 && !p->pPars->fUseZeros) ) - continue; - if ( nNodesGained < p->GainBest || - (nNodesGained == p->GainBest && s_DarLib->pDatas[pObj->Num].Level >= p->LevelBest) ) - continue; - // remember this possibility - Vec_PtrClear( p->vLeavesBest ); - for ( k = 0; k < (int)pCut->nLeaves; k++ ) - Vec_PtrPush( p->vLeavesBest, s_DarLib->pDatas[k].pFunc ); - p->OutBest = s_DarLib->pSubgr0[Class][Out]; - p->OutNumBest = Out; - p->LevelBest = s_DarLib->pDatas[pObj->Num].Level; - p->GainBest = nNodesGained; - p->ClassBest = Class; - assert( p->LevelBest <= Required ); - } -clk = clock() - clk; -p->ClassTimes[Class] += clk; -p->timeEval += clk; -} - -/**Function************************************************************* - - Synopsis [Clears the fields of the nodes used in this cut.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void Dar_LibBuildClear_rec( Dar_LibObj_t * pObj, int * pCounter ) -{ - if ( pObj->fTerm ) - return; - pObj->Num = (*pCounter)++; - s_DarLib->pDatas[ pObj->Num ].pFunc = NULL; - Dar_LibBuildClear_rec( Dar_LibObj(s_DarLib, pObj->Fan0), pCounter ); - Dar_LibBuildClear_rec( Dar_LibObj(s_DarLib, pObj->Fan1), pCounter ); -} - -/**Function************************************************************* - - Synopsis [Reconstructs the best cut.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -Aig_Obj_t * Dar_LibBuildBest_rec( Dar_Man_t * p, Dar_LibObj_t * pObj ) -{ - Aig_Obj_t * pFanin0, * pFanin1; - Dar_LibDat_t * pData = s_DarLib->pDatas + pObj->Num; - if ( pData->pFunc ) - return pData->pFunc; - pFanin0 = Dar_LibBuildBest_rec( p, Dar_LibObj(s_DarLib, pObj->Fan0) ); - pFanin1 = Dar_LibBuildBest_rec( p, Dar_LibObj(s_DarLib, pObj->Fan1) ); - pFanin0 = Aig_NotCond( pFanin0, pObj->fCompl0 ); - pFanin1 = Aig_NotCond( pFanin1, pObj->fCompl1 ); - pData->pFunc = Aig_And( p->pAig, pFanin0, pFanin1 ); -// assert( pData->Level == (int)Aig_Regular(pData->pFunc)->Level ); - return pData->pFunc; -} - -/**Function************************************************************* - - Synopsis [Reconstructs the best cut.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -Aig_Obj_t * Dar_LibBuildBest( Dar_Man_t * p ) -{ - int i, Counter = 4; - for ( i = 0; i < Vec_PtrSize(p->vLeavesBest); i++ ) - s_DarLib->pDatas[i].pFunc = Vec_PtrEntry( p->vLeavesBest, i ); - Dar_LibBuildClear_rec( Dar_LibObj(s_DarLib, p->OutBest), &Counter ); - return Dar_LibBuildBest_rec( p, Dar_LibObj(s_DarLib, p->OutBest) ); -} - - -//////////////////////////////////////////////////////////////////////// -/// END OF FILE /// -//////////////////////////////////////////////////////////////////////// - - -- cgit v1.2.3