From 0c6505a26a537dc911b6566f82d759521e527c08 Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Wed, 30 Jan 2008 20:01:00 -0800 Subject: Version abc80130_2 --- src/aig/dar/darLib.c | 980 +++++++++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 980 insertions(+) create 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 new file mode 100644 index 00000000..e0e97055 --- /dev/null +++ b/src/aig/dar/darLib.c @@ -0,0 +1,980 @@ +/**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[ (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; + } + 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' + (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 ) +{ + 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