abc-master
 All Data Structures Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros
covInt.h
Go to the documentation of this file.
1 /**CFile****************************************************************
2 
3  FileName [covInt.h]
4 
5  SystemName [ABC: Logic synthesis and verification system.]
6 
7  PackageName [Mapping into network of SOPs/ESOPs.]
8 
9  Synopsis [Internal declarations.]
10 
11  Author [Alan Mishchenko]
12 
13  Affiliation [UC Berkeley]
14 
15  Date [Ver. 1.0. Started - June 20, 2005.]
16 
17  Revision [$Id: covInt.h,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
18 
19 ***********************************************************************/
20 
21 #ifndef ABC__map__cov__covInt_h
22 #define ABC__map__cov__covInt_h
23 
24 #include "base/abc/abc.h"
25 
26 
27 ABC_NAMESPACE_HEADER_START
28 
29 
30 ////////////////////////////////////////////////////////////////////////
31 /// DECLARATIONS ///
32 ////////////////////////////////////////////////////////////////////////
33 
34 typedef struct Min_Man_t_ Min_Man_t;
35 typedef struct Min_Cube_t_ Min_Cube_t;
36 
37 struct Min_Man_t_
38 {
39  int nVars; // the number of vars
40  int nWords; // the number of words
41  Extra_MmFixed_t * pMemMan; // memory manager for cubes
42  // temporary cubes
43  Min_Cube_t * pOne0; // tautology cube
44  Min_Cube_t * pOne1; // tautology cube
45  Min_Cube_t * pTriv0[2]; // trivial cube
46  Min_Cube_t * pTriv1[2]; // trivial cube
47  Min_Cube_t * pTemp; // cube for computing the distance
48  Min_Cube_t * pBubble; // cube used as a separator
49  // temporary storage for the new cover
50  int nCubes; // the number of cubes
51  Min_Cube_t ** ppStore; // storage for cubes by number of literals
52 };
53 
54 struct Min_Cube_t_
55 {
56  Min_Cube_t * pNext; // the pointer to the next cube in the cover
57  unsigned nVars : 10; // the number of variables
58  unsigned nWords : 12; // the number of machine words
59  unsigned nLits : 10; // the number of literals in the cube
60  unsigned uData[1]; // the bit-data for the cube
61 };
62 
63 
64 // iterators through the entries in the linked lists of cubes
65 #define Min_CoverForEachCube( pCover, pCube ) \
66  for ( pCube = pCover; \
67  pCube; \
68  pCube = pCube->pNext )
69 #define Min_CoverForEachCubeSafe( pCover, pCube, pCube2 ) \
70  for ( pCube = pCover, \
71  pCube2 = pCube? pCube->pNext: NULL; \
72  pCube; \
73  pCube = pCube2, \
74  pCube2 = pCube? pCube->pNext: NULL )
75 #define Min_CoverForEachCubePrev( pCover, pCube, ppPrev ) \
76  for ( pCube = pCover, \
77  ppPrev = &(pCover); \
78  pCube; \
79  ppPrev = &pCube->pNext, \
80  pCube = pCube->pNext )
81 
82 // macros to get hold of bits and values in the cubes
83 static inline int Min_CubeHasBit( Min_Cube_t * p, int i ) { return (p->uData[(i)>>5] & (1<<((i) & 31))) > 0; }
84 static inline void Min_CubeSetBit( Min_Cube_t * p, int i ) { p->uData[(i)>>5] |= (1<<((i) & 31)); }
85 static inline void Min_CubeXorBit( Min_Cube_t * p, int i ) { p->uData[(i)>>5] ^= (1<<((i) & 31)); }
86 static inline int Min_CubeGetVar( Min_Cube_t * p, int Var ) { return 3 & (p->uData[(2*Var)>>5] >> ((2*Var) & 31)); }
87 static inline void Min_CubeXorVar( Min_Cube_t * p, int Var, int Value ) { p->uData[(2*Var)>>5] ^= (Value<<((2*Var) & 31)); }
88 
89 /*=== covMinEsop.c ==========================================================*/
90 extern void Min_EsopMinimize( Min_Man_t * p );
91 extern void Min_EsopAddCube( Min_Man_t * p, Min_Cube_t * pCube );
92 /*=== covMinSop.c ==========================================================*/
93 extern void Min_SopMinimize( Min_Man_t * p );
94 extern void Min_SopAddCube( Min_Man_t * p, Min_Cube_t * pCube );
95 /*=== covMinMan.c ==========================================================*/
96 extern Min_Man_t * Min_ManAlloc( int nVars );
97 extern void Min_ManClean( Min_Man_t * p, int nSupp );
98 extern void Min_ManFree( Min_Man_t * p );
99 /*=== covMinUtil.c ==========================================================*/
100 extern void Min_CoverCreate( Vec_Str_t * vCover, Min_Cube_t * pCover, char Type );
101 extern void Min_CubeWrite( FILE * pFile, Min_Cube_t * pCube );
102 extern void Min_CoverWrite( FILE * pFile, Min_Cube_t * pCover );
103 extern void Min_CoverWriteStore( FILE * pFile, Min_Man_t * p );
104 extern void Min_CoverWriteFile( Min_Cube_t * pCover, char * pName, int fEsop );
105 extern void Min_CoverCheck( Min_Man_t * p );
106 extern int Min_CubeCheck( Min_Cube_t * pCube );
107 extern Min_Cube_t * Min_CoverCollect( Min_Man_t * p, int nSuppSize );
108 extern void Min_CoverExpand( Min_Man_t * p, Min_Cube_t * pCover );
109 extern int Min_CoverSuppVarNum( Min_Man_t * p, Min_Cube_t * pCover );
110 
111 ////////////////////////////////////////////////////////////////////////
112 /// FUNCTION DEFINITIONS ///
113 ////////////////////////////////////////////////////////////////////////
114 
115 /**Function*************************************************************
116 
117  Synopsis [Creates the cube.]
118 
119  Description []
120 
121  SideEffects []
122 
123  SeeAlso []
124 
125 ***********************************************************************/
126 static inline Min_Cube_t * Min_CubeAlloc( Min_Man_t * p )
127 {
128  Min_Cube_t * pCube;
129  pCube = (Min_Cube_t *)Extra_MmFixedEntryFetch( p->pMemMan );
130  pCube->pNext = NULL;
131  pCube->nVars = p->nVars;
132  pCube->nWords = p->nWords;
133  pCube->nLits = 0;
134  memset( pCube->uData, 0xff, sizeof(unsigned) * p->nWords );
135  return pCube;
136 }
137 
138 /**Function*************************************************************
139 
140  Synopsis [Creates the cube representing elementary var.]
141 
142  Description []
143 
144  SideEffects []
145 
146  SeeAlso []
147 
148 ***********************************************************************/
149 static inline Min_Cube_t * Min_CubeAllocVar( Min_Man_t * p, int iVar, int fCompl )
150 {
151  Min_Cube_t * pCube;
152  pCube = Min_CubeAlloc( p );
153  Min_CubeXorBit( pCube, iVar*2+fCompl );
154  pCube->nLits = 1;
155  return pCube;
156 }
157 
158 /**Function*************************************************************
159 
160  Synopsis [Creates the cube.]
161 
162  Description []
163 
164  SideEffects []
165 
166  SeeAlso []
167 
168 ***********************************************************************/
169 static inline Min_Cube_t * Min_CubeDup( Min_Man_t * p, Min_Cube_t * pCopy )
170 {
171  Min_Cube_t * pCube;
172  pCube = Min_CubeAlloc( p );
173  memcpy( pCube->uData, pCopy->uData, sizeof(unsigned) * p->nWords );
174  pCube->nLits = pCopy->nLits;
175  return pCube;
176 }
177 
178 /**Function*************************************************************
179 
180  Synopsis [Recycles the cube.]
181 
182  Description []
183 
184  SideEffects []
185 
186  SeeAlso []
187 
188 ***********************************************************************/
189 static inline void Min_CubeRecycle( Min_Man_t * p, Min_Cube_t * pCube )
190 {
191  Extra_MmFixedEntryRecycle( p->pMemMan, (char *)pCube );
192 }
193 
194 /**Function*************************************************************
195 
196  Synopsis [Recycles the cube cover.]
197 
198  Description []
199 
200  SideEffects []
201 
202  SeeAlso []
203 
204 ***********************************************************************/
205 static inline void Min_CoverRecycle( Min_Man_t * p, Min_Cube_t * pCover )
206 {
207  Min_Cube_t * pCube, * pCube2;
208  Min_CoverForEachCubeSafe( pCover, pCube, pCube2 )
209  Extra_MmFixedEntryRecycle( p->pMemMan, (char *)pCube );
210 }
211 
212 
213 /**Function*************************************************************
214 
215  Synopsis [Counts the number of cubes in the cover.]
216 
217  Description []
218 
219  SideEffects []
220 
221  SeeAlso []
222 
223 ***********************************************************************/
224 static inline int Min_CubeCountLits( Min_Cube_t * pCube )
225 {
226  unsigned uData;
227  int Count = 0, i, w;
228  for ( w = 0; w < (int)pCube->nWords; w++ )
229  {
230  uData = pCube->uData[w] ^ (pCube->uData[w] >> 1);
231  for ( i = 0; i < 32; i += 2 )
232  if ( uData & (1 << i) )
233  Count++;
234  }
235  return Count;
236 }
237 
238 /**Function*************************************************************
239 
240  Synopsis [Counts the number of cubes in the cover.]
241 
242  Description []
243 
244  SideEffects []
245 
246  SeeAlso []
247 
248 ***********************************************************************/
249 static inline void Min_CubeGetLits( Min_Cube_t * pCube, Vec_Int_t * vLits )
250 {
251  unsigned uData;
252  int i, w;
253  Vec_IntClear( vLits );
254  for ( w = 0; w < (int)pCube->nWords; w++ )
255  {
256  uData = pCube->uData[w] ^ (pCube->uData[w] >> 1);
257  for ( i = 0; i < 32; i += 2 )
258  if ( uData & (1 << i) )
259  Vec_IntPush( vLits, w*16 + i/2 );
260  }
261 }
262 
263 /**Function*************************************************************
264 
265  Synopsis [Counts the number of cubes in the cover.]
266 
267  Description []
268 
269  SideEffects []
270 
271  SeeAlso []
272 
273 ***********************************************************************/
274 static inline int Min_CoverCountCubes( Min_Cube_t * pCover )
275 {
276  Min_Cube_t * pCube;
277  int Count = 0;
278  Min_CoverForEachCube( pCover, pCube )
279  Count++;
280  return Count;
281 }
282 
283 
284 /**Function*************************************************************
285 
286  Synopsis [Checks if two cubes are disjoint.]
287 
288  Description []
289 
290  SideEffects []
291 
292  SeeAlso []
293 
294 ***********************************************************************/
295 static inline int Min_CubesDisjoint( Min_Cube_t * pCube0, Min_Cube_t * pCube1 )
296 {
297  unsigned uData;
298  int i;
299  assert( pCube0->nVars == pCube1->nVars );
300  for ( i = 0; i < (int)pCube0->nWords; i++ )
301  {
302  uData = pCube0->uData[i] & pCube1->uData[i];
303  uData = (uData | (uData >> 1)) & 0x55555555;
304  if ( uData != 0x55555555 )
305  return 1;
306  }
307  return 0;
308 }
309 
310 /**Function*************************************************************
311 
312  Synopsis [Collects the disjoint variables of the two cubes.]
313 
314  Description []
315 
316  SideEffects []
317 
318  SeeAlso []
319 
320 ***********************************************************************/
321 static inline void Min_CoverGetDisjVars( Min_Cube_t * pThis, Min_Cube_t * pCube, Vec_Int_t * vVars )
322 {
323  unsigned uData;
324  int i, w;
325  Vec_IntClear( vVars );
326  for ( w = 0; w < (int)pCube->nWords; w++ )
327  {
328  uData = pThis->uData[w] & (pThis->uData[w] >> 1) & 0x55555555;
329  uData &= (pCube->uData[w] ^ (pCube->uData[w] >> 1));
330  if ( uData == 0 )
331  continue;
332  for ( i = 0; i < 32; i += 2 )
333  if ( uData & (1 << i) )
334  Vec_IntPush( vVars, w*16 + i/2 );
335  }
336 }
337 
338 /**Function*************************************************************
339 
340  Synopsis [Checks if two cubes are disjoint.]
341 
342  Description []
343 
344  SideEffects []
345 
346  SeeAlso []
347 
348 ***********************************************************************/
349 static inline int Min_CubesDistOne( Min_Cube_t * pCube0, Min_Cube_t * pCube1, Min_Cube_t * pTemp )
350 {
351  unsigned uData;
352  int i, fFound = 0;
353  for ( i = 0; i < (int)pCube0->nWords; i++ )
354  {
355  uData = pCube0->uData[i] ^ pCube1->uData[i];
356  if ( uData == 0 )
357  {
358  if ( pTemp ) pTemp->uData[i] = 0;
359  continue;
360  }
361  if ( fFound )
362  return 0;
363  uData = (uData | (uData >> 1)) & 0x55555555;
364  if ( (uData & (uData-1)) > 0 ) // more than one 1
365  return 0;
366  if ( pTemp ) pTemp->uData[i] = uData | (uData << 1);
367  fFound = 1;
368  }
369  if ( fFound == 0 )
370  {
371  printf( "\n" );
372  Min_CubeWrite( stdout, pCube0 );
373  Min_CubeWrite( stdout, pCube1 );
374  printf( "Error: Min_CubesDistOne() looks at two equal cubes!\n" );
375  }
376  return 1;
377 }
378 
379 /**Function*************************************************************
380 
381  Synopsis [Checks if two cubes are disjoint.]
382 
383  Description []
384 
385  SideEffects []
386 
387  SeeAlso []
388 
389 ***********************************************************************/
390 static inline int Min_CubesDistTwo( Min_Cube_t * pCube0, Min_Cube_t * pCube1, int * pVar0, int * pVar1 )
391 {
392  unsigned uData;//, uData2;
393  int i, k, Var0 = -1, Var1 = -1;
394  for ( i = 0; i < (int)pCube0->nWords; i++ )
395  {
396  uData = pCube0->uData[i] ^ pCube1->uData[i];
397  if ( uData == 0 )
398  continue;
399  if ( Var0 >= 0 && Var1 >= 0 ) // more than two 1s
400  return 0;
401  uData = (uData | (uData >> 1)) & 0x55555555;
402  if ( (Var0 >= 0 || Var1 >= 0) && (uData & (uData-1)) > 0 )
403  return 0;
404  for ( k = 0; k < 32; k += 2 )
405  if ( uData & (1 << k) )
406  {
407  if ( Var0 == -1 )
408  Var0 = 16 * i + k/2;
409  else if ( Var1 == -1 )
410  Var1 = 16 * i + k/2;
411  else
412  return 0;
413  }
414  /*
415  if ( Var0 >= 0 )
416  {
417  uData &= 0xFFFF;
418  uData2 = (uData >> 16);
419  if ( uData && uData2 )
420  return 0;
421  if ( uData )
422  {
423  }
424  uData }= uData2;
425  uData &= 0x
426  }
427  */
428  }
429  if ( Var0 >= 0 && Var1 >= 0 )
430  {
431  *pVar0 = Var0;
432  *pVar1 = Var1;
433  return 1;
434  }
435  if ( Var0 == -1 || Var1 == -1 )
436  {
437  printf( "\n" );
438  Min_CubeWrite( stdout, pCube0 );
439  Min_CubeWrite( stdout, pCube1 );
440  printf( "Error: Min_CubesDistTwo() looks at two equal cubes or dist1 cubes!\n" );
441  }
442  return 0;
443 }
444 
445 /**Function*************************************************************
446 
447  Synopsis [Makes the produce of two cubes.]
448 
449  Description []
450 
451  SideEffects []
452 
453  SeeAlso []
454 
455 ***********************************************************************/
456 static inline Min_Cube_t * Min_CubesProduct( Min_Man_t * p, Min_Cube_t * pCube0, Min_Cube_t * pCube1 )
457 {
458  Min_Cube_t * pCube;
459  int i;
460  assert( pCube0->nVars == pCube1->nVars );
461  pCube = Min_CubeAlloc( p );
462  for ( i = 0; i < p->nWords; i++ )
463  pCube->uData[i] = pCube0->uData[i] & pCube1->uData[i];
464  pCube->nLits = Min_CubeCountLits( pCube );
465  return pCube;
466 }
467 
468 /**Function*************************************************************
469 
470  Synopsis [Makes the produce of two cubes.]
471 
472  Description []
473 
474  SideEffects []
475 
476  SeeAlso []
477 
478 ***********************************************************************/
479 static inline Min_Cube_t * Min_CubesXor( Min_Man_t * p, Min_Cube_t * pCube0, Min_Cube_t * pCube1 )
480 {
481  Min_Cube_t * pCube;
482  int i;
483  assert( pCube0->nVars == pCube1->nVars );
484  pCube = Min_CubeAlloc( p );
485  for ( i = 0; i < p->nWords; i++ )
486  pCube->uData[i] = pCube0->uData[i] ^ pCube1->uData[i];
487  pCube->nLits = Min_CubeCountLits( pCube );
488  return pCube;
489 }
490 
491 /**Function*************************************************************
492 
493  Synopsis [Makes the produce of two cubes.]
494 
495  Description []
496 
497  SideEffects []
498 
499  SeeAlso []
500 
501 ***********************************************************************/
502 static inline int Min_CubesAreEqual( Min_Cube_t * pCube0, Min_Cube_t * pCube1 )
503 {
504  int i;
505  for ( i = 0; i < (int)pCube0->nWords; i++ )
506  if ( pCube0->uData[i] != pCube1->uData[i] )
507  return 0;
508  return 1;
509 }
510 
511 /**Function*************************************************************
512 
513  Synopsis [Returns 1 if pCube1 is contained in pCube0, bitwise.]
514 
515  Description []
516 
517  SideEffects []
518 
519  SeeAlso []
520 
521 ***********************************************************************/
522 static inline int Min_CubeIsContained( Min_Cube_t * pCube0, Min_Cube_t * pCube1 )
523 {
524  int i;
525  for ( i = 0; i < (int)pCube0->nWords; i++ )
526  if ( (pCube0->uData[i] & pCube1->uData[i]) != pCube1->uData[i] )
527  return 0;
528  return 1;
529 }
530 
531 /**Function*************************************************************
532 
533  Synopsis [Transforms the cube into the result of merging.]
534 
535  Description []
536 
537  SideEffects []
538 
539  SeeAlso []
540 
541 ***********************************************************************/
542 static inline void Min_CubesTransform( Min_Cube_t * pCube, Min_Cube_t * pDist, Min_Cube_t * pMask )
543 {
544  int w;
545  for ( w = 0; w < (int)pCube->nWords; w++ )
546  {
547  pCube->uData[w] = pCube->uData[w] ^ pDist->uData[w];
548  pCube->uData[w] |= (pDist->uData[w] & ~pMask->uData[w]);
549  }
550 }
551 
552 /**Function*************************************************************
553 
554  Synopsis [Transforms the cube into the result of distance-1 merging.]
555 
556  Description []
557 
558  SideEffects []
559 
560  SeeAlso []
561 
562 ***********************************************************************/
563 static inline void Min_CubesTransformOr( Min_Cube_t * pCube, Min_Cube_t * pDist )
564 {
565  int w;
566  for ( w = 0; w < (int)pCube->nWords; w++ )
567  pCube->uData[w] |= pDist->uData[w];
568 }
569 
570 
571 
572 /**Function*************************************************************
573 
574  Synopsis [Sorts the cover in the increasing number of literals.]
575 
576  Description []
577 
578  SideEffects []
579 
580  SeeAlso []
581 
582 ***********************************************************************/
583 static inline void Min_CoverExpandRemoveEqual( Min_Man_t * p, Min_Cube_t * pCover )
584 {
585  Min_Cube_t * pCube, * pCube2, * pThis;
586  if ( pCover == NULL )
587  {
588  Min_ManClean( p, p->nVars );
589  return;
590  }
591  Min_ManClean( p, pCover->nVars );
592  Min_CoverForEachCubeSafe( pCover, pCube, pCube2 )
593  {
594  // go through the linked list
595  Min_CoverForEachCube( p->ppStore[pCube->nLits], pThis )
596  if ( Min_CubesAreEqual( pCube, pThis ) )
597  {
598  Min_CubeRecycle( p, pCube );
599  break;
600  }
601  if ( pThis != NULL )
602  continue;
603  pCube->pNext = p->ppStore[pCube->nLits];
604  p->ppStore[pCube->nLits] = pCube;
605  p->nCubes++;
606  }
607 }
608 
609 /**Function*************************************************************
610 
611  Synopsis [Returns 1 if the given cube is contained in one of the cubes of the cover.]
612 
613  Description []
614 
615  SideEffects []
616 
617  SeeAlso []
618 
619 ***********************************************************************/
620 static inline int Min_CoverContainsCube( Min_Man_t * p, Min_Cube_t * pCube )
621 {
622  Min_Cube_t * pThis;
623  int i;
624 /*
625  // this cube cannot be equal to any cube
626  Min_CoverForEachCube( p->ppStore[pCube->nLits], pThis )
627  {
628  if ( Min_CubesAreEqual( pCube, pThis ) )
629  {
630  Min_CubeWrite( stdout, pCube );
631  assert( 0 );
632  }
633  }
634 */
635  // try to find a containing cube
636  for ( i = 0; i <= (int)pCube->nLits; i++ )
637  Min_CoverForEachCube( p->ppStore[i], pThis )
638  {
639  // skip the bubble
640  if ( pThis != p->pBubble && Min_CubeIsContained( pThis, pCube ) )
641  return 1;
642  }
643  return 0;
644 }
645 
646 
647 ABC_NAMESPACE_HEADER_END
648 
649 #endif
650 
651 
652 ////////////////////////////////////////////////////////////////////////
653 /// END OF FILE ///
654 ////////////////////////////////////////////////////////////////////////
memset
char * memset()
Min_Cube_t_
Definition: covInt.h:54
Min_CoverCheck
void Min_CoverCheck(Min_Man_t *p)
Definition: covMinUtil.c:223
Min_CubeRecycle
static void Min_CubeRecycle(Min_Man_t *p, Min_Cube_t *pCube)
Definition: covInt.h:189
Min_Cube_t_::nVars
unsigned nVars
Definition: covInt.h:57
Min_CubeXorVar
static void Min_CubeXorVar(Min_Cube_t *p, int Var, int Value)
Definition: covInt.h:87
Min_CubeWrite
void Min_CubeWrite(FILE *pFile, Min_Cube_t *pCube)
Definition: covMinUtil.c:106
p
static Llb_Mgr_t * p
Definition: llb3Image.c:950
Vec_Int_t
typedefABC_NAMESPACE_IMPL_START struct Vec_Int_t_ Vec_Int_t
DECLARATIONS ///.
Definition: bblif.c:37
Min_CubeAllocVar
static Min_Cube_t * Min_CubeAllocVar(Min_Man_t *p, int iVar, int fCompl)
Definition: covInt.h:149
Min_Man_t_::pOne0
Min_Cube_t * pOne0
Definition: covInt.h:43
Min_CoverExpandRemoveEqual
static void Min_CoverExpandRemoveEqual(Min_Man_t *p, Min_Cube_t *pCover)
Definition: covInt.h:583
Min_CubeCountLits
static int Min_CubeCountLits(Min_Cube_t *pCube)
Definition: covInt.h:224
Min_Man_t_::pOne1
Min_Cube_t * pOne1
Definition: covInt.h:44
Min_CubeDup
static Min_Cube_t * Min_CubeDup(Min_Man_t *p, Min_Cube_t *pCopy)
Definition: covInt.h:169
Min_Cube_t_::pNext
Min_Cube_t * pNext
Definition: covInt.h:56
Min_CubesDisjoint
static int Min_CubesDisjoint(Min_Cube_t *pCube0, Min_Cube_t *pCube1)
Definition: covInt.h:295
Min_CoverWriteFile
void Min_CoverWriteFile(Min_Cube_t *pCover, char *pName, int fEsop)
Definition: covMinUtil.c:190
Min_CoverCreate
void Min_CoverCreate(Vec_Str_t *vCover, Min_Cube_t *pCover, char Type)
Definition: covMinUtil.c:85
memcpy
char * memcpy()
Min_CoverForEachCubeSafe
#define Min_CoverForEachCubeSafe(pCover, pCube, pCube2)
Definition: covInt.h:69
Min_ManAlloc
Min_Man_t * Min_ManAlloc(int nVars)
DECLARATIONS ///.
Definition: covMinMan.c:45
Extra_MmFixedEntryFetch
char * Extra_MmFixedEntryFetch(Extra_MmFixed_t *p)
Definition: extraUtilMemory.c:202
Min_CubesDistOne
static int Min_CubesDistOne(Min_Cube_t *pCube0, Min_Cube_t *pCube1, Min_Cube_t *pTemp)
Definition: covInt.h:349
Min_Man_t_::pTriv1
Min_Cube_t * pTriv1[2]
Definition: covInt.h:46
Min_CubesDistTwo
static int Min_CubesDistTwo(Min_Cube_t *pCube0, Min_Cube_t *pCube1, int *pVar0, int *pVar1)
Definition: covInt.h:390
Min_CubesProduct
static Min_Cube_t * Min_CubesProduct(Min_Man_t *p, Min_Cube_t *pCube0, Min_Cube_t *pCube1)
Definition: covInt.h:456
Min_Man_t_::pTemp
Min_Cube_t * pTemp
Definition: covInt.h:47
Min_Man_t_::ppStore
Min_Cube_t ** ppStore
Definition: covInt.h:51
Min_CubeIsContained
static int Min_CubeIsContained(Min_Cube_t *pCube0, Min_Cube_t *pCube1)
Definition: covInt.h:522
Min_CoverExpand
void Min_CoverExpand(Min_Man_t *p, Min_Cube_t *pCover)
Definition: covMinUtil.c:294
Min_CoverCollect
Min_Cube_t * Min_CoverCollect(Min_Man_t *p, int nSuppSize)
Definition: covMinUtil.c:264
Min_CoverGetDisjVars
static void Min_CoverGetDisjVars(Min_Cube_t *pThis, Min_Cube_t *pCube, Vec_Int_t *vVars)
Definition: covInt.h:321
Min_CubeGetVar
static int Min_CubeGetVar(Min_Cube_t *p, int Var)
Definition: covInt.h:86
Min_CubeCheck
int Min_CubeCheck(Min_Cube_t *pCube)
Definition: covMinUtil.c:244
Min_EsopAddCube
void Min_EsopAddCube(Min_Man_t *p, Min_Cube_t *pCube)
Definition: covMinEsop.c:291
Min_CubeSetBit
static void Min_CubeSetBit(Min_Cube_t *p, int i)
Definition: covInt.h:84
Min_CubesTransform
static void Min_CubesTransform(Min_Cube_t *pCube, Min_Cube_t *pDist, Min_Cube_t *pMask)
Definition: covInt.h:542
Min_CoverCountCubes
static int Min_CoverCountCubes(Min_Cube_t *pCover)
Definition: covInt.h:274
Min_Cube_t_::nWords
unsigned nWords
Definition: covInt.h:58
Min_Cube_t_::nLits
unsigned nLits
Definition: covInt.h:59
Min_CoverContainsCube
static int Min_CoverContainsCube(Min_Man_t *p, Min_Cube_t *pCube)
Definition: covInt.h:620
Vec_IntPush
static void Vec_IntPush(Vec_Int_t *p, int Entry)
Definition: bblif.c:468
ABC_NAMESPACE_HEADER_START
#define ABC_NAMESPACE_HEADER_START
NAMESPACES ///.
Definition: abc_global.h:105
Extra_MmFixed_t_
Definition: extraUtilMemory.c:34
Min_CubesXor
static Min_Cube_t * Min_CubesXor(Min_Man_t *p, Min_Cube_t *pCube0, Min_Cube_t *pCube1)
Definition: covInt.h:479
ABC_NAMESPACE_HEADER_END
#define ABC_NAMESPACE_HEADER_END
Definition: abc_global.h:106
Min_CoverWriteStore
void Min_CoverWriteStore(FILE *pFile, Min_Man_t *p)
Definition: covMinUtil.c:159
Min_Man_t_::nCubes
int nCubes
Definition: covInt.h:50
Min_CubesAreEqual
static int Min_CubesAreEqual(Min_Cube_t *pCube0, Min_Cube_t *pCube1)
Definition: covInt.h:502
Min_Man_t_
Definition: covInt.h:37
Min_CubeGetLits
static void Min_CubeGetLits(Min_Cube_t *pCube, Vec_Int_t *vLits)
Definition: covInt.h:249
Min_Man_t_::nWords
int nWords
Definition: covInt.h:40
Min_Man_t_::pMemMan
Extra_MmFixed_t * pMemMan
Definition: covInt.h:41
Min_Man_t_::nVars
int nVars
Definition: covInt.h:39
Vec_Str_t_
Definition: bblif.c:47
Min_Man_t_::pTriv0
Min_Cube_t * pTriv0[2]
Definition: covInt.h:45
Min_CoverForEachCube
#define Min_CoverForEachCube(pCover, pCube)
Definition: covInt.h:65
Minisat::Var
int Var
Definition: SolverTypes.h:42
Min_CubeXorBit
static void Min_CubeXorBit(Min_Cube_t *p, int i)
Definition: covInt.h:85
Min_CubeAlloc
static Min_Cube_t * Min_CubeAlloc(Min_Man_t *p)
FUNCTION DEFINITIONS ///.
Definition: covInt.h:126
Min_CubesTransformOr
static void Min_CubesTransformOr(Min_Cube_t *pCube, Min_Cube_t *pDist)
Definition: covInt.h:563
assert
#define assert(ex)
Definition: util_old.h:213
Min_CoverRecycle
static void Min_CoverRecycle(Min_Man_t *p, Min_Cube_t *pCover)
Definition: covInt.h:205
Min_CoverSuppVarNum
int Min_CoverSuppVarNum(Min_Man_t *p, Min_Cube_t *pCover)
Definition: covMinUtil.c:317
Extra_MmFixedEntryRecycle
void Extra_MmFixedEntryRecycle(Extra_MmFixed_t *p, char *pEntry)
Definition: extraUtilMemory.c:253
Min_CubeHasBit
static int Min_CubeHasBit(Min_Cube_t *p, int i)
Definition: covInt.h:83
Min_SopAddCube
void Min_SopAddCube(Min_Man_t *p, Min_Cube_t *pCube)
Definition: covMinSop.c:433
Vec_IntClear
static void Vec_IntClear(Vec_Int_t *p)
Definition: bblif.c:452
Min_CoverWrite
void Min_CoverWrite(FILE *pFile, Min_Cube_t *pCover)
Definition: covMinUtil.c:140
Min_Man_t_::pBubble
Min_Cube_t * pBubble
Definition: covInt.h:48
Min_EsopMinimize
void Min_EsopMinimize(Min_Man_t *p)
FUNCTION DEFINITIONS ///.
Definition: covMinEsop.c:47
Min_SopMinimize
void Min_SopMinimize(Min_Man_t *p)
FUNCTION DEFINITIONS ///.
Definition: covMinSop.c:47
Min_Cube_t_::uData
unsigned uData[1]
Definition: covInt.h:60
Min_ManClean
void Min_ManClean(Min_Man_t *p, int nSupp)
Definition: covMinMan.c:83
Min_Man_t
typedefABC_NAMESPACE_HEADER_START struct Min_Man_t_ Min_Man_t
DECLARATIONS ///.
Definition: covInt.h:34
Min_ManFree
void Min_ManFree(Min_Man_t *p)
Definition: covMinMan.c:104