| /**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" |
| #include "aig/gia/gia.h" |
| #include "dar.h" |
| |
| ABC_NAMESPACE_IMPL_START |
| |
| |
| //////////////////////////////////////////////////////////////////////// |
| /// 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 |
| { |
| union { |
| Aig_Obj_t * pFunc; // the corresponding AIG node if it exists |
| int iGunc; }; // 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 |
| float dProb; // probability of the node being 1 |
| 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 = Abc_Clock(); |
| p = ABC_ALLOC( Dar_Lib_t, 1 ); |
| memset( p, 0, sizeof(Dar_Lib_t) ); |
| // allocate objects |
| p->nObjs = nObjs; |
| p->pObjs = ABC_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]; |
| } |
| // ABC_PRT( "Library start", Abc_Clock() - clk ); |
| return p; |
| } |
| |
| /**Function************************************************************* |
| |
| Synopsis [Frees the library.] |
| |
| Description [] |
| |
| SideEffects [] |
| |
| SeeAlso [] |
| |
| ***********************************************************************/ |
| void Dar_LibFree( Dar_Lib_t * p ) |
| { |
| ABC_FREE( p->pObjs ); |
| ABC_FREE( p->pDatas ); |
| ABC_FREE( p->pNodesMem ); |
| ABC_FREE( p->pNodes0Mem ); |
| ABC_FREE( p->pSubgrMem ); |
| ABC_FREE( p->pSubgr0Mem ); |
| ABC_FREE( p->pPriosMem ); |
| ABC_FREE( p->pPlaceMem ); |
| ABC_FREE( p->pScoreMem ); |
| ABC_FREE( p->pPerms4 ); |
| ABC_FREE( p->puCanons ); |
| ABC_FREE( p->pPhases ); |
| ABC_FREE( p->pPerms ); |
| ABC_FREE( p->pMap ); |
| ABC_FREE( p ); |
| } |
| |
| /**Function************************************************************* |
| |
| Synopsis [Returns canonical truth tables.] |
| |
| Description [] |
| |
| SideEffects [] |
| |
| SeeAlso [] |
| |
| ***********************************************************************/ |
| int Dar_LibReturnClass( unsigned uTruth ) |
| { |
| return s_DarLib->pMap[uTruth & 0xffff]; |
| } |
| |
| |
| /**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 = ABC_ALLOC( int, Vec_IntSize(vOuts) ); |
| p->pSubgr0Mem = ABC_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 = ABC_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 = ABC_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 = ABC_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 = ABC_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 = ABC_ALLOC( int, p->nNodesTotal ); |
| p->pNodes0Mem = ABC_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; |
| ABC_FREE( p->pDatas ); |
| // allocate datas |
| p->nDatas = nDatas; |
| p->pDatas = ABC_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] = Abc_MinInt( 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 = Abc_MaxInt( 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() |
| { |
| // abctime clk = Abc_Clock(); |
| if ( s_DarLib != NULL ) |
| return; |
| 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 ); |
| // ABC_PRT( "Time", Abc_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[ (int)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[ (int)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; |
| // copy the propability of node being one |
| if ( p->pPars->fPower ) |
| { |
| float Prob = Abc_Int2Float( Vec_IntEntry( p->pAig->vProbs, Aig_ObjId(Aig_Regular(pFanin)) ) ); |
| s_DarLib->pDatas[i].dProb = Aig_IsComplement(pFanin)? 1.0-Prob : Prob; |
| } |
| } |
| 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, float * pPower ) |
| { |
| 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_NodeMffcLabel( p, pRoot, pPower ); |
| // 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' + (int)(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, Aig_Obj_t * pRoot ) |
| { |
| 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 + Abc_MaxInt(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 ); |
| if ( Aig_Regular(pFanin0) == pRoot || Aig_Regular(pFanin1) == pRoot ) |
| continue; |
| 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, Aig_Regular(pData->pFunc)); |
| // assign the probability |
| if ( p->pPars->fPower ) |
| { |
| float Prob = Abc_Int2Float( Vec_IntEntry( p->pAig->vProbs, Aig_ObjId(Aig_Regular(pData->pFunc)) ) ); |
| pData->dProb = Aig_IsComplement(pData->pFunc)? 1.0-Prob : Prob; |
| } |
| } |
| } |
| } |
| |
| /**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, float * pPower ) |
| { |
| Dar_LibDat_t * pData; |
| float Power0, Power1; |
| int Area; |
| if ( pPower ) |
| *pPower = (float)0.0; |
| pData = s_DarLib->pDatas + pObj->Num; |
| if ( pData->TravId == Out ) |
| return 0; |
| pData->TravId = Out; |
| if ( pObj->fTerm ) |
| { |
| if ( pPower ) |
| *pPower = pData->dProb; |
| return 0; |
| } |
| assert( pObj->Num > 3 ); |
| if ( pData->Level > Required ) |
| return 0xff; |
| if ( pData->pFunc && !pData->fMffc ) |
| { |
| if ( pPower ) |
| *pPower = pData->dProb; |
| return 0; |
| } |
| // 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, pPower? &Power0 : NULL ); |
| if ( Area > nNodesSaved ) |
| return 0xff; |
| Area += Dar_LibEval_rec( Dar_LibObj(s_DarLib, pObj->Fan1), Out, nNodesSaved, Required+1, pPower? &Power1 : NULL ); |
| if ( Area > nNodesSaved ) |
| return 0xff; |
| if ( pPower ) |
| { |
| Dar_LibDat_t * pData0 = s_DarLib->pDatas + Dar_LibObj(s_DarLib, pObj->Fan0)->Num; |
| Dar_LibDat_t * pData1 = s_DarLib->pDatas + Dar_LibObj(s_DarLib, pObj->Fan1)->Num; |
| pData->dProb = (pObj->fCompl0? 1.0 - pData0->dProb : pData0->dProb)* |
| (pObj->fCompl1? 1.0 - pData1->dProb : pData1->dProb); |
| *pPower = Power0 + 2.0 * pData0->dProb * (1.0 - pData0->dProb) + |
| Power1 + 2.0 * pData1->dProb * (1.0 - pData1->dProb); |
| } |
| 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 * pnMffcSize ) |
| { |
| int fTraining = 0; |
| float PowerSaved, PowerAdded; |
| Dar_LibObj_t * pObj; |
| int Out, k, Class, nNodesSaved, nNodesAdded, nNodesGained; |
| abctime clk = Abc_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, p->pPars->fPower? &PowerSaved : NULL ); |
| // evaluate the cut |
| Class = s_DarLib->pMap[pCut->uTruth]; |
| Dar_LibEvalAssignNums( p, Class, pRoot ); |
| // 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, p->pPars->fPower? &PowerAdded : NULL ); |
| nNodesGained = nNodesSaved - nNodesAdded; |
| if ( p->pPars->fPower && PowerSaved < PowerAdded ) |
| continue; |
| 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 ); |
| *pnMffcSize = nNodesSaved; |
| } |
| clk = Abc_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 = (Aig_Obj_t *)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) ); |
| } |
| |
| |
| |
| |
| |
| |
| /**Function************************************************************* |
| |
| Synopsis [Matches the cut with its canonical form.] |
| |
| Description [] |
| |
| SideEffects [] |
| |
| SeeAlso [] |
| |
| ***********************************************************************/ |
| int Dar2_LibCutMatch( Gia_Man_t * p, Vec_Int_t * vCutLits, unsigned uTruth ) |
| { |
| unsigned uPhase; |
| char * pPerm; |
| int i; |
| assert( Vec_IntSize(vCutLits) == 4 ); |
| // get the fanin permutation |
| uPhase = s_DarLib->pPhases[uTruth]; |
| pPerm = s_DarLib->pPerms4[ (int)s_DarLib->pPerms[uTruth] ]; |
| // collect fanins with the corresponding permutation/phase |
| for ( i = 0; i < Vec_IntSize(vCutLits); i++ ) |
| { |
| // pFanin = Gia_ManObj( p, pCut->pLeaves[ (int)pPerm[i] ] ); |
| // pFanin = Gia_ManObj( p, Vec_IntEntry( vCutLits, (int)pPerm[i] ) ); |
| // pFanin = Gia_ObjFromLit( p, Vec_IntEntry( vCutLits, (int)pPerm[i] ) ); |
| s_DarLib->pDatas[i].iGunc = Abc_LitNotCond( Vec_IntEntry(vCutLits, (int)pPerm[i]), ((uPhase >> i) & 1) ); |
| s_DarLib->pDatas[i].Level = Gia_ObjLevel( p, Gia_Regular(Gia_ObjFromLit(p, s_DarLib->pDatas[i].iGunc)) ); |
| } |
| return 1; |
| } |
| |
| /**Function************************************************************* |
| |
| Synopsis [Assigns numbers to the nodes of one class.] |
| |
| Description [] |
| |
| SideEffects [] |
| |
| SeeAlso [] |
| |
| ***********************************************************************/ |
| void Dar2_LibEvalAssignNums( Gia_Man_t * p, int Class ) |
| { |
| Dar_LibObj_t * pObj; |
| Dar_LibDat_t * pData, * pData0, * pData1; |
| int iFanin0, iFanin1, i, iLit; |
| 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->iGunc = -1; |
| 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 + Abc_MaxInt(pData0->Level, pData1->Level); |
| if ( pData0->iGunc == -1 || pData1->iGunc == -1 ) |
| continue; |
| iFanin0 = Abc_LitNotCond( pData0->iGunc, pObj->fCompl0 ); |
| iFanin1 = Abc_LitNotCond( pData1->iGunc, pObj->fCompl1 ); |
| // compute the resulting literal |
| if ( iFanin0 == 0 || iFanin1 == 0 || iFanin0 == Abc_LitNot(iFanin1) ) |
| iLit = 0; |
| else if ( iFanin0 == 1 || iFanin0 == iFanin1 ) |
| iLit = iFanin1; |
| else if ( iFanin1 == 1 ) |
| iLit = iFanin0; |
| else |
| { |
| iLit = Gia_ManHashLookup( p, Gia_ObjFromLit(p, iFanin0), Gia_ObjFromLit(p, iFanin1) ); |
| if ( iLit == 0 ) |
| iLit = -1; |
| } |
| pData->iGunc = iLit; |
| if ( pData->iGunc >= 0 ) |
| { |
| // update the level to be more accurate |
| pData->Level = Gia_ObjLevel( p, Gia_Regular(Gia_ObjFromLit(p, pData->iGunc)) ); |
| // mark the node if it is part of MFFC |
| // pData->fMffc = Gia_ObjIsTravIdCurrentArray(p, Gia_Regular(pData->pGunc)); |
| } |
| } |
| } |
| |
| /**Function************************************************************* |
| |
| Synopsis [Evaluates one cut.] |
| |
| Description [Returns the best gain.] |
| |
| SideEffects [] |
| |
| SeeAlso [] |
| |
| ***********************************************************************/ |
| int Dar2_LibEval_rec( Dar_LibObj_t * pObj, int Out ) |
| { |
| Dar_LibDat_t * pData; |
| int Area; |
| pData = s_DarLib->pDatas + pObj->Num; |
| if ( pData->TravId == Out ) |
| return 0; |
| pData->TravId = Out; |
| if ( pObj->fTerm ) |
| return 0; |
| assert( pObj->Num > 3 ); |
| if ( pData->iGunc >= 0 )//&& !pData->fMffc ) |
| return 0; |
| // this is a new node - get a bound on the area of its branches |
| // nNodesSaved--; |
| Area = Dar2_LibEval_rec( Dar_LibObj(s_DarLib, pObj->Fan0), Out ); |
| // if ( Area > nNodesSaved ) |
| // return 0xff; |
| Area += Dar2_LibEval_rec( Dar_LibObj(s_DarLib, pObj->Fan1), Out ); |
| // if ( Area > nNodesSaved ) |
| // return 0xff; |
| return Area + 1; |
| } |
| |
| /**Function************************************************************* |
| |
| Synopsis [Evaluates one cut.] |
| |
| Description [Returns the best gain.] |
| |
| SideEffects [] |
| |
| SeeAlso [] |
| |
| ***********************************************************************/ |
| int Dar2_LibEval( Gia_Man_t * p, Vec_Int_t * vCutLits, unsigned uTruth, int fKeepLevel, Vec_Int_t * vLeavesBest2 ) |
| { |
| int p_OutBest = -1; |
| int p_OutNumBest = -1; |
| int p_LevelBest = 1000000; |
| int p_GainBest = -1000000; |
| int p_ClassBest = -1; |
| // int fTraining = 0; |
| Dar_LibObj_t * pObj; |
| int Out, k, Class, nNodesSaved, nNodesAdded, nNodesGained; |
| // abctime clk = Abc_Clock(); |
| assert( Vec_IntSize(vCutLits) == 4 ); |
| assert( (uTruth >> 16) == 0 ); |
| // check if the cut exits and assigns leaves and their levels |
| if ( !Dar2_LibCutMatch(p, vCutLits, uTruth) ) |
| return -1; |
| // mark MFFC of the node |
| // nNodesSaved = Dar2_LibCutMarkMffc( p->pAig, pRoot, pCut->nLeaves, p->pPars->fPower? &PowerSaved : NULL ); |
| nNodesSaved = 0; |
| // evaluate the cut |
| Class = s_DarLib->pMap[uTruth]; |
| Dar2_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]); |
| // nNodesAdded = Dar2_LibEval_rec( pObj, Out, nNodesSaved - !p->pPars->fUseZeros, Required, p->pPars->fPower? &PowerAdded : NULL ); |
| nNodesAdded = Dar2_LibEval_rec( pObj, Out ); |
| nNodesGained = nNodesSaved - nNodesAdded; |
| if ( fKeepLevel ) |
| { |
| if ( s_DarLib->pDatas[pObj->Num].Level > p_LevelBest || |
| (s_DarLib->pDatas[pObj->Num].Level == p_LevelBest && nNodesGained <= p_GainBest) ) |
| continue; |
| } |
| else |
| { |
| if ( nNodesGained < p_GainBest || |
| (nNodesGained == p_GainBest && s_DarLib->pDatas[pObj->Num].Level >= p_LevelBest) ) |
| continue; |
| } |
| // remember this possibility |
| Vec_IntClear( vLeavesBest2 ); |
| for ( k = 0; k < Vec_IntSize(vCutLits); k++ ) |
| Vec_IntPush( vLeavesBest2, s_DarLib->pDatas[k].iGunc ); |
| 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 = Abc_Clock() - clk; |
| //p->ClassTimes[Class] += clk; |
| //p->timeEval += clk; |
| assert( p_OutBest != -1 ); |
| return p_OutBest; |
| } |
| |
| /**Function************************************************************* |
| |
| Synopsis [Clears the fields of the nodes used i this cut.] |
| |
| Description [] |
| |
| SideEffects [] |
| |
| SeeAlso [] |
| |
| ***********************************************************************/ |
| void Dar2_LibBuildClear_rec( Dar_LibObj_t * pObj, int * pCounter ) |
| { |
| if ( pObj->fTerm ) |
| return; |
| pObj->Num = (*pCounter)++; |
| s_DarLib->pDatas[ pObj->Num ].iGunc = -1; |
| Dar2_LibBuildClear_rec( Dar_LibObj(s_DarLib, pObj->Fan0), pCounter ); |
| Dar2_LibBuildClear_rec( Dar_LibObj(s_DarLib, pObj->Fan1), pCounter ); |
| } |
| |
| /**Function************************************************************* |
| |
| Synopsis [Reconstructs the best cut.] |
| |
| Description [] |
| |
| SideEffects [] |
| |
| SeeAlso [] |
| |
| ***********************************************************************/ |
| int Dar2_LibBuildBest_rec( Gia_Man_t * p, Dar_LibObj_t * pObj ) |
| { |
| Gia_Obj_t * pNode; |
| Dar_LibDat_t * pData; |
| int iFanin0, iFanin1; |
| pData = s_DarLib->pDatas + pObj->Num; |
| if ( pData->iGunc >= 0 ) |
| return pData->iGunc; |
| iFanin0 = Dar2_LibBuildBest_rec( p, Dar_LibObj(s_DarLib, pObj->Fan0) ); |
| iFanin1 = Dar2_LibBuildBest_rec( p, Dar_LibObj(s_DarLib, pObj->Fan1) ); |
| iFanin0 = Abc_LitNotCond( iFanin0, pObj->fCompl0 ); |
| iFanin1 = Abc_LitNotCond( iFanin1, pObj->fCompl1 ); |
| pData->iGunc = Gia_ManHashAnd( p, iFanin0, iFanin1 ); |
| pNode = Gia_ManObj( p, Abc_Lit2Var(pData->iGunc) ); |
| if ( Gia_ObjIsAnd( pNode ) ) |
| Gia_ObjSetAndLevel( p, pNode ); |
| Gia_ObjSetPhase( p, pNode ); |
| return pData->iGunc; |
| } |
| |
| /**Function************************************************************* |
| |
| Synopsis [Reconstructs the best cut.] |
| |
| Description [] |
| |
| SideEffects [] |
| |
| SeeAlso [] |
| |
| ***********************************************************************/ |
| int Dar2_LibBuildBest( Gia_Man_t * p, Vec_Int_t * vLeavesBest2, int OutBest ) |
| { |
| int i, iLeaf, Counter = 4; |
| assert( Vec_IntSize(vLeavesBest2) == 4 ); |
| Vec_IntForEachEntry( vLeavesBest2, iLeaf, i ) |
| s_DarLib->pDatas[i].iGunc = iLeaf; |
| Dar2_LibBuildClear_rec( Dar_LibObj(s_DarLib, OutBest), &Counter ); |
| return Dar2_LibBuildBest_rec( p, Dar_LibObj(s_DarLib, OutBest) ); |
| } |
| |
| /**Function************************************************************* |
| |
| Synopsis [Evaluate and build the new node.] |
| |
| Description [] |
| |
| SideEffects [] |
| |
| SeeAlso [] |
| |
| ***********************************************************************/ |
| int Dar_LibEvalBuild( Gia_Man_t * p, Vec_Int_t * vCutLits, unsigned uTruth, int fKeepLevel, Vec_Int_t * vLeavesBest2 ) |
| { |
| int OutBest = Dar2_LibEval( p, vCutLits, uTruth, fKeepLevel, vLeavesBest2 ); |
| return Dar2_LibBuildBest( p, vLeavesBest2, OutBest ); |
| } |
| |
| //////////////////////////////////////////////////////////////////////// |
| /// END OF FILE /// |
| //////////////////////////////////////////////////////////////////////// |
| |
| |
| ABC_NAMESPACE_IMPL_END |
| |
