src/aig/dar/darLib.c File Reference

#include "darInt.h"
Include dependency graph for darLib.c:

Go to the source code of this file.

Data Structures

struct  Dar_LibObj_t_
struct  Dar_LibDat_t_
struct  Dar_Lib_t_

Typedefs

typedef struct Dar_Lib_t_ Dar_Lib_t
typedef struct Dar_LibObj_t_ Dar_LibObj_t
typedef struct Dar_LibDat_t_ Dar_LibDat_t

Functions

static Dar_LibObj_t * Dar_LibObj (Dar_Lib_t *p, int Id)
static int Dar_LibObjTruth (Dar_LibObj_t *pObj)
Dar_Lib_t * Dar_LibAlloc (int nObjs)
void Dar_LibFree (Dar_Lib_t *p)
void Dar_LibReturnCanonicals (unsigned *pCanons)
void Dar_LibAddNode (Dar_Lib_t *p, int Id0, int Id1, int fCompl0, int fCompl1)
void Dar_LibSetup_rec (Dar_Lib_t *p, Dar_LibObj_t *pObj, int Class, int fCollect)
void Dar_LibSetup (Dar_Lib_t *p, Vec_Int_t *vOuts, Vec_Int_t *vPrios)
void Dar_LibCreateData (Dar_Lib_t *p, int nDatas)
void Dar_LibSetup0_rec (Dar_Lib_t *p, Dar_LibObj_t *pObj, int Class, int fCollect)
void Dar_LibPrepare (int nSubgraphs)
Dar_Lib_t * Dar_LibRead ()
void Dar_LibStart ()
void Dar_LibStop ()
void Dar_LibIncrementScore (int Class, int Out, int Gain)
void Dar_LibDumpPriorities ()
int Dar_LibCutMatch (Dar_Man_t *p, Dar_Cut_t *pCut)
int Dar_LibCutMarkMffc (Aig_Man_t *p, Aig_Obj_t *pRoot, int nLeaves)
void Dar_LibObjPrint_rec (Dar_LibObj_t *pObj)
void Dar_LibEvalAssignNums (Dar_Man_t *p, int Class)
int Dar_LibEval_rec (Dar_LibObj_t *pObj, int Out, int nNodesSaved, int Required)
void Dar_LibEval (Dar_Man_t *p, Aig_Obj_t *pRoot, Dar_Cut_t *pCut, int Required)
void Dar_LibBuildClear_rec (Dar_LibObj_t *pObj, int *pCounter)
Aig_Obj_t * Dar_LibBuildBest_rec (Dar_Man_t *p, Dar_LibObj_t *pObj)
Aig_Obj_t * Dar_LibBuildBest (Dar_Man_t *p)

Variables

static Dar_Lib_t * s_DarLib = NULL

Typedef Documentation

typedef struct Dar_Lib_t_ Dar_Lib_t

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

] DECLARATIONS ///

Definition at line 27 of file darLib.c.

typedef struct Dar_LibDat_t_ Dar_LibDat_t

Definition at line 29 of file darLib.c.

typedef struct Dar_LibObj_t_ Dar_LibObj_t

Definition at line 28 of file darLib.c.

Function Documentation

void Dar_LibAddNode ( Dar_Lib_t *  p,
int  Id0,
int  Id1,
int  fCompl0,
int  fCompl1 
)

Function*************************************************************

Synopsis [Adds one AND to the library.]

Description []

SideEffects []

SeeAlso []

Definition at line 211 of file darLib.c.

00212 {
00213     Dar_LibObj_t * pFan0 = Dar_LibObj( p, Id0 );
00214     Dar_LibObj_t * pFan1 = Dar_LibObj( p, Id1 );
00215     Dar_LibObj_t * pObj  = p->pObjs + p->iObj++;
00216     pObj->Fan0 = Id0;
00217     pObj->Fan1 = Id1;
00218     pObj->fCompl0 = fCompl0;
00219     pObj->fCompl1 = fCompl1;
00220     pObj->fPhase = (fCompl0 ^ pFan0->fPhase) & (fCompl1 ^ pFan1->fPhase);
00221     pObj->Num = 0xFFFF & (fCompl0? ~pFan0->Num : pFan0->Num) & (fCompl1? ~pFan1->Num : pFan1->Num);
00222 }

Dar_Lib_t* Dar_LibAlloc ( int  nObjs  ) 

FUNCTION DEFINITIONS ///Function*************************************************************

Synopsis [Starts the library.]

Description []

SideEffects []

SeeAlso []

Definition at line 120 of file darLib.c.

00121 {
00122     unsigned uTruths[4] = { 0xAAAA, 0xCCCC, 0xF0F0, 0xFF00 };
00123     Dar_Lib_t * p;
00124     int i;//, clk = clock();
00125     p = ALLOC( Dar_Lib_t, 1 );
00126     memset( p, 0, sizeof(Dar_Lib_t) );
00127     // allocate objects
00128     p->nObjs = nObjs;
00129     p->pObjs = ALLOC( Dar_LibObj_t, nObjs );
00130     memset( p->pObjs, 0, sizeof(Dar_LibObj_t) * nObjs );
00131     // allocate canonical data
00132     p->pPerms4 = Dar_Permutations( 4 );
00133     Dar_Truth4VarNPN( &p->puCanons, &p->pPhases, &p->pPerms, &p->pMap );
00134     // start the elementary objects
00135     p->iObj = 4;
00136     for ( i = 0; i < 4; i++ )
00137     {
00138         p->pObjs[i].fTerm = 1;
00139         p->pObjs[i].Num = uTruths[i];
00140     }
00141 //    PRT( "Library start", clock() - clk );
00142     return p;
00143 }

Aig_Obj_t* Dar_LibBuildBest ( Dar_Man_t *  p  ) 

Function*************************************************************

Synopsis [Reconstructs the best cut.]

Description []

SideEffects []

SeeAlso []

Definition at line 966 of file darLib.c.

00967 {
00968     int i, Counter = 4;
00969     for ( i = 0; i < Vec_PtrSize(p->vLeavesBest); i++ )
00970         s_DarLib->pDatas[i].pFunc = Vec_PtrEntry( p->vLeavesBest, i );
00971     Dar_LibBuildClear_rec( Dar_LibObj(s_DarLib, p->OutBest), &Counter );
00972     return Dar_LibBuildBest_rec( p, Dar_LibObj(s_DarLib, p->OutBest) );
00973 }

Aig_Obj_t* Dar_LibBuildBest_rec ( Dar_Man_t *  p,
Dar_LibObj_t *  pObj 
)

Function*************************************************************

Synopsis [Reconstructs the best cut.]

Description []

SideEffects []

SeeAlso []

Definition at line 940 of file darLib.c.

00941 {
00942     Aig_Obj_t * pFanin0, * pFanin1;
00943     Dar_LibDat_t * pData = s_DarLib->pDatas + pObj->Num;
00944     if ( pData->pFunc )
00945         return pData->pFunc;
00946     pFanin0 = Dar_LibBuildBest_rec( p, Dar_LibObj(s_DarLib, pObj->Fan0) );
00947     pFanin1 = Dar_LibBuildBest_rec( p, Dar_LibObj(s_DarLib, pObj->Fan1) );
00948     pFanin0 = Aig_NotCond( pFanin0, pObj->fCompl0 );
00949     pFanin1 = Aig_NotCond( pFanin1, pObj->fCompl1 );
00950     pData->pFunc = Aig_And( p->pAig, pFanin0, pFanin1 );
00951 //    assert( pData->Level == (int)Aig_Regular(pData->pFunc)->Level );
00952     return pData->pFunc;
00953 }

void Dar_LibBuildClear_rec ( Dar_LibObj_t *  pObj,
int *  pCounter 
)

Function*************************************************************

Synopsis [Clears the fields of the nodes used in this cut.]

Description []

SideEffects []

SeeAlso []

Definition at line 919 of file darLib.c.

00920 {
00921     if ( pObj->fTerm )
00922         return;
00923     pObj->Num = (*pCounter)++;
00924     s_DarLib->pDatas[ pObj->Num ].pFunc = NULL;
00925     Dar_LibBuildClear_rec( Dar_LibObj(s_DarLib, pObj->Fan0), pCounter );
00926     Dar_LibBuildClear_rec( Dar_LibObj(s_DarLib, pObj->Fan1), pCounter );
00927 }

void Dar_LibCreateData ( Dar_Lib_t *  p,
int  nDatas 
)

Function*************************************************************

Synopsis [Starts the library.]

Description []

SideEffects []

SeeAlso []

Definition at line 407 of file darLib.c.

00408 {
00409     if ( p->nDatas == nDatas )
00410         return;
00411     FREE( p->pDatas );
00412     // allocate datas
00413     p->nDatas = nDatas;
00414     p->pDatas = ALLOC( Dar_LibDat_t, nDatas );
00415     memset( p->pDatas, 0, sizeof(Dar_LibDat_t) * nDatas );
00416 }

int Dar_LibCutMarkMffc ( Aig_Man_t *  p,
Aig_Obj_t *  pRoot,
int  nLeaves 
)

Function*************************************************************

Synopsis [Marks the MFFC of the node.]

Description []

SideEffects []

SeeAlso []

Definition at line 719 of file darLib.c.

00720 {
00721     int i, nNodes;
00722     // mark the cut leaves
00723     for ( i = 0; i < nLeaves; i++ )
00724         Aig_Regular(s_DarLib->pDatas[i].pFunc)->nRefs++;
00725     // label MFFC with current ID
00726     nNodes = Aig_NodeMffsLabel( p, pRoot );
00727     // unmark the cut leaves
00728     for ( i = 0; i < nLeaves; i++ )
00729         Aig_Regular(s_DarLib->pDatas[i].pFunc)->nRefs--;
00730     return nNodes;
00731 }

int Dar_LibCutMatch ( Dar_Man_t *  p,
Dar_Cut_t *  pCut 
)

Function*************************************************************

Synopsis [Matches the cut with its canonical form.]

Description []

SideEffects []

SeeAlso []

Definition at line 679 of file darLib.c.

00680 {
00681     Aig_Obj_t * pFanin;
00682     unsigned uPhase;
00683     char * pPerm;
00684     int i;
00685     assert( pCut->nLeaves == 4 );
00686     // get the fanin permutation
00687     uPhase = s_DarLib->pPhases[pCut->uTruth];
00688     pPerm = s_DarLib->pPerms4[ (int)s_DarLib->pPerms[pCut->uTruth] ];
00689     // collect fanins with the corresponding permutation/phase
00690     for ( i = 0; i < (int)pCut->nLeaves; i++ )
00691     {
00692         pFanin = Aig_ManObj( p->pAig, pCut->pLeaves[ (int)pPerm[i] ] );
00693         if ( pFanin == NULL )
00694         {
00695             p->nCutsBad++;
00696             return 0;
00697         }
00698         pFanin = Aig_NotCond(pFanin, ((uPhase >> i) & 1) );
00699         s_DarLib->pDatas[i].pFunc = pFanin;
00700         s_DarLib->pDatas[i].Level = Aig_Regular(pFanin)->Level;
00701     }
00702     p->nCutsGood++;
00703     return 1;
00704 }

void Dar_LibDumpPriorities (  ) 

Function*************************************************************

Synopsis [Prints out the priorities into the file.]

Description []

SideEffects []

SeeAlso []

Definition at line 641 of file darLib.c.

00642 {
00643     int i, k, Out, Out2, Counter = 0, Printed = 0;
00644     printf( "\nOutput priorities (total = %d):\n", s_DarLib->nSubgrTotal );
00645     for ( i = 0; i < 222; i++ )
00646     {
00647 //        printf( "Class%d: ", i );
00648         for ( k = 0; k < s_DarLib->nSubgr[i]; k++ )
00649         {
00650             Out = s_DarLib->pPrios[i][k];
00651             Out2 = k == 0 ? Out : s_DarLib->pPrios[i][k-1];
00652             assert( s_DarLib->pScore[i][Out2] >= s_DarLib->pScore[i][Out] );
00653 //            printf( "%d(%d), ", Out, s_DarLib->pScore[i][Out] );
00654             printf( "%d, ", Out );
00655             Printed++;
00656             if ( ++Counter == 15 )
00657             {
00658                 printf( "\n" );
00659                 Counter = 0;
00660             }
00661         }
00662     }
00663     printf( "\n" );
00664     assert( Printed == s_DarLib->nSubgrTotal );
00665 }

void Dar_LibEval ( Dar_Man_t *  p,
Aig_Obj_t *  pRoot,
Dar_Cut_t *  pCut,
int  Required 
)

Function*************************************************************

Synopsis [Evaluates one cut.]

Description [Returns the best gain.]

SideEffects []

SeeAlso []

Definition at line 859 of file darLib.c.

00860 {
00861     int fTraining = 0;
00862     Dar_LibObj_t * pObj;
00863     int Out, k, Class, nNodesSaved, nNodesAdded, nNodesGained, clk;
00864     clk = clock();
00865     if ( pCut->nLeaves != 4 )
00866         return;
00867     // check if the cut exits and assigns leaves and their levels
00868     if ( !Dar_LibCutMatch(p, pCut) )
00869         return;
00870     // mark MFFC of the node
00871     nNodesSaved = Dar_LibCutMarkMffc( p->pAig, pRoot, pCut->nLeaves );
00872     // evaluate the cut
00873     Class = s_DarLib->pMap[pCut->uTruth];
00874     Dar_LibEvalAssignNums( p, Class );
00875     // profile outputs by their savings
00876     p->nTotalSubgs += s_DarLib->nSubgr0[Class];
00877     p->ClassSubgs[Class] += s_DarLib->nSubgr0[Class];
00878     for ( Out = 0; Out < s_DarLib->nSubgr0[Class]; Out++ )
00879     {
00880         pObj = Dar_LibObj(s_DarLib, s_DarLib->pSubgr0[Class][Out]);
00881         if ( Aig_Regular(s_DarLib->pDatas[pObj->Num].pFunc) == pRoot )
00882             continue;
00883         nNodesAdded = Dar_LibEval_rec( pObj, Out, nNodesSaved - !p->pPars->fUseZeros, Required );
00884         nNodesGained = nNodesSaved - nNodesAdded;
00885         if ( fTraining && nNodesGained >= 0 )
00886             Dar_LibIncrementScore( Class, Out, nNodesGained + 1 );
00887         if ( nNodesGained < 0 || (nNodesGained == 0 && !p->pPars->fUseZeros) )
00888             continue;
00889         if ( nNodesGained <  p->GainBest || 
00890             (nNodesGained == p->GainBest && s_DarLib->pDatas[pObj->Num].Level >= p->LevelBest) )
00891             continue;
00892         // remember this possibility
00893         Vec_PtrClear( p->vLeavesBest );
00894         for ( k = 0; k < (int)pCut->nLeaves; k++ )
00895             Vec_PtrPush( p->vLeavesBest, s_DarLib->pDatas[k].pFunc );
00896         p->OutBest    = s_DarLib->pSubgr0[Class][Out];
00897         p->OutNumBest = Out;
00898         p->LevelBest  = s_DarLib->pDatas[pObj->Num].Level;
00899         p->GainBest   = nNodesGained;
00900         p->ClassBest  = Class;
00901         assert( p->LevelBest <= Required );
00902     }
00903 clk = clock() - clk;
00904 p->ClassTimes[Class] += clk;
00905 p->timeEval += clk;
00906 }

int Dar_LibEval_rec ( Dar_LibObj_t *  pObj,
int  Out,
int  nNodesSaved,
int  Required 
)

Function*************************************************************

Synopsis [Evaluates one cut.]

Description [Returns the best gain.]

SideEffects []

SeeAlso []

Definition at line 822 of file darLib.c.

00823 {
00824     Dar_LibDat_t * pData;
00825     int Area;
00826     if ( pObj->fTerm )
00827         return 0;
00828     assert( pObj->Num > 3 );
00829     pData = s_DarLib->pDatas + pObj->Num;
00830     if ( pData->Level > Required )
00831         return 0xff;
00832     if ( pData->pFunc && !pData->fMffc )
00833         return 0;
00834     if ( pData->TravId == Out )
00835         return 0;
00836     pData->TravId = Out;
00837     // this is a new node - get a bound on the area of its branches
00838     nNodesSaved--;
00839     Area = Dar_LibEval_rec( Dar_LibObj(s_DarLib, pObj->Fan0), Out, nNodesSaved, Required+1 );
00840     if ( Area > nNodesSaved )
00841         return 0xff;
00842     Area += Dar_LibEval_rec( Dar_LibObj(s_DarLib, pObj->Fan1), Out, nNodesSaved, Required+1 );
00843     if ( Area > nNodesSaved )
00844         return 0xff;
00845     return Area + 1;
00846 }

void Dar_LibEvalAssignNums ( Dar_Man_t *  p,
int  Class 
)

Function*************************************************************

Synopsis [Assigns numbers to the nodes of one class.]

Description []

SideEffects []

SeeAlso []

Definition at line 773 of file darLib.c.

00774 {
00775     Dar_LibObj_t * pObj;
00776     Dar_LibDat_t * pData, * pData0, * pData1;
00777     Aig_Obj_t * pFanin0, * pFanin1;
00778     int i;
00779     for ( i = 0; i < s_DarLib->nNodes0[Class]; i++ )
00780     {
00781         // get one class node, assign its temporary number and set its data
00782         pObj = Dar_LibObj(s_DarLib, s_DarLib->pNodes0[Class][i]);
00783         pObj->Num = 4 + i;
00784         assert( (int)pObj->Num < s_DarLib->nNodes0Max + 4 );
00785         pData = s_DarLib->pDatas + pObj->Num;
00786         pData->fMffc = 0;
00787         pData->pFunc = NULL;
00788         pData->TravId = 0xFFFF;
00789 
00790         // explore the fanins
00791         assert( (int)Dar_LibObj(s_DarLib, pObj->Fan0)->Num < s_DarLib->nNodes0Max + 4 );
00792         assert( (int)Dar_LibObj(s_DarLib, pObj->Fan1)->Num < s_DarLib->nNodes0Max + 4 );
00793         pData0 = s_DarLib->pDatas + Dar_LibObj(s_DarLib, pObj->Fan0)->Num;
00794         pData1 = s_DarLib->pDatas + Dar_LibObj(s_DarLib, pObj->Fan1)->Num;
00795         pData->Level = 1 + AIG_MAX(pData0->Level, pData1->Level);
00796         if ( pData0->pFunc == NULL || pData1->pFunc == NULL )
00797             continue;
00798         pFanin0 = Aig_NotCond( pData0->pFunc, pObj->fCompl0 );
00799         pFanin1 = Aig_NotCond( pData1->pFunc, pObj->fCompl1 );
00800         pData->pFunc = Aig_TableLookupTwo( p->pAig, pFanin0, pFanin1 );
00801         if ( pData->pFunc )
00802         {
00803             // update the level to be more accurate
00804             pData->Level = Aig_Regular(pData->pFunc)->Level;
00805             // mark the node if it is part of MFFC
00806             pData->fMffc = Aig_ObjIsTravIdCurrent(p->pAig, pData->pFunc);
00807         }
00808     }
00809 }

void Dar_LibFree ( Dar_Lib_t *  p  ) 

Function*************************************************************

Synopsis [Frees the library.]

Description []

SideEffects []

SeeAlso []

Definition at line 156 of file darLib.c.

00157 {
00158     free( p->pObjs );
00159     free( p->pDatas );
00160     free( p->pNodesMem );
00161     free( p->pNodes0Mem );
00162     free( p->pSubgrMem );
00163     free( p->pSubgr0Mem );
00164     free( p->pPriosMem );
00165     FREE( p->pPlaceMem );
00166     FREE( p->pScoreMem );
00167     free( p->pPerms4 );
00168     free( p->puCanons );
00169     free( p->pPhases );
00170     free( p->pPerms );
00171     free( p->pMap );
00172     free( p );
00173 }

void Dar_LibIncrementScore ( int  Class,
int  Out,
int  Gain 
)

Function*************************************************************

Synopsis [Updates the score of the class and adjusts the priority of this class.]

Description []

SideEffects []

SeeAlso []

Definition at line 606 of file darLib.c.

00607 {
00608     int * pPrios = s_DarLib->pPrios[Class];  // pPrios[i] = Out
00609     int * pPlace = s_DarLib->pPlace[Class];  // pPlace[Out] = i
00610     int * pScore = s_DarLib->pScore[Class];  // score of Out
00611     int Out2;
00612     assert( Class >= 0 && Class < 222 );
00613     assert( Out >= 0 && Out < s_DarLib->nSubgr[Class] );
00614     assert( pPlace[pPrios[Out]] == Out );
00615     // increment the score
00616     pScore[Out] += Gain;
00617     // move the out in the order 
00618     while ( pPlace[Out] > 0 && pScore[Out] > pScore[ pPrios[pPlace[Out]-1] ] )
00619     {
00620         // get the previous output in the priority list
00621         Out2 = pPrios[pPlace[Out]-1];
00622         // swap Out and Out2
00623         pPlace[Out]--;
00624         pPlace[Out2]++;
00625         pPrios[pPlace[Out]] = Out;
00626         pPrios[pPlace[Out2]] = Out2;
00627     }
00628 }

static Dar_LibObj_t* Dar_LibObj ( Dar_Lib_t *  p,
int  Id 
) [inline, static]

Definition at line 102 of file darLib.c.

00102 { return p->pObjs + Id; }

void Dar_LibObjPrint_rec ( Dar_LibObj_t *  pObj  ) 

Function*************************************************************

Synopsis [Evaluates one cut.]

Description [Returns the best gain.]

SideEffects []

SeeAlso []

Definition at line 744 of file darLib.c.

00745 {
00746     if ( pObj->fTerm )
00747     {
00748         printf( "%c", 'a' + (int)(pObj - s_DarLib->pObjs) );
00749         return;
00750     }
00751     printf( "(" );
00752     Dar_LibObjPrint_rec( Dar_LibObj(s_DarLib, pObj->Fan0) );
00753     if ( pObj->fCompl0 )
00754         printf( "\'" );
00755     Dar_LibObjPrint_rec( Dar_LibObj(s_DarLib, pObj->Fan1) );
00756     if ( pObj->fCompl0 )
00757         printf( "\'" );
00758     printf( ")" );
00759 }

static int Dar_LibObjTruth ( Dar_LibObj_t *  pObj  )  [inline, static]

Definition at line 103 of file darLib.c.

00103 { return pObj->Num < (0xFFFF & ~pObj->Num) ? pObj->Num : (0xFFFF & ~pObj->Num); }

void Dar_LibPrepare ( int  nSubgraphs  ) 

Function*************************************************************

Synopsis [Starts the library.]

Description []

SideEffects []

SeeAlso []

Definition at line 453 of file darLib.c.

00454 {
00455     Dar_Lib_t * p = s_DarLib;
00456     int i, k, nNodes0Total;
00457     if ( p->nSubgraphs == nSubgraphs )
00458         return;
00459 
00460     // favor special classes:
00461     //  1 : F = (!d*!c*!b*!a)
00462     //  4 : F = (!d*!c*!(b*a))
00463     // 12 : F = (!d*!(c*!(!b*!a)))
00464     // 20 : F = (!d*!(c*b*a))
00465 
00466     // set the subgraph counters 
00467     p->nSubgr0Total = 0;
00468     for ( i = 0; i < 222; i++ )
00469     {
00470 //        if ( i == 1 || i == 4 || i == 12 || i == 20 ) // special classes 
00471         if ( i == 1 ) // special classes 
00472             p->nSubgr0[i] = p->nSubgr[i];
00473         else
00474             p->nSubgr0[i] = AIG_MIN( p->nSubgr[i], nSubgraphs );
00475         p->nSubgr0Total += p->nSubgr0[i];
00476         for ( k = 0; k < p->nSubgr0[i]; k++ )
00477             p->pSubgr0[i][k] = p->pSubgr[i][ p->pPrios[i][k] ];
00478     }
00479 
00480     // count the number of nodes
00481     // clean node counters
00482     for ( i = 0; i < 222; i++ )
00483         p->nNodes0[i] = 0;
00484     // create traversal IDs
00485     for ( i = 0; i < p->iObj; i++ )
00486         Dar_LibObj(p, i)->Num = 0xff;
00487     // count nodes in each class
00488     // count the total number of nodes and the largest class
00489     p->nNodes0Total = 0;
00490     p->nNodes0Max = 0;
00491     for ( i = 0; i < 222; i++ )
00492     {
00493         for ( k = 0; k < p->nSubgr0[i]; k++ )
00494             Dar_LibSetup0_rec( p, Dar_LibObj(p, p->pSubgr0[i][k]), i, 0 );
00495         p->nNodes0Total += p->nNodes0[i];
00496         p->nNodes0Max = AIG_MAX( p->nNodes0Max, p->nNodes0[i] );
00497     }
00498 
00499     // clean node counters
00500     for ( i = 0; i < 222; i++ )
00501         p->nNodes0[i] = 0;
00502     // create traversal IDs
00503     for ( i = 0; i < p->iObj; i++ )
00504         Dar_LibObj(p, i)->Num = 0xff;
00505     // add the nodes to storage
00506     nNodes0Total = 0;
00507     for ( i = 0; i < 222; i++ )
00508     {
00509         for ( k = 0; k < p->nSubgr0[i]; k++ )
00510             Dar_LibSetup0_rec( p, Dar_LibObj(p, p->pSubgr0[i][k]), i, 1 );
00511          nNodes0Total += p->nNodes0[i];
00512     }
00513     assert( nNodes0Total == p->nNodes0Total );
00514      // prepare the number of the PI nodes
00515     for ( i = 0; i < 4; i++ )
00516         Dar_LibObj(p, i)->Num = i;
00517 
00518     // realloc the datas
00519     Dar_LibCreateData( p, p->nNodes0Max + 32 ); 
00520     // allocated more because Dar_LibBuildBest() sometimes requires more entries
00521 }

Dar_Lib_t* Dar_LibRead (  ) 

Function*************************************************************

Synopsis [Reads library from array.]

Description []

SideEffects []

SeeAlso []

Definition at line 534 of file darLib.c.

00535 {
00536     Vec_Int_t * vObjs, * vOuts, * vPrios;
00537     Dar_Lib_t * p;
00538     int i;
00539     // read nodes and outputs
00540     vObjs  = Dar_LibReadNodes();
00541     vOuts  = Dar_LibReadOuts();
00542     vPrios = Dar_LibReadPrios();
00543     // create library
00544     p = Dar_LibAlloc( Vec_IntSize(vObjs)/2 + 4 );
00545     // create nodes
00546     for ( i = 0; i < vObjs->nSize; i += 2 )
00547         Dar_LibAddNode( p, vObjs->pArray[i] >> 1, vObjs->pArray[i+1] >> 1,
00548             vObjs->pArray[i] & 1, vObjs->pArray[i+1] & 1 );
00549     // create outputs
00550     Dar_LibSetup( p, vOuts, vPrios );
00551     Vec_IntFree( vObjs );
00552     Vec_IntFree( vOuts );
00553     Vec_IntFree( vPrios );
00554     return p;
00555 }

void Dar_LibReturnCanonicals ( unsigned *  pCanons  ) 

Function*************************************************************

Synopsis [Returns canonical truth tables.]

Description []

SideEffects []

SeeAlso []

Definition at line 186 of file darLib.c.

00187 {
00188     int Visits[222] = {0};
00189     int i, k;
00190     // find canonical truth tables
00191     for ( i = k = 0; i < (1<<16); i++ )
00192         if ( !Visits[s_DarLib->pMap[i]] )
00193         {
00194             Visits[s_DarLib->pMap[i]] = 1;
00195             pCanons[k++] = ((i<<16) | i);
00196         }
00197     assert( k == 222 );
00198 }

void Dar_LibSetup ( Dar_Lib_t *  p,
Vec_Int_t *  vOuts,
Vec_Int_t *  vPrios 
)

Function*************************************************************

Synopsis [Adds one AND to the library.]

Description []

SideEffects []

SeeAlso []

Definition at line 259 of file darLib.c.

00260 {
00261     int fTraining = 0;
00262     Dar_LibObj_t * pObj;
00263     int nNodesTotal, uTruth, Class, Out, i, k;
00264     assert( p->iObj == p->nObjs );
00265 
00266     // count the number of representatives of each class
00267     for ( i = 0; i < 222; i++ )
00268         p->nSubgr[i] = p->nNodes[i] = 0;
00269     Vec_IntForEachEntry( vOuts, Out, i )
00270     {
00271         pObj = Dar_LibObj( p, Out );
00272         uTruth = Dar_LibObjTruth( pObj );
00273         Class = p->pMap[uTruth];
00274         p->nSubgr[Class]++;
00275     }
00276     // allocate memory for the roots of each class
00277     p->pSubgrMem = ALLOC( int, Vec_IntSize(vOuts) );
00278     p->pSubgr0Mem = ALLOC( int, Vec_IntSize(vOuts) );
00279     p->nSubgrTotal = 0;
00280     for ( i = 0; i < 222; i++ )
00281     {
00282         p->pSubgr[i] = p->pSubgrMem + p->nSubgrTotal;
00283         p->pSubgr0[i] = p->pSubgr0Mem + p->nSubgrTotal;
00284         p->nSubgrTotal += p->nSubgr[i];
00285         p->nSubgr[i] = 0;
00286     }
00287     assert( p->nSubgrTotal == Vec_IntSize(vOuts) );
00288     // add the outputs to storage
00289     Vec_IntForEachEntry( vOuts, Out, i )
00290     {
00291         pObj = Dar_LibObj( p, Out );
00292         uTruth = Dar_LibObjTruth( pObj );
00293         Class = p->pMap[uTruth];
00294         p->pSubgr[Class][ p->nSubgr[Class]++ ] = Out;
00295     }
00296 
00297     if ( fTraining )
00298     {
00299         // allocate memory for the priority of roots of each class
00300         p->pPriosMem = ALLOC( int, Vec_IntSize(vOuts) );
00301         p->nSubgrTotal = 0;
00302         for ( i = 0; i < 222; i++ )
00303         {
00304             p->pPrios[i] = p->pPriosMem + p->nSubgrTotal;
00305             p->nSubgrTotal += p->nSubgr[i];
00306             for ( k = 0; k < p->nSubgr[i]; k++ )
00307                 p->pPrios[i][k] = k;
00308 
00309         }
00310         assert( p->nSubgrTotal == Vec_IntSize(vOuts) );
00311 
00312         // allocate memory for the priority of roots of each class
00313         p->pPlaceMem = ALLOC( int, Vec_IntSize(vOuts) );
00314         p->nSubgrTotal = 0;
00315         for ( i = 0; i < 222; i++ )
00316         {
00317             p->pPlace[i] = p->pPlaceMem + p->nSubgrTotal;
00318             p->nSubgrTotal += p->nSubgr[i];
00319             for ( k = 0; k < p->nSubgr[i]; k++ )
00320                 p->pPlace[i][k] = k;
00321 
00322         }
00323         assert( p->nSubgrTotal == Vec_IntSize(vOuts) );
00324 
00325         // allocate memory for the priority of roots of each class
00326         p->pScoreMem = ALLOC( int, Vec_IntSize(vOuts) );
00327         p->nSubgrTotal = 0;
00328         for ( i = 0; i < 222; i++ )
00329         {
00330             p->pScore[i] = p->pScoreMem + p->nSubgrTotal;
00331             p->nSubgrTotal += p->nSubgr[i];
00332             for ( k = 0; k < p->nSubgr[i]; k++ )
00333                 p->pScore[i][k] = 0;
00334 
00335         }
00336         assert( p->nSubgrTotal == Vec_IntSize(vOuts) );
00337     }
00338     else
00339     {
00340         int Counter = 0;
00341         // allocate memory for the priority of roots of each class
00342         p->pPriosMem = ALLOC( int, Vec_IntSize(vOuts) );
00343         p->nSubgrTotal = 0;
00344         for ( i = 0; i < 222; i++ )
00345         {
00346             p->pPrios[i] = p->pPriosMem + p->nSubgrTotal;
00347             p->nSubgrTotal += p->nSubgr[i];
00348             for ( k = 0; k < p->nSubgr[i]; k++ )
00349                 p->pPrios[i][k] = Vec_IntEntry(vPrios, Counter++);
00350 
00351         }
00352         assert( p->nSubgrTotal == Vec_IntSize(vOuts) );
00353         assert( Counter == Vec_IntSize(vPrios) );
00354     }
00355 
00356     // create traversal IDs
00357     for ( i = 0; i < p->iObj; i++ )
00358         Dar_LibObj(p, i)->Num = 0xff;
00359     // count nodes in each class
00360     for ( i = 0; i < 222; i++ )
00361         for ( k = 0; k < p->nSubgr[i]; k++ )
00362             Dar_LibSetup_rec( p, Dar_LibObj(p, p->pSubgr[i][k]), i, 0 );
00363     // count the total number of nodes
00364     p->nNodesTotal = 0;
00365     for ( i = 0; i < 222; i++ )
00366         p->nNodesTotal += p->nNodes[i];
00367     // allocate memory for the nodes of each class
00368     p->pNodesMem = ALLOC( int, p->nNodesTotal );
00369     p->pNodes0Mem = ALLOC( int, p->nNodesTotal );
00370     p->nNodesTotal = 0;
00371     for ( i = 0; i < 222; i++ )
00372     {
00373         p->pNodes[i] = p->pNodesMem + p->nNodesTotal;
00374         p->pNodes0[i] = p->pNodes0Mem + p->nNodesTotal;
00375         p->nNodesTotal += p->nNodes[i];
00376         p->nNodes[i] = 0;
00377     }
00378     // create traversal IDs
00379     for ( i = 0; i < p->iObj; i++ )
00380         Dar_LibObj(p, i)->Num = 0xff;
00381     // add the nodes to storage
00382     nNodesTotal = 0;
00383     for ( i = 0; i < 222; i++ )
00384     {
00385          for ( k = 0; k < p->nSubgr[i]; k++ )
00386             Dar_LibSetup_rec( p, Dar_LibObj(p, p->pSubgr[i][k]), i, 1 );
00387          nNodesTotal += p->nNodes[i];
00388 //printf( "Class %3d : Subgraphs = %4d. Nodes = %5d.\n", i, p->nSubgr[i], p->nNodes[i] );
00389     }
00390     assert( nNodesTotal == p->nNodesTotal );
00391      // prepare the number of the PI nodes
00392     for ( i = 0; i < 4; i++ )
00393         Dar_LibObj(p, i)->Num = i;
00394 }

void Dar_LibSetup0_rec ( Dar_Lib_t *  p,
Dar_LibObj_t *  pObj,
int  Class,
int  fCollect 
)

Function*************************************************************

Synopsis [Adds one AND to the library.]

Description []

SideEffects []

SeeAlso []

Definition at line 429 of file darLib.c.

00430 {
00431     if ( pObj->fTerm || (int)pObj->Num == Class )
00432         return;
00433     pObj->Num = Class;
00434     Dar_LibSetup0_rec( p, Dar_LibObj(p, pObj->Fan0), Class, fCollect );
00435     Dar_LibSetup0_rec( p, Dar_LibObj(p, pObj->Fan1), Class, fCollect );
00436     if ( fCollect )
00437         p->pNodes0[Class][ p->nNodes0[Class]++ ] = pObj-p->pObjs;
00438     else
00439         p->nNodes0[Class]++;
00440 }

void Dar_LibSetup_rec ( Dar_Lib_t *  p,
Dar_LibObj_t *  pObj,
int  Class,
int  fCollect 
)

Function*************************************************************

Synopsis [Adds one AND to the library.]

Description []

SideEffects []

SeeAlso []

Definition at line 235 of file darLib.c.

00236 {
00237     if ( pObj->fTerm || (int)pObj->Num == Class )
00238         return;
00239     pObj->Num = Class;
00240     Dar_LibSetup_rec( p, Dar_LibObj(p, pObj->Fan0), Class, fCollect );
00241     Dar_LibSetup_rec( p, Dar_LibObj(p, pObj->Fan1), Class, fCollect );
00242     if ( fCollect )
00243         p->pNodes[Class][ p->nNodes[Class]++ ] = pObj-p->pObjs;
00244     else
00245         p->nNodes[Class]++;
00246 }

void Dar_LibStart (  ) 

Function*************************************************************

Synopsis [Starts the library.]

Description []

SideEffects []

SeeAlso []

Definition at line 568 of file darLib.c.

00569 {
00570 //    int clk = clock();
00571     assert( s_DarLib == NULL );
00572     s_DarLib = Dar_LibRead();
00573 //    printf( "The 4-input library started with %d nodes and %d subgraphs. ", s_DarLib->nObjs - 4, s_DarLib->nSubgrTotal );
00574 //    PRT( "Time", clock() - clk );
00575 }

void Dar_LibStop (  ) 

Function*************************************************************

Synopsis [Stops the library.]

Description []

SideEffects []

SeeAlso []

Definition at line 588 of file darLib.c.

00589 {
00590     assert( s_DarLib != NULL );
00591     Dar_LibFree( s_DarLib );
00592     s_DarLib = NULL;
00593 }

Variable Documentation

Dar_Lib_t* s_DarLib = NULL [static]

Definition at line 100 of file darLib.c.

Generated on Tue Jan 5 12:18:17 2010 for abc70930 by  doxygen 1.6.1