src/opt/lpk/lpkAbcDsd.c File Reference

#include "lpkInt.h"
Include dependency graph for lpkAbcDsd.c:

Go to the source code of this file.

Functions

int Lpk_FunComputeMinSuppSizeVar (Lpk_Fun_t *p, unsigned **ppTruths, int nTruths, unsigned **ppCofs, unsigned uNonDecSupp)
unsigned Lpk_ComputeBoundSets_rec (Kit_DsdNtk_t *p, int iLit, Vec_Int_t *vSets, int nSizeMax)
Vec_Int_t * Lpk_ComputeBoundSets (Kit_DsdNtk_t *p, int nSizeMax)
static void Lpk_PrintSetOne (int uSupport)
static void Lpk_PrintSets (Vec_Int_t *vSets)
Vec_Int_t * Lpk_MergeBoundSets (Vec_Int_t *vSets0, Vec_Int_t *vSets1, int nSizeMax)
void Lpk_FunCompareBoundSets (Lpk_Fun_t *p, Vec_Int_t *vBSets, int nCofDepth, unsigned uNonDecSupp, unsigned uLateArrSupp, Lpk_Res_t *pRes)
unsigned Lpk_DsdLateArriving (Lpk_Fun_t *p)
int Lpk_DsdAnalizeOne (Lpk_Fun_t *p, unsigned *ppTruths[5][16], Kit_DsdNtk_t *pNtks[], char pCofVars[], int nCofDepth, Lpk_Res_t *pRes)
Lpk_Res_t * Lpk_DsdAnalize (Lpk_Man_t *pMan, Lpk_Fun_t *p, int nShared)
Lpk_Fun_t * Lpk_DsdSplit (Lpk_Man_t *pMan, Lpk_Fun_t *p, char *pCofVars, int nCofVars, unsigned uBoundSet)

Function Documentation

Vec_Int_t* Lpk_ComputeBoundSets ( Kit_DsdNtk_t *  p,
int  nSizeMax 
)

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

Synopsis [Computes the set of subsets of decomposable variables.]

Description []

SideEffects []

SeeAlso []

Definition at line 155 of file lpkAbcDsd.c.

00156 {
00157     Vec_Int_t * vSets;
00158     unsigned uSupport, Entry;
00159     int Number, i;
00160     assert( p->nVars <= 16 );
00161     vSets = Vec_IntAlloc( 100 );
00162     Vec_IntPush( vSets, 0 );
00163     if ( Kit_DsdNtkRoot(p)->Type == KIT_DSD_CONST1 )
00164         return vSets;
00165     if ( Kit_DsdNtkRoot(p)->Type == KIT_DSD_VAR )
00166     {
00167         uSupport = ( 1 << Kit_DsdLit2Var(Kit_DsdNtkRoot(p)->pFans[0]) );
00168         if ( Kit_WordCountOnes(uSupport) <= nSizeMax )
00169             Vec_IntPush( vSets, uSupport );
00170         return vSets;
00171     }
00172     uSupport = Lpk_ComputeBoundSets_rec( p, p->Root, vSets, nSizeMax );
00173     assert( (uSupport & 0xFFFF0000) == 0 );
00174     // add the total support of the network
00175     if ( Kit_WordCountOnes(uSupport) <= nSizeMax )
00176         Vec_IntPush( vSets, uSupport );
00177     // set the remaining variables
00178     Vec_IntForEachEntry( vSets, Number, i )
00179     {
00180         Entry = Number;
00181         Vec_IntWriteEntry( vSets, i, Entry | ((uSupport & ~Entry) << 16) );
00182     }
00183     return vSets;
00184 }

unsigned Lpk_ComputeBoundSets_rec ( Kit_DsdNtk_t *  p,
int  iLit,
Vec_Int_t *  vSets,
int  nSizeMax 
)

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

Synopsis [Recursively computes decomposable subsets.]

Description []

SideEffects []

SeeAlso []

Definition at line 101 of file lpkAbcDsd.c.

00102 {
00103     unsigned i, iLitFanin, uSupport, uSuppCur;
00104     Kit_DsdObj_t * pObj;
00105     // consider the case of simple gate
00106     pObj = Kit_DsdNtkObj( p, Kit_DsdLit2Var(iLit) );
00107     if ( pObj == NULL )
00108         return (1 << Kit_DsdLit2Var(iLit));
00109     if ( pObj->Type == KIT_DSD_AND || pObj->Type == KIT_DSD_XOR )
00110     {
00111         unsigned uSupps[16], Limit, s;
00112         uSupport = 0;
00113         Kit_DsdObjForEachFanin( p, pObj, iLitFanin, i )
00114         {
00115             uSupps[i] = Lpk_ComputeBoundSets_rec( p, iLitFanin, vSets, nSizeMax );
00116             uSupport |= uSupps[i];
00117         }
00118         // create all subsets, except empty and full
00119         Limit = (1 << pObj->nFans) - 1;
00120         for ( s = 1; s < Limit; s++ )
00121         {
00122             uSuppCur = 0;
00123             for ( i = 0; i < pObj->nFans; i++ )
00124                 if ( s & (1 << i) )
00125                     uSuppCur |= uSupps[i];
00126             if ( Kit_WordCountOnes(uSuppCur) <= nSizeMax )
00127                 Vec_IntPush( vSets, uSuppCur );
00128         }
00129         return uSupport;
00130     }
00131     assert( pObj->Type == KIT_DSD_PRIME );
00132     // get the cumulative support of all fanins
00133     uSupport = 0;
00134     Kit_DsdObjForEachFanin( p, pObj, iLitFanin, i )
00135     {
00136         uSuppCur  = Lpk_ComputeBoundSets_rec( p, iLitFanin, vSets, nSizeMax );
00137         uSupport |= uSuppCur;
00138         if ( Kit_WordCountOnes(uSuppCur) <= nSizeMax )
00139             Vec_IntPush( vSets, uSuppCur );
00140     }
00141     return uSupport;
00142 }

Lpk_Res_t* Lpk_DsdAnalize ( Lpk_Man_t *  pMan,
Lpk_Fun_t *  p,
int  nShared 
)

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

Synopsis [Performs DSD-based decomposition of the function.]

Description []

SideEffects []

SeeAlso []

Definition at line 440 of file lpkAbcDsd.c.

00441 { 
00442     static Lpk_Res_t Res0, * pRes0 = &Res0;
00443     static Lpk_Res_t Res1, * pRes1 = &Res1;
00444     static Lpk_Res_t Res2, * pRes2 = &Res2;
00445     static Lpk_Res_t Res3, * pRes3 = &Res3;
00446     int fUseBackLooking = 1;
00447     Lpk_Res_t * pRes = NULL;
00448     Vec_Int_t * vBSets;
00449     Kit_DsdNtk_t * pNtks[8] = {NULL};
00450     char pCofVars[5];
00451     int i;
00452 
00453     assert( p->nLutK >= 3 );
00454     assert( nShared >= 0 && nShared <= 3 );
00455     assert( p->uSupp == Kit_BitMask(p->nVars) );
00456 
00457     // try decomposition without cofactoring
00458     pNtks[0] = Kit_DsdDecomposeExpand( Lpk_FunTruth( p, 0 ), p->nVars );
00459     if ( pMan->pPars->fVerbose )
00460         pMan->nBlocks[ Kit_DsdNonDsdSizeMax(pNtks[0]) ]++;
00461     vBSets = Lpk_ComputeBoundSets( pNtks[0], p->nLutK );
00462     Lpk_FunCompareBoundSets( p, vBSets, 0, 0xFFFF, Lpk_DsdLateArriving(p), pRes0 );
00463     Vec_IntFree( vBSets );
00464 
00465     // check the result
00466     if ( pRes0->nBSVars == (int)p->nLutK )
00467         { pRes = pRes0; goto finish; }
00468     if ( pRes0->nBSVars == (int)p->nLutK - 1 )
00469         { pRes = pRes0; goto finish; }
00470     if ( nShared == 0 )
00471         goto finish;
00472 
00473     // prepare storage
00474     Kit_TruthCopy( pMan->ppTruths[0][0], Lpk_FunTruth( p, 0 ), p->nVars );
00475 
00476     // cofactor 1 time
00477     if ( !Lpk_DsdAnalizeOne( p, pMan->ppTruths, pNtks, pCofVars, 1, pRes1 ) )
00478         goto finish;
00479     assert( pRes1->nBSVars <= (int)p->nLutK - 1 );
00480     if ( pRes1->nBSVars == (int)p->nLutK - 1 )
00481         { pRes = pRes1; goto finish; }
00482     if ( pRes0->nBSVars == (int)p->nLutK - 2 )
00483         { pRes = pRes0; goto finish; }
00484     if ( pRes1->nBSVars == (int)p->nLutK - 2 )
00485         { pRes = pRes1; goto finish; }
00486     if ( nShared == 1 )
00487         goto finish;
00488 
00489     // cofactor 2 times
00490     if ( p->nLutK >= 4 ) 
00491     {
00492         if ( !Lpk_DsdAnalizeOne( p, pMan->ppTruths, pNtks, pCofVars, 2, pRes2 ) )
00493             goto finish;
00494         assert( pRes2->nBSVars <= (int)p->nLutK - 2 );
00495         if ( pRes2->nBSVars == (int)p->nLutK - 2 )
00496             { pRes = pRes2; goto finish; }
00497         if ( fUseBackLooking )
00498         {
00499             if ( pRes0->nBSVars == (int)p->nLutK - 3 )
00500                 { pRes = pRes0; goto finish; }
00501             if ( pRes1->nBSVars == (int)p->nLutK - 3 )
00502                 { pRes = pRes1; goto finish; }
00503         }
00504         if ( pRes2->nBSVars == (int)p->nLutK - 3 )
00505             { pRes = pRes2; goto finish; }
00506         if ( nShared == 2 )
00507             goto finish;
00508         assert( nShared == 3 );
00509     }
00510 
00511     // cofactor 3 times
00512     if ( p->nLutK >= 5 ) 
00513     {
00514         if ( !Lpk_DsdAnalizeOne( p, pMan->ppTruths, pNtks, pCofVars, 3, pRes3 ) )
00515             goto finish;
00516         assert( pRes3->nBSVars <= (int)p->nLutK - 3 );
00517         if ( pRes3->nBSVars == (int)p->nLutK - 3 )
00518             { pRes = pRes3; goto finish; }
00519         if ( fUseBackLooking )
00520         {
00521             if ( pRes0->nBSVars == (int)p->nLutK - 4 )
00522                 { pRes = pRes0; goto finish; }
00523             if ( pRes1->nBSVars == (int)p->nLutK - 4 )
00524                 { pRes = pRes1; goto finish; }
00525             if ( pRes2->nBSVars == (int)p->nLutK - 4 )
00526                 { pRes = pRes2; goto finish; }
00527         }
00528         if ( pRes3->nBSVars == (int)p->nLutK - 4 )
00529             { pRes = pRes3; goto finish; }
00530     }
00531 
00532 finish:
00533     // free the networks
00534     for ( i = 0; i < (1<<nShared); i++ )
00535         if ( pNtks[i] )
00536             Kit_DsdNtkFree( pNtks[i] );
00537     // choose the best under these conditions
00538     return pRes;
00539 }

int Lpk_DsdAnalizeOne ( Lpk_Fun_t *  p,
unsigned *  ppTruths[5][16],
Kit_DsdNtk_t *  pNtks[],
char  pCofVars[],
int  nCofDepth,
Lpk_Res_t *  pRes 
)

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

Synopsis [Performs DSD-based decomposition of the function.]

Description []

SideEffects []

SeeAlso []

Definition at line 360 of file lpkAbcDsd.c.

00361 {
00362     int fVerbose = 0;
00363     Vec_Int_t * pvBSets[4][8];
00364     unsigned uNonDecSupp, uLateArrSupp;
00365     int i, k, nNonDecSize, nNonDecSizeMax;
00366     assert( nCofDepth >= 1 && nCofDepth <= 3 );
00367     assert( nCofDepth < (int)p->nLutK - 1 );
00368     assert( p->fSupports );
00369 
00370     // find the support of the largest non-DSD block
00371     nNonDecSizeMax = 0;
00372     uNonDecSupp = p->uSupp;
00373     for ( i = 0; i < (1<<(nCofDepth-1)); i++ )
00374     {
00375         nNonDecSize = Kit_DsdNonDsdSizeMax( pNtks[i] );
00376         if ( nNonDecSizeMax < nNonDecSize )
00377         {
00378             nNonDecSizeMax = nNonDecSize;
00379             uNonDecSupp = Kit_DsdNonDsdSupports( pNtks[i] );
00380         }
00381         else if ( nNonDecSizeMax == nNonDecSize )
00382             uNonDecSupp |= Kit_DsdNonDsdSupports( pNtks[i] );
00383     }
00384 
00385     // remove those variables that cannot be used because of delay constraints
00386     // if variables arrival time is more than p->DelayLim - 2, it cannot be used
00387     uLateArrSupp = Lpk_DsdLateArriving( p );
00388     if ( (uNonDecSupp & ~uLateArrSupp) == 0 )
00389     {
00390         memset( pRes, 0, sizeof(Lpk_Res_t) );
00391         return 0;
00392     }
00393 
00394     // find the next cofactoring variable
00395     pCofVars[nCofDepth-1] = Lpk_FunComputeMinSuppSizeVar( p, ppTruths[nCofDepth-1], 1<<(nCofDepth-1), ppTruths[nCofDepth], uNonDecSupp & ~uLateArrSupp );
00396 
00397     // derive decomposed networks
00398     for ( i = 0; i < (1<<nCofDepth); i++ )
00399     {
00400         if ( pNtks[i] )
00401             Kit_DsdNtkFree( pNtks[i] );
00402         pNtks[i] = Kit_DsdDecomposeExpand( ppTruths[nCofDepth][i], p->nVars );
00403 if ( fVerbose )
00404 Kit_DsdPrint( stdout, pNtks[i] );
00405         pvBSets[nCofDepth][i] = Lpk_ComputeBoundSets( pNtks[i], p->nLutK - nCofDepth ); // try restricting to those in uNonDecSupp!!!
00406     }
00407 
00408     // derive the set of feasible boundsets
00409     for ( i = nCofDepth - 1; i >= 0; i-- )
00410         for ( k = 0; k < (1<<i); k++ )
00411             pvBSets[i][k] = Lpk_MergeBoundSets( pvBSets[i+1][2*k+0], pvBSets[i+1][2*k+1], p->nLutK - nCofDepth );
00412     // compare bound-sets
00413     Lpk_FunCompareBoundSets( p, pvBSets[0][0], nCofDepth, uNonDecSupp, uLateArrSupp, pRes );
00414     // free the bound sets
00415     for ( i = nCofDepth; i >= 0; i-- )
00416         for ( k = 0; k < (1<<i); k++ )
00417             Vec_IntFree( pvBSets[i][k] );
00418  
00419     // copy the cofactoring variables
00420     if ( pRes->BSVars )
00421     {
00422         pRes->nCofVars = nCofDepth;
00423         for ( i = 0; i < nCofDepth; i++ )
00424             pRes->pCofVars[i] = pCofVars[i];
00425     }
00426     return 1;
00427 }

unsigned Lpk_DsdLateArriving ( Lpk_Fun_t *  p  ) 

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

Synopsis [Finds late arriving inputs, which cannot be in the bound set.]

Description []

SideEffects []

SeeAlso []

Definition at line 340 of file lpkAbcDsd.c.

00341 {
00342     unsigned i, uLateArrSupp = 0;
00343     Lpk_SuppForEachVar( p->uSupp, i )
00344         if ( p->pDelays[i] > (int)p->nDelayLim - 2 )
00345             uLateArrSupp |= (1 << i);  
00346     return uLateArrSupp;
00347 }

Lpk_Fun_t* Lpk_DsdSplit ( Lpk_Man_t *  pMan,
Lpk_Fun_t *  p,
char *  pCofVars,
int  nCofVars,
unsigned  uBoundSet 
)

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

Synopsis [Splits the function into two subfunctions using DSD.]

Description []

SideEffects []

SeeAlso []

Definition at line 552 of file lpkAbcDsd.c.

00553 {
00554     Lpk_Fun_t * pNew;
00555     Kit_DsdNtk_t * pNtkDec;
00556     int i, k, iVacVar, nCofs;
00557     // prepare storage
00558     Kit_TruthCopy( pMan->ppTruths[0][0], Lpk_FunTruth(p, 0), p->nVars );
00559     // get the vacuous variable
00560     iVacVar = Kit_WordFindFirstBit( uBoundSet );
00561     // compute the cofactors
00562     for ( i = 0; i < nCofVars; i++ )
00563         for ( k = 0; k < (1<<i); k++ )
00564         {
00565             Kit_TruthCofactor0New( pMan->ppTruths[i+1][2*k+0], pMan->ppTruths[i][k], p->nVars, pCofVars[i] );
00566             Kit_TruthCofactor1New( pMan->ppTruths[i+1][2*k+1], pMan->ppTruths[i][k], p->nVars, pCofVars[i] );
00567         }
00568     // decompose each cofactor w.r.t. the bound set
00569     nCofs = (1<<nCofVars);
00570     for ( k = 0; k < nCofs; k++ )
00571     {
00572         pNtkDec = Kit_DsdDecomposeExpand( pMan->ppTruths[nCofVars][k], p->nVars );
00573         Kit_DsdTruthPartialTwo( pMan->pDsdMan, pNtkDec, uBoundSet, iVacVar, pMan->ppTruths[nCofVars+1][k], pMan->ppTruths[nCofVars+1][nCofs+k] );
00574         Kit_DsdNtkFree( pNtkDec );
00575     }
00576     // compute the composition/decomposition functions (they will be in pMan->ppTruths[1][0]/pMan->ppTruths[1][1])
00577     for ( i = nCofVars; i >= 1; i-- )
00578         for ( k = 0; k < (1<<i); k++ )
00579             Kit_TruthMuxVar( pMan->ppTruths[i][k], pMan->ppTruths[i+1][2*k+0], pMan->ppTruths[i+1][2*k+1], p->nVars, pCofVars[i-1] );
00580 
00581     // derive the new component (decomposition function)
00582     pNew = Lpk_FunDup( p, pMan->ppTruths[1][1] );
00583     // update the old component (composition function)
00584     Kit_TruthCopy( Lpk_FunTruth(p, 0), pMan->ppTruths[1][0], p->nVars );
00585     p->uSupp = Kit_TruthSupport( Lpk_FunTruth(p, 0), p->nVars );
00586     p->pFanins[iVacVar] = pNew->Id;
00587     p->pDelays[iVacVar] = Lpk_SuppDelay( pNew->uSupp, pNew->pDelays );
00588     // support minimize both
00589     p->fSupports = 0;
00590     Lpk_FunSuppMinimize( p );
00591     Lpk_FunSuppMinimize( pNew );
00592     // update delay and area requirements
00593     pNew->nDelayLim = p->pDelays[iVacVar];
00594     pNew->nAreaLim = 1;
00595     p->nAreaLim = p->nAreaLim - 1;
00596     return pNew;
00597 }

void Lpk_FunCompareBoundSets ( Lpk_Fun_t *  p,
Vec_Int_t *  vBSets,
int  nCofDepth,
unsigned  uNonDecSupp,
unsigned  uLateArrSupp,
Lpk_Res_t *  pRes 
)

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

Synopsis [Performs DSD-based decomposition of the function.]

Description []

SideEffects []

SeeAlso []

Definition at line 269 of file lpkAbcDsd.c.

00270 {
00271     int fVerbose = 0;
00272     unsigned uBoundSet;
00273     int i, nVarsBS, nVarsRem, Delay, Area;
00274 
00275     // compare the resulting boundsets
00276     memset( pRes, 0, sizeof(Lpk_Res_t) );
00277     Vec_IntForEachEntry( vBSets, uBoundSet, i )
00278     {
00279         if ( (uBoundSet & 0xFFFF) == 0 ) // skip empty boundset
00280             continue;
00281         if ( (uBoundSet & uNonDecSupp) == 0 ) // skip those boundsets that are not in the domain of interest
00282             continue;
00283         if ( (uBoundSet & uLateArrSupp) ) // skip those boundsets that are late arriving
00284             continue;
00285 if ( fVerbose )
00286 Lpk_PrintSetOne( uBoundSet );
00287         assert( (uBoundSet & (uBoundSet >> 16)) == 0 );
00288         nVarsBS = Kit_WordCountOnes( uBoundSet & 0xFFFF );
00289         if ( nVarsBS == 1 )
00290             continue;
00291         assert( nVarsBS <= (int)p->nLutK - nCofDepth );
00292         nVarsRem = p->nVars - nVarsBS + 1;
00293         Area = 1 + Lpk_LutNumLuts( nVarsRem, p->nLutK );
00294         Delay = 1 + Lpk_SuppDelay( uBoundSet & 0xFFFF, p->pDelays );
00295 if ( fVerbose )
00296 printf( "area = %d limit = %d  delay = %d limit = %d\n", Area, (int)p->nAreaLim, Delay, (int)p->nDelayLim );
00297         if ( Area > (int)p->nAreaLim || Delay > (int)p->nDelayLim )
00298             continue;
00299         if ( pRes->BSVars == 0 || pRes->nSuppSizeL > nVarsRem || (pRes->nSuppSizeL == nVarsRem && pRes->DelayEst > Delay) )
00300         {
00301             pRes->nBSVars = nVarsBS;
00302             pRes->BSVars = (uBoundSet & 0xFFFF);
00303             pRes->nSuppSizeS = nVarsBS + nCofDepth;
00304             pRes->nSuppSizeL = nVarsRem;
00305             pRes->DelayEst = Delay;
00306             pRes->AreaEst = Area;
00307         }
00308     }
00309 if ( fVerbose )
00310 {
00311 if ( pRes->BSVars )
00312 {
00313 printf( "Found bound set " );
00314 Lpk_PrintSetOne( pRes->BSVars );
00315 printf( "\n" );
00316 }
00317 else
00318 printf( "Did not find boundsets.\n" );
00319 printf( "\n" );
00320 }
00321     if ( pRes->BSVars )
00322     {
00323         assert( pRes->DelayEst <= (int)p->nDelayLim );
00324         assert( pRes->AreaEst <= (int)p->nAreaLim );
00325     }
00326 }

int Lpk_FunComputeMinSuppSizeVar ( Lpk_Fun_t *  p,
unsigned **  ppTruths,
int  nTruths,
unsigned **  ppCofs,
unsigned  uNonDecSupp 
)

CFile****************************************************************

FileName [lpkAbcDsd.c]

SystemName [ABC: Logic synthesis and verification system.]

PackageName [Fast Boolean matching for LUT structures.]

Synopsis [LUT-decomposition based on recursive DSD.]

Author [Alan Mishchenko]

Affiliation [UC Berkeley]

Date [Ver. 1.0. Started - April 28, 2007.]

Revision [

Id
lpkAbcDsd.c,v 1.00 2007/04/28 00:00:00 alanmi Exp

] DECLARATIONS /// FUNCTION DEFINITIONS ///Function*************************************************************

Synopsis [Cofactors TTs w.r.t. all vars and finds the best var.]

Description [The best variable is the variable with the minimum sum total of the support sizes of all truth tables. This procedure computes and returns cofactors w.r.t. the best variable.]

SideEffects []

SeeAlso []

Definition at line 44 of file lpkAbcDsd.c.

00045 {
00046     int i, Var, VarBest, nSuppSize0, nSuppSize1, nSuppTotalMin, nSuppTotalCur, nSuppMaxMin, nSuppMaxCur;
00047     assert( nTruths > 0 );
00048     VarBest = -1;
00049     Lpk_SuppForEachVar( p->uSupp, Var )
00050     {
00051         if ( (uNonDecSupp & (1 << Var)) == 0 )
00052             continue;
00053         nSuppMaxCur = 0;
00054         nSuppTotalCur = 0;
00055         for ( i = 0; i < nTruths; i++ )
00056         {
00057             if ( nTruths == 1 )
00058             {
00059                 nSuppSize0 = Kit_WordCountOnes( p->puSupps[2*Var+0] );
00060                 nSuppSize1 = Kit_WordCountOnes( p->puSupps[2*Var+1] );
00061             }
00062             else
00063             {
00064                 Kit_TruthCofactor0New( ppCofs[2*i+0], ppTruths[i], p->nVars, Var );
00065                 Kit_TruthCofactor1New( ppCofs[2*i+1], ppTruths[i], p->nVars, Var );
00066                 nSuppSize0 = Kit_TruthSupportSize( ppCofs[2*i+0], p->nVars );
00067                 nSuppSize1 = Kit_TruthSupportSize( ppCofs[2*i+1], p->nVars );
00068             }        
00069             nSuppMaxCur = ABC_MAX( nSuppMaxCur, nSuppSize0 );
00070             nSuppMaxCur = ABC_MAX( nSuppMaxCur, nSuppSize1 );
00071             nSuppTotalCur += nSuppSize0 + nSuppSize1;
00072         }
00073         if ( VarBest == -1 || nSuppMaxMin > nSuppMaxCur ||
00074              (nSuppMaxMin == nSuppMaxCur && nSuppTotalMin > nSuppTotalCur) )
00075         {
00076             VarBest = Var;
00077             nSuppMaxMin = nSuppMaxCur;
00078             nSuppTotalMin = nSuppTotalCur;
00079         }
00080     }
00081     // recompute cofactors for the best var
00082     for ( i = 0; i < nTruths; i++ )
00083     {
00084         Kit_TruthCofactor0New( ppCofs[2*i+0], ppTruths[i], p->nVars, VarBest );
00085         Kit_TruthCofactor1New( ppCofs[2*i+1], ppTruths[i], p->nVars, VarBest );
00086     }
00087     return VarBest;
00088 }

Vec_Int_t* Lpk_MergeBoundSets ( Vec_Int_t *  vSets0,
Vec_Int_t *  vSets1,
int  nSizeMax 
)

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

Synopsis [Merges two bound sets.]

Description []

SideEffects []

SeeAlso []

Definition at line 240 of file lpkAbcDsd.c.

00241 {
00242     Vec_Int_t * vSets;
00243     int Entry0, Entry1, Entry;
00244     int i, k;
00245     vSets = Vec_IntAlloc( 100 );
00246     Vec_IntForEachEntry( vSets0, Entry0, i )
00247     Vec_IntForEachEntry( vSets1, Entry1, k )
00248     {
00249         Entry = Entry0 | Entry1;
00250         if ( (Entry & (Entry >> 16)) )
00251             continue;
00252         if ( Kit_WordCountOnes(Entry & 0xffff) <= nSizeMax )
00253             Vec_IntPush( vSets, Entry );
00254     }
00255     return vSets;
00256 }

static void Lpk_PrintSetOne ( int  uSupport  )  [static]

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

Synopsis [Prints the sets of subsets.]

Description []

SideEffects []

SeeAlso []

Definition at line 197 of file lpkAbcDsd.c.

00198 {
00199     unsigned k;
00200     for ( k = 0; k < 16; k++ )
00201         if ( uSupport & (1<<k) )
00202             printf( "%c", 'a'+k );
00203     printf( " " );
00204 }

static void Lpk_PrintSets ( Vec_Int_t *  vSets  )  [static]

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

Synopsis [Prints the sets of subsets.]

Description []

SideEffects []

SeeAlso []

Definition at line 216 of file lpkAbcDsd.c.

00217 {
00218     unsigned uSupport;
00219     int Number, i;
00220     printf( "Subsets(%d): ", Vec_IntSize(vSets) );
00221     Vec_IntForEachEntry( vSets, Number, i )
00222     {
00223         uSupport = Number;
00224         Lpk_PrintSetOne( uSupport );
00225     }
00226     printf( "\n" );
00227 }

Generated on Tue Jan 5 12:19:28 2010 for abc70930 by  doxygen 1.6.1