abc-master
 All Data Structures Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros
Functions
kitSop.c File Reference
#include "kit.h"

Go to the source code of this file.

Functions

ABC_NAMESPACE_IMPL_START void Kit_SopCreate (Kit_Sop_t *cResult, Vec_Int_t *vInput, int nVars, Vec_Int_t *vMemory)
 DECLARATIONS ///. More...
 
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 370 of file kitSop.c.

371 {
372  unsigned uCube;
373  int i, k, nLitsCur;
374  // go through each literal
375  for ( i = 0; i < nLits; i++ )
376  {
377  // go through all the cubes
378  nLitsCur = 0;
379  Kit_SopForEachCube( cSop, uCube, k )
380  if ( Kit_CubeHasLit(uCube, i) )
381  nLitsCur++;
382  if ( nLitsCur > 1 )
383  return i;
384  }
385  return -1;
386 }
Kit_CubeHasLit
static int Kit_CubeHasLit(unsigned uCube, int i)
Definition: kit.h:175
if
if(last==0)
Definition: sparse_int.h:34
Kit_SopForEachCube
#define Kit_SopForEachCube(cSop, uCube, i)
ITERATORS ///.
Definition: kit.h:497
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 454 of file kitSop.c.

455 {
456  unsigned uCube;
457  int i, k, iMax, nLitsMax, nLitsCur;
458  int fUseFirst = 1;
459 
460  // go through each literal
461  iMax = -1;
462  nLitsMax = -1;
463  for ( i = 0; i < nLits; i++ )
464  {
465  if ( !Kit_CubeHasLit(uMask, i) )
466  continue;
467  // go through all the cubes
468  nLitsCur = 0;
469  Kit_SopForEachCube( cSop, uCube, k )
470  if ( Kit_CubeHasLit(uCube, i) )
471  nLitsCur++;
472  // skip the literal that does not occur or occurs once
473  if ( nLitsCur < 2 )
474  continue;
475  // check if this is the best literal
476  if ( fUseFirst )
477  {
478  if ( nLitsMax < nLitsCur )
479  {
480  nLitsMax = nLitsCur;
481  iMax = i;
482  }
483  }
484  else
485  {
486  if ( nLitsMax <= nLitsCur )
487  {
488  nLitsMax = nLitsCur;
489  iMax = i;
490  }
491  }
492  }
493  if ( nLitsMax >= 0 )
494  return iMax;
495  return -1;
496 }
Kit_CubeHasLit
static int Kit_CubeHasLit(unsigned uCube, int i)
Definition: kit.h:175
if
if(last==0)
Definition: sparse_int.h:34
Kit_SopForEachCube
#define Kit_SopForEachCube(cSop, uCube, i)
ITERATORS ///.
Definition: kit.h:497
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 560 of file kitSop.c.

561 {
562  int iLitBest;
563  // get the best literal
564  iLitBest = Kit_SopBestLiteral( cSop, nLits, uCube );
565  // start the cover
566  cResult->nCubes = 0;
567  cResult->pCubes = Vec_IntFetch( vMemory, 1 );
568  // set the cube
569  Kit_SopPushCube( cResult, Kit_CubeSetLit(0, iLitBest) );
570 }
Kit_SopBestLiteral
int Kit_SopBestLiteral(Kit_Sop_t *cSop, int nLits, unsigned uMask)
Definition: kitSop.c:454
Vec_IntFetch
static unsigned * Vec_IntFetch(Vec_Int_t *p, int nWords)
Definition: vecInt.h:853
Kit_CubeSetLit
static unsigned Kit_CubeSetLit(unsigned uCube, int i)
Definition: kit.h:176
Kit_SopPushCube
static void Kit_SopPushCube(Kit_Sop_t *cSop, unsigned uCube)
Definition: kit.h:191
static unsigned Kit_SopCommonCube ( Kit_Sop_t *  cSop)
inlinestatic

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

Synopsis [Returns the common cube.]

Description []

SideEffects []

SeeAlso []

Definition at line 290 of file kitSop.c.

291 {
292  unsigned uMask, uCube;
293  int i;
294  uMask = ~(unsigned)0;
295  Kit_SopForEachCube( cSop, uCube, i )
296  uMask &= uCube;
297  return uMask;
298 }
Kit_SopForEachCube
#define Kit_SopForEachCube(cSop, uCube, i)
ITERATORS ///.
Definition: kit.h:497
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 350 of file kitSop.c.

351 {
352  assert( Kit_SopCubeNum(cSop) > 0 );
353  cResult->nCubes = 0;
354  cResult->pCubes = Vec_IntFetch( vMemory, 1 );
355  Kit_SopPushCube( cResult, Kit_SopCommonCube(cSop) );
356 }
Vec_IntFetch
static unsigned * Vec_IntFetch(Vec_Int_t *p, int nWords)
Definition: vecInt.h:853
Kit_SopCommonCube
static unsigned Kit_SopCommonCube(Kit_Sop_t *cSop)
Definition: kitSop.c:290
assert
#define assert(ex)
Definition: util_old.h:213
Kit_SopCubeNum
static int Kit_SopCubeNum(Kit_Sop_t *cSop)
Definition: kit.h:188
Kit_SopPushCube
static void Kit_SopPushCube(Kit_Sop_t *cSop, unsigned uCube)
Definition: kit.h:191
ABC_NAMESPACE_IMPL_START void Kit_SopCreate ( Kit_Sop_t *  cResult,
Vec_Int_t *  vInput,
int  nVars,
Vec_Int_t *  vMemory 
)

DECLARATIONS ///.

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

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

Synopsis [Creates SOP from the cube array.]

Description []

SideEffects []

SeeAlso []

Definition at line 45 of file kitSop.c.

46 {
47  unsigned uCube;
48  int i;
49  // start the cover
50  cResult->nCubes = 0;
51  cResult->pCubes = Vec_IntFetch( vMemory, Vec_IntSize(vInput) );
52  // add the cubes
53  Vec_IntForEachEntry( vInput, uCube, i )
54  Kit_SopPushCube( cResult, uCube );
55 }
Vec_IntFetch
static unsigned * Vec_IntFetch(Vec_Int_t *p, int nWords)
Definition: vecInt.h:853
Vec_IntSize
static int Vec_IntSize(Vec_Int_t *p)
Definition: bblif.c:252
Vec_IntForEachEntry
#define Vec_IntForEachEntry(vVec, Entry, i)
MACRO DEFINITIONS ///.
Definition: vecInt.h:54
Kit_SopPushCube
static void Kit_SopPushCube(Kit_Sop_t *cSop, unsigned uCube)
Definition: kit.h:191
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 68 of file kitSop.c.

69 {
70  unsigned uCube, uMask = 0;
71  int i, nCubes = Vec_IntSize(vInput);
72  // start the cover
73  cResult->nCubes = 0;
74  cResult->pCubes = Vec_IntFetch( vMemory, nCubes );
75  // add the cubes
76 // Vec_IntForEachEntry( vInput, uCube, i )
77  for ( i = 0; i < nCubes; i++ )
78  {
79  uCube = Vec_IntEntry( vInput, i );
80  uMask = ((uCube | (uCube >> 1)) & 0x55555555);
81  uMask |= (uMask << 1);
82  Kit_SopPushCube( cResult, uCube ^ uMask );
83  }
84 }
Vec_IntFetch
static unsigned * Vec_IntFetch(Vec_Int_t *p, int nWords)
Definition: vecInt.h:853
Vec_IntEntry
static int Vec_IntEntry(Vec_Int_t *p, int i)
Definition: bblif.c:268
Vec_IntSize
static int Vec_IntSize(Vec_Int_t *p)
Definition: bblif.c:252
Kit_SopPushCube
static void Kit_SopPushCube(Kit_Sop_t *cSop, unsigned uCube)
Definition: kit.h:191
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 145 of file kitSop.c.

146 {
147  unsigned uCube, uDiv;
148  int i;
149  // get the only cube
150  assert( Kit_SopCubeNum(cDiv) == 1 );
151  uDiv = Kit_SopCube(cDiv, 0);
152  // allocate covers
153  vQuo->nCubes = 0;
154  vQuo->pCubes = Vec_IntFetch( vMemory, Kit_SopCubeNum(cSop) );
155  vRem->nCubes = 0;
156  vRem->pCubes = Vec_IntFetch( vMemory, Kit_SopCubeNum(cSop) );
157  // sort the cubes
158  Kit_SopForEachCube( cSop, uCube, i )
159  {
160  if ( Kit_CubeContains( uCube, uDiv ) )
161  Kit_SopPushCube( vQuo, Kit_CubeSharp(uCube, uDiv) );
162  else
163  Kit_SopPushCube( vRem, uCube );
164  }
165 }
Kit_SopCube
static unsigned Kit_SopCube(Kit_Sop_t *cSop, int i)
Definition: kit.h:189
Kit_CubeContains
static int Kit_CubeContains(unsigned uLarge, unsigned uSmall)
Definition: kit.h:180
Kit_CubeSharp
static unsigned Kit_CubeSharp(unsigned uCube, unsigned uMask)
Definition: kit.h:181
Vec_IntFetch
static unsigned * Vec_IntFetch(Vec_Int_t *p, int nWords)
Definition: vecInt.h:853
Kit_SopForEachCube
#define Kit_SopForEachCube(cSop, uCube, i)
ITERATORS ///.
Definition: kit.h:497
assert
#define assert(ex)
Definition: util_old.h:213
Kit_SopCubeNum
static int Kit_SopCubeNum(Kit_Sop_t *cSop)
Definition: kit.h:188
Kit_SopPushCube
static void Kit_SopPushCube(Kit_Sop_t *cSop, unsigned uCube)
Definition: kit.h:191
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 121 of file kitSop.c.

122 {
123  unsigned uCube;
124  int i, k = 0;
125  Kit_SopForEachCube( cSop, uCube, i )
126  {
127  if ( Kit_CubeHasLit(uCube, iLit) )
128  Kit_SopWriteCube( cSop, Kit_CubeRemLit(uCube, iLit), k++ );
129  }
130  Kit_SopShrink( cSop, k );
131 }
Kit_CubeHasLit
static int Kit_CubeHasLit(unsigned uCube, int i)
Definition: kit.h:175
Kit_CubeRemLit
static unsigned Kit_CubeRemLit(unsigned uCube, int i)
Definition: kit.h:178
Kit_SopForEachCube
#define Kit_SopForEachCube(cSop, uCube, i)
ITERATORS ///.
Definition: kit.h:497
Kit_SopWriteCube
static void Kit_SopWriteCube(Kit_Sop_t *cSop, unsigned uCube, int i)
Definition: kit.h:192
Kit_SopShrink
static void Kit_SopShrink(Kit_Sop_t *cSop, int nCubesNew)
Definition: kit.h:190
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 178 of file kitSop.c.

179 {
180  unsigned uCube, uDiv;
181  unsigned uCube2 = 0; // Suppress "might be used uninitialized"
182  unsigned uDiv2, uQuo;
183  int i, i2, k, k2, nCubesRem;
184  assert( Kit_SopCubeNum(cSop) >= Kit_SopCubeNum(cDiv) );
185  // consider special case
186  if ( Kit_SopCubeNum(cDiv) == 1 )
187  {
188  Kit_SopDivideByCube( cSop, cDiv, vQuo, vRem, vMemory );
189  return;
190  }
191  // allocate quotient
192  vQuo->nCubes = 0;
193  vQuo->pCubes = Vec_IntFetch( vMemory, Kit_SopCubeNum(cSop) / Kit_SopCubeNum(cDiv) );
194  // for each cube of the cover
195  // it either belongs to the quotient or to the remainder
196  Kit_SopForEachCube( cSop, uCube, i )
197  {
198  // skip taken cubes
199  if ( Kit_CubeIsMarked(uCube) )
200  continue;
201  // find a matching cube in the divisor
202  uDiv = ~0;
203  Kit_SopForEachCube( cDiv, uDiv, k )
204  if ( Kit_CubeContains( uCube, uDiv ) )
205  break;
206  // the cube is not found
207  if ( k == Kit_SopCubeNum(cDiv) )
208  continue;
209  // the quotient cube exists
210  uQuo = Kit_CubeSharp( uCube, uDiv );
211  // find corresponding cubes for other cubes of the divisor
212  uDiv2 = ~0;
213  Kit_SopForEachCube( cDiv, uDiv2, k2 )
214  {
215  if ( k2 == k )
216  continue;
217  // find a matching cube
218  Kit_SopForEachCube( cSop, uCube2, i2 )
219  {
220  // skip taken cubes
221  if ( Kit_CubeIsMarked(uCube2) )
222  continue;
223  // check if the cube can be used
224  if ( Kit_CubeContains( uCube2, uDiv2 ) && uQuo == Kit_CubeSharp( uCube2, uDiv2 ) )
225  break;
226  }
227  // the case when the cube is not found
228  if ( i2 == Kit_SopCubeNum(cSop) )
229  break;
230  }
231  // we did not find some cubes - continue looking at other cubes
232  if ( k2 != Kit_SopCubeNum(cDiv) )
233  continue;
234  // we found all cubes - add the quotient cube
235  Kit_SopPushCube( vQuo, uQuo );
236 
237  // mark the first cube
238  Kit_SopWriteCube( cSop, Kit_CubeMark(uCube), i );
239  // mark other cubes that have this quotient
240  Kit_SopForEachCube( cDiv, uDiv2, k2 )
241  {
242  if ( k2 == k )
243  continue;
244  // find a matching cube
245  Kit_SopForEachCube( cSop, uCube2, i2 )
246  {
247  // skip taken cubes
248  if ( Kit_CubeIsMarked(uCube2) )
249  continue;
250  // check if the cube can be used
251  if ( Kit_CubeContains( uCube2, uDiv2 ) && uQuo == Kit_CubeSharp( uCube2, uDiv2 ) )
252  break;
253  }
254  assert( i2 < Kit_SopCubeNum(cSop) );
255  // the cube is found, mark it
256  // (later we will add all unmarked cubes to the remainder)
257  Kit_SopWriteCube( cSop, Kit_CubeMark(uCube2), i2 );
258  }
259  }
260  // determine the number of cubes in the remainder
261  nCubesRem = Kit_SopCubeNum(cSop) - Kit_SopCubeNum(vQuo) * Kit_SopCubeNum(cDiv);
262  // allocate remainder
263  vRem->nCubes = 0;
264  vRem->pCubes = Vec_IntFetch( vMemory, nCubesRem );
265  // finally add the remaining unmarked cubes to the remainder
266  // and clean the marked cubes in the cover
267  Kit_SopForEachCube( cSop, uCube, i )
268  {
269  if ( !Kit_CubeIsMarked(uCube) )
270  {
271  Kit_SopPushCube( vRem, uCube );
272  continue;
273  }
274  Kit_SopWriteCube( cSop, Kit_CubeUnmark(uCube), i );
275  }
276  assert( nCubesRem == Kit_SopCubeNum(vRem) );
277 }
Kit_CubeContains
static int Kit_CubeContains(unsigned uLarge, unsigned uSmall)
Definition: kit.h:180
Kit_CubeSharp
static unsigned Kit_CubeSharp(unsigned uCube, unsigned uMask)
Definition: kit.h:181
Kit_CubeIsMarked
static int Kit_CubeIsMarked(unsigned uCube)
Definition: kit.h:184
Vec_IntFetch
static unsigned * Vec_IntFetch(Vec_Int_t *p, int nWords)
Definition: vecInt.h:853
if
if(last==0)
Definition: sparse_int.h:34
Kit_CubeMark
static unsigned Kit_CubeMark(unsigned uCube)
Definition: kit.h:185
Kit_SopForEachCube
#define Kit_SopForEachCube(cSop, uCube, i)
ITERATORS ///.
Definition: kit.h:497
Kit_SopWriteCube
static void Kit_SopWriteCube(Kit_Sop_t *cSop, unsigned uCube, int i)
Definition: kit.h:192
Kit_SopDivideByCube
void Kit_SopDivideByCube(Kit_Sop_t *cSop, Kit_Sop_t *cDiv, Kit_Sop_t *vQuo, Kit_Sop_t *vRem, Vec_Int_t *vMemory)
Definition: kitSop.c:145
Kit_CubeUnmark
static unsigned Kit_CubeUnmark(unsigned uCube)
Definition: kit.h:186
assert
#define assert(ex)
Definition: util_old.h:213
Kit_SopCubeNum
static int Kit_SopCubeNum(Kit_Sop_t *cSop)
Definition: kit.h:188
Kit_SopPushCube
static void Kit_SopPushCube(Kit_Sop_t *cSop, unsigned uCube)
Definition: kit.h:191
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 534 of file kitSop.c.

535 {
536  if ( Kit_SopCubeNum(cSop) <= 1 )
537  return 0;
538  if ( Kit_SopAnyLiteral( cSop, nLits ) == -1 )
539  return 0;
540  // duplicate the cover
541  Kit_SopDup( cResult, cSop, vMemory );
542  // perform the kerneling
543  Kit_SopDivisorZeroKernel_rec( cResult, nLits );
544  assert( Kit_SopCubeNum(cResult) > 0 );
545  return 1;
546 }
Kit_SopDup
void Kit_SopDup(Kit_Sop_t *cResult, Kit_Sop_t *cSop, Vec_Int_t *vMemory)
Definition: kitSop.c:97
assert
#define assert(ex)
Definition: util_old.h:213
Kit_SopAnyLiteral
int Kit_SopAnyLiteral(Kit_Sop_t *cSop, int nLits)
Definition: kitSop.c:370
Kit_SopCubeNum
static int Kit_SopCubeNum(Kit_Sop_t *cSop)
Definition: kit.h:188
Kit_SopDivisorZeroKernel_rec
void Kit_SopDivisorZeroKernel_rec(Kit_Sop_t *cSop, int nLits)
Definition: kitSop.c:509
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 509 of file kitSop.c.

510 {
511  int iLit;
512  // find any literal that occurs at least two times
513  iLit = Kit_SopWorstLiteral( cSop, nLits );
514  if ( iLit == -1 )
515  return;
516  // derive the cube-free quotient
517  Kit_SopDivideByLiteralQuo( cSop, iLit ); // the same cover
518  Kit_SopMakeCubeFree( cSop ); // the same cover
519  // call recursively
520  Kit_SopDivisorZeroKernel_rec( cSop, nLits ); // the same cover
521 }
Kit_SopDivideByLiteralQuo
void Kit_SopDivideByLiteralQuo(Kit_Sop_t *cSop, int iLit)
Definition: kitSop.c:121
Kit_SopMakeCubeFree
void Kit_SopMakeCubeFree(Kit_Sop_t *cSop)
Definition: kitSop.c:311
Kit_SopWorstLiteral
int Kit_SopWorstLiteral(Kit_Sop_t *cSop, int nLits)
Definition: kitSop.c:400
Kit_SopDivisorZeroKernel_rec
void Kit_SopDivisorZeroKernel_rec(Kit_Sop_t *cSop, int nLits)
Definition: kitSop.c:509
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 97 of file kitSop.c.

98 {
99  unsigned uCube;
100  int i;
101  // start the cover
102  cResult->nCubes = 0;
103  cResult->pCubes = Vec_IntFetch( vMemory, Kit_SopCubeNum(cSop) );
104  // add the cubes
105  Kit_SopForEachCube( cSop, uCube, i )
106  Kit_SopPushCube( cResult, uCube );
107 }
Vec_IntFetch
static unsigned * Vec_IntFetch(Vec_Int_t *p, int nWords)
Definition: vecInt.h:853
Kit_SopForEachCube
#define Kit_SopForEachCube(cSop, uCube, i)
ITERATORS ///.
Definition: kit.h:497
Kit_SopCubeNum
static int Kit_SopCubeNum(Kit_Sop_t *cSop)
Definition: kit.h:188
Kit_SopPushCube
static void Kit_SopPushCube(Kit_Sop_t *cSop, unsigned uCube)
Definition: kit.h:191
int Kit_SopIsCubeFree ( Kit_Sop_t *  cSop)

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

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

Description []

SideEffects []

SeeAlso []

Definition at line 334 of file kitSop.c.

335 {
336  return Kit_SopCommonCube( cSop ) == 0;
337 }
Kit_SopCommonCube
static unsigned Kit_SopCommonCube(Kit_Sop_t *cSop)
Definition: kitSop.c:290
void Kit_SopMakeCubeFree ( Kit_Sop_t *  cSop)

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

Synopsis [Makes the cover cube-free.]

Description []

SideEffects []

SeeAlso []

Definition at line 311 of file kitSop.c.

312 {
313  unsigned uMask, uCube;
314  int i;
315  uMask = Kit_SopCommonCube( cSop );
316  if ( uMask == 0 )
317  return;
318  // remove the common cube
319  Kit_SopForEachCube( cSop, uCube, i )
320  Kit_SopWriteCube( cSop, Kit_CubeSharp(uCube, uMask), i );
321 }
Kit_CubeSharp
static unsigned Kit_CubeSharp(unsigned uCube, unsigned uMask)
Definition: kit.h:181
Kit_SopCommonCube
static unsigned Kit_SopCommonCube(Kit_Sop_t *cSop)
Definition: kitSop.c:290
Kit_SopForEachCube
#define Kit_SopForEachCube(cSop, uCube, i)
ITERATORS ///.
Definition: kit.h:497
Kit_SopWriteCube
static void Kit_SopWriteCube(Kit_Sop_t *cSop, unsigned uCube, int i)
Definition: kit.h:192
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 400 of file kitSop.c.

401 {
402  unsigned uCube;
403  int i, k, iMin, nLitsMin, nLitsCur;
404  int fUseFirst = 1;
405 
406  // go through each literal
407  iMin = -1;
408  nLitsMin = 1000000;
409  for ( i = 0; i < nLits; i++ )
410  {
411  // go through all the cubes
412  nLitsCur = 0;
413  Kit_SopForEachCube( cSop, uCube, k )
414  if ( Kit_CubeHasLit(uCube, i) )
415  nLitsCur++;
416  // skip the literal that does not occur or occurs once
417  if ( nLitsCur < 2 )
418  continue;
419  // check if this is the best literal
420  if ( fUseFirst )
421  {
422  if ( nLitsMin > nLitsCur )
423  {
424  nLitsMin = nLitsCur;
425  iMin = i;
426  }
427  }
428  else
429  {
430  if ( nLitsMin >= nLitsCur )
431  {
432  nLitsMin = nLitsCur;
433  iMin = i;
434  }
435  }
436  }
437  if ( nLitsMin < 1000000 )
438  return iMin;
439  return -1;
440 }
Kit_CubeHasLit
static int Kit_CubeHasLit(unsigned uCube, int i)
Definition: kit.h:175
if
if(last==0)
Definition: sparse_int.h:34
Kit_SopForEachCube
#define Kit_SopForEachCube(cSop, uCube, i)
ITERATORS ///.
Definition: kit.h:497