src/aig/kit/kitSop.c File Reference

#include "kit.h"
Include dependency graph for kitSop.c:

Go to the source code of this file.

Functions

void Kit_SopCreate (Kit_Sop_t *cResult, Vec_Int_t *vInput, int nVars, Vec_Int_t *vMemory)
void Kit_SopCreateInverse (Kit_Sop_t *cResult, Vec_Int_t *vInput, int nLits, Vec_Int_t *vMemory)
void Kit_SopDup (Kit_Sop_t *cResult, Kit_Sop_t *cSop, Vec_Int_t *vMemory)
void Kit_SopDivideByLiteralQuo (Kit_Sop_t *cSop, int iLit)
void Kit_SopDivideByCube (Kit_Sop_t *cSop, Kit_Sop_t *cDiv, Kit_Sop_t *vQuo, Kit_Sop_t *vRem, Vec_Int_t *vMemory)
void Kit_SopDivideInternal (Kit_Sop_t *cSop, Kit_Sop_t *cDiv, Kit_Sop_t *vQuo, Kit_Sop_t *vRem, Vec_Int_t *vMemory)
static unsigned Kit_SopCommonCube (Kit_Sop_t *cSop)
void Kit_SopMakeCubeFree (Kit_Sop_t *cSop)
int Kit_SopIsCubeFree (Kit_Sop_t *cSop)
void Kit_SopCommonCubeCover (Kit_Sop_t *cResult, Kit_Sop_t *cSop, Vec_Int_t *vMemory)
int Kit_SopAnyLiteral (Kit_Sop_t *cSop, int nLits)
int Kit_SopWorstLiteral (Kit_Sop_t *cSop, int nLits)
int Kit_SopBestLiteral (Kit_Sop_t *cSop, int nLits, unsigned uMask)
void Kit_SopDivisorZeroKernel_rec (Kit_Sop_t *cSop, int nLits)
int Kit_SopDivisor (Kit_Sop_t *cResult, Kit_Sop_t *cSop, int nLits, Vec_Int_t *vMemory)
void Kit_SopBestLiteralCover (Kit_Sop_t *cResult, Kit_Sop_t *cSop, unsigned uCube, int nLits, Vec_Int_t *vMemory)

Function Documentation

int Kit_SopAnyLiteral ( Kit_Sop_t *  cSop,
int  nLits 
)

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

Synopsis [Find any literal that occurs more than once.]

Description []

SideEffects []

SeeAlso []

Definition at line 365 of file kitSop.c.

00366 {
00367     unsigned uCube;
00368     int i, k, nLitsCur;
00369     // go through each literal
00370     for ( i = 0; i < nLits; i++ )
00371     {
00372         // go through all the cubes
00373         nLitsCur = 0;
00374         Kit_SopForEachCube( cSop, uCube, k )
00375             if ( Kit_CubeHasLit(uCube, i) )
00376                 nLitsCur++;
00377         if ( nLitsCur > 1 )
00378             return i;
00379     }
00380     return -1;
00381 }

int Kit_SopBestLiteral ( Kit_Sop_t *  cSop,
int  nLits,
unsigned  uMask 
)

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

Synopsis [Find the least often occurring literal.]

Description [Find the least often occurring literal among those that occur more than once.]

SideEffects []

SeeAlso []

Definition at line 449 of file kitSop.c.

00450 {
00451     unsigned uCube;
00452     int i, k, iMax, nLitsMax, nLitsCur;
00453     int fUseFirst = 1;
00454 
00455     // go through each literal
00456     iMax = -1;
00457     nLitsMax = -1;
00458     for ( i = 0; i < nLits; i++ )
00459     {
00460         if ( !Kit_CubeHasLit(uMask, i) )
00461             continue;
00462         // go through all the cubes
00463         nLitsCur = 0;
00464         Kit_SopForEachCube( cSop, uCube, k )
00465             if ( Kit_CubeHasLit(uCube, i) )
00466                 nLitsCur++;
00467         // skip the literal that does not occur or occurs once
00468         if ( nLitsCur < 2 )
00469             continue;
00470         // check if this is the best literal
00471         if ( fUseFirst )
00472         {
00473             if ( nLitsMax < nLitsCur )
00474             {
00475                 nLitsMax = nLitsCur;
00476                 iMax = i;
00477             }
00478         }
00479         else
00480         {
00481             if ( nLitsMax <= nLitsCur )
00482             {
00483                 nLitsMax = nLitsCur;
00484                 iMax = i;
00485             }
00486         }
00487     }
00488     if ( nLitsMax >= 0 )
00489         return iMax;
00490     return -1;
00491 }

void Kit_SopBestLiteralCover ( Kit_Sop_t *  cResult,
Kit_Sop_t *  cSop,
unsigned  uCube,
int  nLits,
Vec_Int_t *  vMemory 
)

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

Synopsis [Create the one-literal cover with the best literal from cSop.]

Description []

SideEffects []

SeeAlso []

Definition at line 555 of file kitSop.c.

00556 {
00557     int iLitBest;
00558     // get the best literal
00559     iLitBest = Kit_SopBestLiteral( cSop, nLits, uCube );
00560     // start the cover
00561     cResult->nCubes = 0;
00562     cResult->pCubes = Vec_IntFetch( vMemory, 1 );
00563     // set the cube
00564     Kit_SopPushCube( cResult, Kit_CubeSetLit(0, iLitBest) );
00565 }

static unsigned Kit_SopCommonCube ( Kit_Sop_t *  cSop  )  [inline, static]

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

Synopsis [Returns the common cube.]

Description []

SideEffects []

SeeAlso []

Definition at line 285 of file kitSop.c.

00286 {
00287     unsigned uMask, uCube;
00288     int i;
00289     uMask = ~(unsigned)0;
00290     Kit_SopForEachCube( cSop, uCube, i )
00291         uMask &= uCube;
00292     return uMask;
00293 }

void Kit_SopCommonCubeCover ( Kit_Sop_t *  cResult,
Kit_Sop_t *  cSop,
Vec_Int_t *  vMemory 
)

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

Synopsis [Creates SOP composes of the common cube of the given SOP.]

Description []

SideEffects []

SeeAlso []

Definition at line 345 of file kitSop.c.

00346 {
00347     assert( Kit_SopCubeNum(cSop) > 0 );
00348     cResult->nCubes = 0;
00349     cResult->pCubes = Vec_IntFetch( vMemory, 1 );
00350     Kit_SopPushCube( cResult, Kit_SopCommonCube(cSop) );
00351 }

void Kit_SopCreate ( Kit_Sop_t *  cResult,
Vec_Int_t *  vInput,
int  nVars,
Vec_Int_t *  vMemory 
)

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

FileName [kitSop.c]

SystemName [ABC: Logic synthesis and verification system.]

PackageName [Computation kit.]

Synopsis [Procedures involving SOPs.]

Author [Alan Mishchenko]

Affiliation [UC Berkeley]

Date [Ver. 1.0. Started - Dec 6, 2006.]

Revision [

Id
kitSop.c,v 1.00 2006/12/06 00:00:00 alanmi Exp

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

Synopsis [Creates SOP from the cube array.]

Description []

SideEffects []

SeeAlso []

Definition at line 42 of file kitSop.c.

00043 {
00044     unsigned uCube;
00045     int i;
00046     // start the cover
00047     cResult->nCubes = 0;
00048     cResult->pCubes = Vec_IntFetch( vMemory, Vec_IntSize(vInput) );
00049     // add the cubes
00050     Vec_IntForEachEntry( vInput, uCube, i )
00051         Kit_SopPushCube( cResult, uCube );
00052 }

void Kit_SopCreateInverse ( Kit_Sop_t *  cResult,
Vec_Int_t *  vInput,
int  nLits,
Vec_Int_t *  vMemory 
)

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

Synopsis [Creates SOP from the cube array.]

Description []

SideEffects []

SeeAlso []

Definition at line 65 of file kitSop.c.

00066 {
00067     unsigned uCube, uMask = 0;
00068     int i, nCubes = Vec_IntSize(vInput);
00069     // start the cover
00070     cResult->nCubes = 0;
00071     cResult->pCubes = Vec_IntFetch( vMemory, nCubes );
00072     // add the cubes
00073 //    Vec_IntForEachEntry( vInput, uCube, i )
00074     for ( i = 0; i < nCubes; i++ )
00075     {
00076         uCube = Vec_IntEntry( vInput, i );
00077         uMask = ((uCube | (uCube >> 1)) & 0x55555555);
00078         uMask |= (uMask << 1);
00079         Kit_SopPushCube( cResult, uCube ^ uMask );
00080     }
00081 }

void Kit_SopDivideByCube ( Kit_Sop_t *  cSop,
Kit_Sop_t *  cDiv,
Kit_Sop_t *  vQuo,
Kit_Sop_t *  vRem,
Vec_Int_t *  vMemory 
)

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

Synopsis [Divides cover by one cube.]

Description []

SideEffects []

SeeAlso []

Definition at line 142 of file kitSop.c.

00143 {
00144     unsigned uCube, uDiv;
00145     int i;
00146     // get the only cube
00147     assert( Kit_SopCubeNum(cDiv) == 1 );
00148     uDiv = Kit_SopCube(cDiv, 0);
00149     // allocate covers
00150     vQuo->nCubes = 0;
00151     vQuo->pCubes = Vec_IntFetch( vMemory, Kit_SopCubeNum(cSop) );
00152     vRem->nCubes = 0;
00153     vRem->pCubes = Vec_IntFetch( vMemory, Kit_SopCubeNum(cSop) );
00154     // sort the cubes
00155     Kit_SopForEachCube( cSop, uCube, i )
00156     {
00157         if ( Kit_CubeContains( uCube, uDiv ) )
00158             Kit_SopPushCube( vQuo, Kit_CubeSharp(uCube, uDiv) );
00159         else
00160             Kit_SopPushCube( vRem, uCube );
00161     }
00162 }

void Kit_SopDivideByLiteralQuo ( Kit_Sop_t *  cSop,
int  iLit 
)

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

Synopsis [Derives the quotient of division by literal.]

Description [Reduces the cover to be equal to the result of division of the given cover by the literal.]

SideEffects []

SeeAlso []

Definition at line 118 of file kitSop.c.

00119 {
00120     unsigned uCube;
00121     int i, k = 0;
00122     Kit_SopForEachCube( cSop, uCube, i )
00123     {
00124         if ( Kit_CubeHasLit(uCube, iLit) )
00125             Kit_SopWriteCube( cSop, Kit_CubeRemLit(uCube, iLit), k++ );
00126     }
00127     Kit_SopShrink( cSop, k );
00128 }

void Kit_SopDivideInternal ( Kit_Sop_t *  cSop,
Kit_Sop_t *  cDiv,
Kit_Sop_t *  vQuo,
Kit_Sop_t *  vRem,
Vec_Int_t *  vMemory 
)

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

Synopsis [Divides cover by one cube.]

Description []

SideEffects []

SeeAlso []

Definition at line 175 of file kitSop.c.

00176 {
00177     unsigned uCube, uDiv, uCube2, uDiv2, uQuo;
00178     int i, i2, k, k2, nCubesRem;
00179     assert( Kit_SopCubeNum(cSop) >= Kit_SopCubeNum(cDiv) );
00180     // consider special case
00181     if ( Kit_SopCubeNum(cDiv) == 1 )
00182     {
00183         Kit_SopDivideByCube( cSop, cDiv, vQuo, vRem, vMemory );
00184         return;
00185     }
00186     // allocate quotient
00187     vQuo->nCubes = 0;
00188     vQuo->pCubes = Vec_IntFetch( vMemory, Kit_SopCubeNum(cSop) / Kit_SopCubeNum(cDiv) );
00189     // for each cube of the cover
00190     // it either belongs to the quotient or to the remainder
00191     Kit_SopForEachCube( cSop, uCube, i )
00192     {
00193         // skip taken cubes
00194         if ( Kit_CubeIsMarked(uCube) )
00195             continue;
00196         // find a matching cube in the divisor
00197         uDiv = ~0;
00198         Kit_SopForEachCube( cDiv, uDiv, k )
00199             if ( Kit_CubeContains( uCube, uDiv ) )
00200                 break;
00201         // the cube is not found 
00202         if ( k == Kit_SopCubeNum(cDiv) )
00203             continue;
00204         // the quotient cube exists
00205         uQuo = Kit_CubeSharp( uCube, uDiv );
00206         // find corresponding cubes for other cubes of the divisor
00207         uDiv2 = ~0;
00208         Kit_SopForEachCube( cDiv, uDiv2, k2 )
00209         {
00210             if ( k2 == k )
00211                 continue;
00212             // find a matching cube
00213             Kit_SopForEachCube( cSop, uCube2, i2 )
00214             {
00215                 // skip taken cubes
00216                 if ( Kit_CubeIsMarked(uCube2) )
00217                     continue;
00218                 // check if the cube can be used
00219                 if ( Kit_CubeContains( uCube2, uDiv2 ) && uQuo == Kit_CubeSharp( uCube2, uDiv2 ) )
00220                     break;
00221             }
00222             // the case when the cube is not found
00223             if ( i2 == Kit_SopCubeNum(cSop) )
00224                 break;
00225         }
00226         // we did not find some cubes - continue looking at other cubes
00227         if ( k2 != Kit_SopCubeNum(cDiv) )
00228             continue;
00229         // we found all cubes - add the quotient cube
00230         Kit_SopPushCube( vQuo, uQuo );
00231 
00232         // mark the first cube
00233         Kit_SopWriteCube( cSop, Kit_CubeMark(uCube), i );
00234         // mark other cubes that have this quotient
00235         Kit_SopForEachCube( cDiv, uDiv2, k2 )
00236         {
00237             if ( k2 == k )
00238                 continue;
00239             // find a matching cube
00240             Kit_SopForEachCube( cSop, uCube2, i2 )
00241             {
00242                 // skip taken cubes
00243                 if ( Kit_CubeIsMarked(uCube2) )
00244                     continue;
00245                 // check if the cube can be used
00246                 if ( Kit_CubeContains( uCube2, uDiv2 ) && uQuo == Kit_CubeSharp( uCube2, uDiv2 ) )
00247                     break;
00248             }
00249             assert( i2 < Kit_SopCubeNum(cSop) );
00250             // the cube is found, mark it 
00251             // (later we will add all unmarked cubes to the remainder)
00252             Kit_SopWriteCube( cSop, Kit_CubeMark(uCube2), i2 );
00253         }
00254     }
00255     // determine the number of cubes in the remainder
00256     nCubesRem = Kit_SopCubeNum(cSop) - Kit_SopCubeNum(vQuo) * Kit_SopCubeNum(cDiv);
00257     // allocate remainder
00258     vRem->nCubes = 0;
00259     vRem->pCubes = Vec_IntFetch( vMemory, nCubesRem );
00260     // finally add the remaining unmarked cubes to the remainder 
00261     // and clean the marked cubes in the cover
00262     Kit_SopForEachCube( cSop, uCube, i )
00263     {
00264         if ( !Kit_CubeIsMarked(uCube) )
00265         {
00266             Kit_SopPushCube( vRem, uCube );
00267             continue;
00268         }
00269         Kit_SopWriteCube( cSop, Kit_CubeUnmark(uCube), i );
00270     }
00271     assert( nCubesRem == Kit_SopCubeNum(vRem) );
00272 }

int Kit_SopDivisor ( Kit_Sop_t *  cResult,
Kit_Sop_t *  cSop,
int  nLits,
Vec_Int_t *  vMemory 
)

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

Synopsis [Computes the quick divisor of the cover.]

Description [Returns 0, if there is no divisor other than trivial.]

SideEffects []

SeeAlso []

Definition at line 529 of file kitSop.c.

00530 {
00531     if ( Kit_SopCubeNum(cSop) <= 1 )
00532         return 0;
00533     if ( Kit_SopAnyLiteral( cSop, nLits ) == -1 )
00534         return 0;
00535     // duplicate the cover
00536     Kit_SopDup( cResult, cSop, vMemory );
00537     // perform the kerneling
00538     Kit_SopDivisorZeroKernel_rec( cResult, nLits );
00539     assert( Kit_SopCubeNum(cResult) > 0 );
00540     return 1;
00541 }

void Kit_SopDivisorZeroKernel_rec ( Kit_Sop_t *  cSop,
int  nLits 
)

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

Synopsis [Computes a level-zero kernel.]

Description [Modifies the cover to contain one level-zero kernel.]

SideEffects []

SeeAlso []

Definition at line 504 of file kitSop.c.

00505 {
00506     int iLit;
00507     // find any literal that occurs at least two times
00508     iLit = Kit_SopWorstLiteral( cSop, nLits );
00509     if ( iLit == -1 )
00510         return;
00511     // derive the cube-free quotient
00512     Kit_SopDivideByLiteralQuo( cSop, iLit ); // the same cover
00513     Kit_SopMakeCubeFree( cSop );             // the same cover
00514     // call recursively
00515     Kit_SopDivisorZeroKernel_rec( cSop, nLits );    // the same cover
00516 }

void Kit_SopDup ( Kit_Sop_t *  cResult,
Kit_Sop_t *  cSop,
Vec_Int_t *  vMemory 
)

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

Synopsis [Duplicates SOP.]

Description []

SideEffects []

SeeAlso []

Definition at line 94 of file kitSop.c.

00095 {
00096     unsigned uCube;
00097     int i;
00098     // start the cover
00099     cResult->nCubes = 0;
00100     cResult->pCubes = Vec_IntFetch( vMemory, Kit_SopCubeNum(cSop) );
00101     // add the cubes
00102     Kit_SopForEachCube( cSop, uCube, i )
00103         Kit_SopPushCube( cResult, uCube );
00104 }

int Kit_SopIsCubeFree ( Kit_Sop_t *  cSop  ) 

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

Synopsis [Checks if the cover is cube-free.]

Description []

SideEffects []

SeeAlso []

Definition at line 329 of file kitSop.c.

00330 {
00331     return Kit_SopCommonCube( cSop ) == 0;
00332 }

void Kit_SopMakeCubeFree ( Kit_Sop_t *  cSop  ) 

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

Synopsis [Makes the cover cube-free.]

Description []

SideEffects []

SeeAlso []

Definition at line 306 of file kitSop.c.

00307 {
00308     unsigned uMask, uCube;
00309     int i;
00310     uMask = Kit_SopCommonCube( cSop );
00311     if ( uMask == 0 )
00312         return;
00313     // remove the common cube
00314     Kit_SopForEachCube( cSop, uCube, i )
00315         Kit_SopWriteCube( cSop, Kit_CubeSharp(uCube, uMask), i );
00316 }

int Kit_SopWorstLiteral ( Kit_Sop_t *  cSop,
int  nLits 
)

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

Synopsis [Find the least often occurring literal.]

Description [Find the least often occurring literal among those that occur more than once.]

SideEffects []

SeeAlso []

Definition at line 395 of file kitSop.c.

00396 {
00397     unsigned uCube;
00398     int i, k, iMin, nLitsMin, nLitsCur;
00399     int fUseFirst = 1;
00400 
00401     // go through each literal
00402     iMin = -1;
00403     nLitsMin = 1000000;
00404     for ( i = 0; i < nLits; i++ )
00405     {
00406         // go through all the cubes
00407         nLitsCur = 0;
00408         Kit_SopForEachCube( cSop, uCube, k )
00409             if ( Kit_CubeHasLit(uCube, i) )
00410                 nLitsCur++;
00411         // skip the literal that does not occur or occurs once
00412         if ( nLitsCur < 2 )
00413             continue;
00414         // check if this is the best literal
00415         if ( fUseFirst )
00416         {
00417             if ( nLitsMin > nLitsCur )
00418             {
00419                 nLitsMin = nLitsCur;
00420                 iMin = i;
00421             }
00422         }
00423         else
00424         {
00425             if ( nLitsMin >= nLitsCur )
00426             {
00427                 nLitsMin = nLitsCur;
00428                 iMin = i;
00429             }
00430         }
00431     }
00432     if ( nLitsMin < 1000000 )
00433         return iMin;
00434     return -1;
00435 }

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