abc-master
 All Data Structures Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros
ifDec16.c
Go to the documentation of this file.
1 /**CFile****************************************************************
2 
3  FileName [ifDec16.c]
4 
5  SystemName [ABC: Logic synthesis and verification system.]
6 
7  PackageName [FPGA mapping based on priority cuts.]
8 
9  Synopsis [Fast checking procedures.]
10 
11  Author [Alan Mishchenko]
12 
13  Affiliation [UC Berkeley]
14 
15  Date [Ver. 1.0. Started - November 21, 2006.]
16 
17  Revision [$Id: ifDec16.c,v 1.00 2006/11/21 00:00:00 alanmi Exp $]
18 
19 ***********************************************************************/
20 
21 #include "if.h"
22 #include "bool/kit/kit.h"
23 #include "misc/vec/vecMem.h"
24 
25 ABC_NAMESPACE_IMPL_START
26 
27 ////////////////////////////////////////////////////////////////////////
28 /// DECLARATIONS ///
29 ////////////////////////////////////////////////////////////////////////
30 
31 #define CLU_VAR_MAX 16
32 #define CLU_WRD_MAX (1 << ((CLU_VAR_MAX)-6))
33 #define CLU_MEM_MAX 1000 // 1 GB
34 #define CLU_UNUSED 0xff
35 
36 // decomposition
37 typedef struct If_Grp_t_ If_Grp_t;
38 struct If_Grp_t_
39 {
40  char nVars;
41  char nMyu;
42  char pVars[CLU_VAR_MAX];
43 };
44 
45 // hash table entry
46 typedef struct If_Hte_t_ If_Hte_t;
47 struct If_Hte_t_
48 {
49  If_Hte_t * pNext;
50  unsigned Group;
51  unsigned Counter;
52  word pTruth[1];
53 };
54 
55 // variable swapping code
56 static word PMasks[5][3] = {
57  { ABC_CONST(0x9999999999999999), ABC_CONST(0x2222222222222222), ABC_CONST(0x4444444444444444) },
58  { ABC_CONST(0xC3C3C3C3C3C3C3C3), ABC_CONST(0x0C0C0C0C0C0C0C0C), ABC_CONST(0x3030303030303030) },
59  { ABC_CONST(0xF00FF00FF00FF00F), ABC_CONST(0x00F000F000F000F0), ABC_CONST(0x0F000F000F000F00) },
60  { ABC_CONST(0xFF0000FFFF0000FF), ABC_CONST(0x0000FF000000FF00), ABC_CONST(0x00FF000000FF0000) },
61  { ABC_CONST(0xFFFF00000000FFFF), ABC_CONST(0x00000000FFFF0000), ABC_CONST(0x0000FFFF00000000) }
62 };
63 // elementary truth tables
64 static word Truth6[6] = {
65  ABC_CONST(0xAAAAAAAAAAAAAAAA),
66  ABC_CONST(0xCCCCCCCCCCCCCCCC),
67  ABC_CONST(0xF0F0F0F0F0F0F0F0),
68  ABC_CONST(0xFF00FF00FF00FF00),
69  ABC_CONST(0xFFFF0000FFFF0000),
70  ABC_CONST(0xFFFFFFFF00000000)
71 };
72 static word TruthAll[CLU_VAR_MAX][CLU_WRD_MAX] = {{0}};
73 
74 extern void Kit_DsdPrintFromTruth( unsigned * pTruth, int nVars );
75 extern void Extra_PrintBinary( FILE * pFile, unsigned Sign[], int nBits );
76 
77 extern int If_CluSupportSize( word * t, int nVars );
78 
79 int s_Count2 = 0;
80 int s_Count3 = 0;
81 
82 ////////////////////////////////////////////////////////////////////////
83 /// FUNCTION DEFINITIONS ///
84 ////////////////////////////////////////////////////////////////////////
85 
86 static inline unsigned If_CluGrp2Uns( If_Grp_t * pG )
87 {
88  char * pChar = (char *)pG;
89  unsigned Res = 0;
90  int i;
91  for ( i = 0; i < 8; i++ )
92  Res |= ((pChar[i] & 15) << (i << 2));
93  return Res;
94 }
95 
96 static inline void If_CluUns2Grp( unsigned Group, If_Grp_t * pG )
97 {
98  char * pChar = (char *)pG;
99  int i;
100  for ( i = 0; i < 8; i++ )
101  pChar[i] = ((Group >> (i << 2)) & 15);
102 }
103 
104 unsigned int If_CluPrimeCudd( unsigned int p )
105 {
106  int i,pn;
107 
108  p--;
109  do {
110  p++;
111  if (p&1) {
112  pn = 1;
113  i = 3;
114  while ((unsigned) (i * i) <= p) {
115  if (p % i == 0) {
116  pn = 0;
117  break;
118  }
119  i += 2;
120  }
121  } else {
122  pn = 0;
123  }
124  } while (!pn);
125  return(p);
126 
127 } /* end of Cudd_Prime */
128 
129 // hash table
130 static inline int If_CluWordNum( int nVars )
131 {
132  return nVars <= 6 ? 1 : 1 << (nVars-6);
133 }
134 static inline int If_CluCountOnes( word t )
135 {
136  t = (t & ABC_CONST(0x5555555555555555)) + ((t>> 1) & ABC_CONST(0x5555555555555555));
137  t = (t & ABC_CONST(0x3333333333333333)) + ((t>> 2) & ABC_CONST(0x3333333333333333));
138  t = (t & ABC_CONST(0x0F0F0F0F0F0F0F0F)) + ((t>> 4) & ABC_CONST(0x0F0F0F0F0F0F0F0F));
139  t = (t & ABC_CONST(0x00FF00FF00FF00FF)) + ((t>> 8) & ABC_CONST(0x00FF00FF00FF00FF));
140  t = (t & ABC_CONST(0x0000FFFF0000FFFF)) + ((t>>16) & ABC_CONST(0x0000FFFF0000FFFF));
141  return (t & ABC_CONST(0x00000000FFFFFFFF)) + (t>>32);
142 }
143 
144 void If_CluHashTableCheck( If_Man_t * p )
145 {
146  int t = 1;
147  If_Hte_t * pEntry;
148  int i, RetValue, Status;
149  for ( i = 0; i < p->nTableSize[t]; i++ )
150  {
151  for ( pEntry = ((If_Hte_t **)p->pHashTable[t])[i]; pEntry; pEntry = pEntry->pNext )
152  {
153  Status = ((pEntry->Group & 15) > 0);
154  RetValue = If_CutPerformCheck16( NULL, (unsigned *)pEntry->pTruth, 13, If_CluSupportSize(pEntry->pTruth, 13), "555" );
155  if ( RetValue != Status )
156  {
157  Kit_DsdPrintFromTruth( (unsigned*)pEntry->pTruth, 13 ); printf( "\n" );
158  RetValue = If_CutPerformCheck16( NULL, (unsigned *)pEntry->pTruth, 13, If_CluSupportSize(pEntry->pTruth, 13), "555" );
159  printf( "Hash table problem!!!\n" );
160  }
161  }
162  }
163 }
164 void If_CluHashPrintStats( If_Man_t * p, int t )
165 {
166  If_Hte_t * pEntry;
167  int i, Counter;
168  for ( i = 0; i < p->nTableSize[t]; i++ )
169  {
170  Counter = 0;
171  for ( pEntry = ((If_Hte_t **)p->pHashTable[t])[i]; pEntry; pEntry = pEntry->pNext )
172  Counter++;
173  if ( Counter == 0 )
174  continue;
175  if ( Counter < 10 )
176  continue;
177  printf( "%d=%d ", i, Counter );
178  }
179 }
180 int If_CluHashFindMedian( If_Man_t * p, int t )
181 {
182  If_Hte_t * pEntry;
183  Vec_Int_t * vCounters;
184  int i, Max = 0, Total = 0, Half = 0;
185  vCounters = Vec_IntStart( 1000 );
186  for ( i = 0; i < p->nTableSize[t]; i++ )
187  {
188  for ( pEntry = ((If_Hte_t **)p->pHashTable[t])[i]; pEntry; pEntry = pEntry->pNext )
189  {
190  if ( Max < (int)pEntry->Counter )
191  {
192  Max = pEntry->Counter;
193  Vec_IntSetEntry( vCounters, pEntry->Counter, 0 );
194  }
195  Vec_IntAddToEntry( vCounters, pEntry->Counter, 1 );
196  Total++;
197  }
198  }
199  for ( i = Max; i > 0; i-- )
200  {
201  Half += Vec_IntEntry( vCounters, i );
202  if ( Half > Total/2 )
203  break;
204  }
205 /*
206  printf( "total = %d ", Total );
207  printf( "half = %d ", Half );
208  printf( "i = %d ", i );
209  printf( "Max = %d.\n", Max );
210 */
211  Vec_IntFree( vCounters );
212  return Abc_MaxInt( i, 1 );
213 }
214 int If_CluHashKey( word * pTruth, int nWords, int Size )
215 {
216  static unsigned BigPrimes[8] = {12582917, 25165843, 50331653, 100663319, 201326611, 402653189, 805306457, 1610612741};
217  unsigned Value = 0;
218  int i;
219  if ( nWords < 4 )
220  {
221  unsigned char * s = (unsigned char *)pTruth;
222  for ( i = 0; i < 8 * nWords; i++ )
223  Value ^= BigPrimes[i % 7] * s[i];
224  }
225  else
226  {
227  unsigned * s = (unsigned *)pTruth;
228  for ( i = 0; i < 2 * nWords; i++ )
229  Value ^= BigPrimes[i % 7] * s[i];
230  }
231  return Value % Size;
232 }
233 unsigned * If_CluHashLookup( If_Man_t * p, word * pTruth, int t )
234 {
235  If_Hte_t * pEntry, * pPrev;
236  int nWords, HashKey;
237  if ( p == NULL )
238  return NULL;
239  nWords = If_CluWordNum(p->pPars->nLutSize);
240  if ( p->pMemEntries == NULL )
241  p->pMemEntries = Mem_FixedStart( sizeof(If_Hte_t) + sizeof(word) * (If_CluWordNum(p->pPars->nLutSize) - 1) );
242  if ( p->pHashTable[t] == NULL )
243  {
244  // decide how large should be the table
245  int nEntriesMax1 = 4 * If_CluPrimeCudd( Vec_PtrSize(p->vObjs) * p->pPars->nCutsMax );
246  int nEntriesMax2 = (int)(((double)CLU_MEM_MAX * (1 << 20)) / If_CluWordNum(p->pPars->nLutSize) / 8);
247 // int nEntriesMax2 = 10000;
248  // create table
249  p->nTableSize[t] = If_CluPrimeCudd( Abc_MinInt(nEntriesMax1, nEntriesMax2)/2 );
250  p->pHashTable[t] = ABC_CALLOC( void *, p->nTableSize[t] );
251  }
252  // check if this entry exists
253  HashKey = If_CluHashKey( pTruth, nWords, p->nTableSize[t] );
254  for ( pEntry = ((If_Hte_t **)p->pHashTable[t])[HashKey]; pEntry; pEntry = pEntry->pNext )
255  if ( memcmp(pEntry->pTruth, pTruth, sizeof(word) * nWords) == 0 )
256  {
257  pEntry->Counter++;
258  return &pEntry->Group;
259  }
260  // resize the hash table
261  if ( p->nTableEntries[t] >= 2 * p->nTableSize[t] )
262  {
263  // collect useful entries
264  If_Hte_t * pPrev;
265  Vec_Ptr_t * vUseful = Vec_PtrAlloc( p->nTableEntries[t] );
266  int i, Median = If_CluHashFindMedian( p, t );
267  for ( i = 0; i < p->nTableSize[t]; i++ )
268  {
269  for ( pEntry = ((If_Hte_t **)p->pHashTable[t])[i]; pEntry; )
270  {
271  if ( (int)pEntry->Counter > Median )
272  {
273  Vec_PtrPush( vUseful, pEntry );
274  pEntry = pEntry->pNext;
275  }
276  else
277  {
278  pPrev = pEntry->pNext;
279  Mem_FixedEntryRecycle( p->pMemEntries, (char *)pEntry );
280  pEntry = pPrev;
281  }
282  }
283  }
284  // add useful entries
285  memset( p->pHashTable[t], 0, sizeof(void *) * p->nTableSize[t] );
286  Vec_PtrForEachEntry( If_Hte_t *, vUseful, pEntry, i )
287  {
288  HashKey = If_CluHashKey( pEntry->pTruth, nWords, p->nTableSize[t] );
289  pPrev = ((If_Hte_t **)p->pHashTable[t])[HashKey];
290  if ( pPrev == NULL || pEntry->Counter >= pPrev->Counter )
291  {
292  pEntry->pNext = pPrev;
293  ((If_Hte_t **)p->pHashTable[t])[HashKey] = pEntry;
294  }
295  else
296  {
297  while ( pPrev->pNext && pEntry->Counter < pPrev->pNext->Counter )
298  pPrev = pPrev->pNext;
299  pEntry->pNext = pPrev->pNext;
300  pPrev->pNext = pEntry;
301  }
302  }
303  p->nTableEntries[t] = Vec_PtrSize( vUseful );
304  Vec_PtrFree( vUseful );
305  }
306  // create entry
307  p->nTableEntries[t]++;
308  pEntry = (If_Hte_t *)Mem_FixedEntryFetch( p->pMemEntries );
309  memcpy( pEntry->pTruth, pTruth, sizeof(word) * nWords );
310  pEntry->Group = CLU_UNUSED;
311  pEntry->Counter = 1;
312  // insert at the beginning
313 // pEntry->pNext = ((If_Hte_t **)p->pHashTable[t])[HashKey];
314 // ((If_Hte_t **)p->pHashTable[t])[HashKey] = pEntry;
315  // insert at the end
316  pEntry->pNext = NULL;
317  for ( pPrev = ((If_Hte_t **)p->pHashTable[t])[HashKey]; pPrev && pPrev->pNext; pPrev = pPrev->pNext );
318  if ( pPrev == NULL )
319  ((If_Hte_t **)p->pHashTable[t])[HashKey] = pEntry;
320  else
321  pPrev->pNext = pEntry;
322  return &pEntry->Group;
323 }
324 
325 // variable permutation for large functions
326 static inline void If_CluClear( word * pIn, int nVars )
327 {
328  int w, nWords = If_CluWordNum( nVars );
329  for ( w = 0; w < nWords; w++ )
330  pIn[w] = 0;
331 }
332 static inline void If_CluFill( word * pIn, int nVars )
333 {
334  int w, nWords = If_CluWordNum( nVars );
335  for ( w = 0; w < nWords; w++ )
336  pIn[w] = ~(word)0;
337 }
338 static inline void If_CluCopy( word * pOut, word * pIn, int nVars )
339 {
340  int w, nWords = If_CluWordNum( nVars );
341  for ( w = 0; w < nWords; w++ )
342  pOut[w] = pIn[w];
343 }
344 static inline int If_CluEqual( word * pOut, word * pIn, int nVars )
345 {
346  int w, nWords = If_CluWordNum( nVars );
347  for ( w = 0; w < nWords; w++ )
348  if ( pOut[w] != pIn[w] )
349  return 0;
350  return 1;
351 }
352 static inline void If_CluAnd( word * pRes, word * pIn1, word * pIn2, int nVars )
353 {
354  int w, nWords = If_CluWordNum( nVars );
355  for ( w = 0; w < nWords; w++ )
356  pRes[w] = pIn1[w] & pIn2[w];
357 }
358 static inline void If_CluSharp( word * pRes, word * pIn1, word * pIn2, int nVars )
359 {
360  int w, nWords = If_CluWordNum( nVars );
361  for ( w = 0; w < nWords; w++ )
362  pRes[w] = pIn1[w] & ~pIn2[w];
363 }
364 static inline void If_CluOr( word * pRes, word * pIn1, word * pIn2, int nVars )
365 {
366  int w, nWords = If_CluWordNum( nVars );
367  for ( w = 0; w < nWords; w++ )
368  pRes[w] = pIn1[w] | pIn2[w];
369 }
370 static inline word If_CluAdjust( word t, int nVars )
371 {
372  assert( nVars >= 0 && nVars <= 6 );
373  if ( nVars == 6 )
374  return t;
375  t &= (((word)1) << (1 << nVars)) - 1;
376  if ( nVars == 0 )
377  t |= t << (1<<nVars++);
378  if ( nVars == 1 )
379  t |= t << (1<<nVars++);
380  if ( nVars == 2 )
381  t |= t << (1<<nVars++);
382  if ( nVars == 3 )
383  t |= t << (1<<nVars++);
384  if ( nVars == 4 )
385  t |= t << (1<<nVars++);
386  if ( nVars == 5 )
387  t |= t << (1<<nVars++);
388  return t;
389 }
390 static inline void If_CluAdjustBig( word * pF, int nVarsCur, int nVarsMax )
391 {
392  int v, nWords;
393  if ( nVarsCur == nVarsMax )
394  return;
395  assert( nVarsCur < nVarsMax );
396  for ( v = Abc_MaxInt( nVarsCur, 6 ); v < nVarsMax; v++ )
397  {
398  nWords = If_CluWordNum( v );
399  If_CluCopy( pF + nWords, pF, v );
400  }
401 }
402 static inline void If_CluSwapAdjacent( word * pOut, word * pIn, int iVar, int nVars )
403 {
404  int i, k, nWords = If_CluWordNum( nVars );
405  assert( iVar < nVars - 1 );
406  if ( iVar < 5 )
407  {
408  int Shift = (1 << iVar);
409  for ( i = 0; i < nWords; i++ )
410  pOut[i] = (pIn[i] & PMasks[iVar][0]) | ((pIn[i] & PMasks[iVar][1]) << Shift) | ((pIn[i] & PMasks[iVar][2]) >> Shift);
411  }
412  else if ( iVar > 5 )
413  {
414  int Step = (1 << (iVar - 6));
415  for ( k = 0; k < nWords; k += 4*Step )
416  {
417  for ( i = 0; i < Step; i++ )
418  pOut[i] = pIn[i];
419  for ( i = 0; i < Step; i++ )
420  pOut[Step+i] = pIn[2*Step+i];
421  for ( i = 0; i < Step; i++ )
422  pOut[2*Step+i] = pIn[Step+i];
423  for ( i = 0; i < Step; i++ )
424  pOut[3*Step+i] = pIn[3*Step+i];
425  pIn += 4*Step;
426  pOut += 4*Step;
427  }
428  }
429  else // if ( iVar == 5 )
430  {
431  for ( i = 0; i < nWords; i += 2 )
432  {
433  pOut[i] = (pIn[i] & ABC_CONST(0x00000000FFFFFFFF)) | ((pIn[i+1] & ABC_CONST(0x00000000FFFFFFFF)) << 32);
434  pOut[i+1] = (pIn[i+1] & ABC_CONST(0xFFFFFFFF00000000)) | ((pIn[i] & ABC_CONST(0xFFFFFFFF00000000)) >> 32);
435  }
436  }
437 }
438 
439 void If_CluChangePhase( word * pF, int nVars, int iVar )
440 {
441  int nWords = If_CluWordNum( nVars );
442  assert( iVar < nVars );
443  if ( iVar < 6 )
444  {
445  int i, Shift = (1 << iVar);
446  for ( i = 0; i < nWords; i++ )
447  pF[i] = ((pF[i] & ~Truth6[iVar]) << Shift) | ((pF[i] & Truth6[iVar]) >> Shift);
448  }
449  else
450  {
451  word Temp;
452  int i, k, Step = (1 << (iVar - 6));
453  for ( k = 0; k < nWords; k += 2*Step )
454  {
455  for ( i = 0; i < Step; i++ )
456  {
457  Temp = pF[i];
458  pF[i] = pF[Step+i];
459  pF[Step+i] = Temp;
460  }
461  pF += 2*Step;
462  }
463  }
464 }
465 void If_CluCountOnesInCofs( word * pTruth, int nVars, int * pStore )
466 {
467  int nWords = If_CluWordNum( nVars );
468  int i, k, nOnes = 0, Limit = Abc_MinInt( nVars, 6 );
469  memset( pStore, 0, sizeof(int) * 2 * nVars );
470  // compute positive cofactors
471  for ( k = 0; k < nWords; k++ )
472  for ( i = 0; i < Limit; i++ )
473  pStore[2*i+1] += If_CluCountOnes( pTruth[k] & Truth6[i] );
474  if ( nVars > 6 )
475  for ( k = 0; k < nWords; k++ )
476  for ( i = 6; i < nVars; i++ )
477  if ( k & (1 << (i-6)) )
478  pStore[2*i+1] += If_CluCountOnes( pTruth[k] );
479  // compute negative cofactors
480  for ( k = 0; k < nWords; k++ )
481  nOnes += If_CluCountOnes( pTruth[k] );
482  for ( i = 0; i < nVars; i++ )
483  pStore[2*i] = nOnes - pStore[2*i+1];
484 }
485 unsigned If_CluSemiCanonicize( word * pTruth, int nVars, int * pCanonPerm )
486 {
487  word pFunc[CLU_WRD_MAX], * pIn = pTruth, * pOut = pFunc, * pTemp;
488  int pStore[CLU_VAR_MAX*2];
489  unsigned uCanonPhase = 0;
490  int i, Temp, fChange, Counter = 0;
491 //Kit_DsdPrintFromTruth( (unsigned*)pTruth, nVars ); printf( "\n" );
492 
493  // collect signatures
494  If_CluCountOnesInCofs( pTruth, nVars, pStore );
495  // canonicize phase
496  for ( i = 0; i < nVars; i++ )
497  {
498  if ( pStore[2*i+0] <= pStore[2*i+1] )
499  continue;
500  uCanonPhase |= (1 << i);
501  Temp = pStore[2*i+0];
502  pStore[2*i+0] = pStore[2*i+1];
503  pStore[2*i+1] = Temp;
504  If_CluChangePhase( pIn, nVars, i );
505  }
506  // compute permutation
507  for ( i = 0; i < nVars; i++ )
508  pCanonPerm[i] = i;
509  do {
510  fChange = 0;
511  for ( i = 0; i < nVars-1; i++ )
512  {
513  if ( pStore[2*i] <= pStore[2*(i+1)] )
514  continue;
515  Counter++;
516  fChange = 1;
517 
518  Temp = pCanonPerm[i];
519  pCanonPerm[i] = pCanonPerm[i+1];
520  pCanonPerm[i+1] = Temp;
521 
522  Temp = pStore[2*i];
523  pStore[2*i] = pStore[2*(i+1)];
524  pStore[2*(i+1)] = Temp;
525 
526  Temp = pStore[2*i+1];
527  pStore[2*i+1] = pStore[2*(i+1)+1];
528  pStore[2*(i+1)+1] = Temp;
529 
530  If_CluSwapAdjacent( pOut, pIn, i, nVars );
531  pTemp = pIn; pIn = pOut; pOut = pTemp;
532  }
533  } while ( fChange );
534  // swap if it was moved an odd number of times
535  if ( Counter & 1 )
536  If_CluCopy( pOut, pIn, nVars );
537  return uCanonPhase;
538 }
539 void If_CluSemiCanonicizeVerify( word * pTruth, word * pTruth0, int nVars, int * pCanonPerm, unsigned uCanonPhase )
540 {
541  word pFunc[CLU_WRD_MAX], pGunc[CLU_WRD_MAX], * pIn = pTruth, * pOut = pFunc, * pTemp;
542  int i, Temp, fChange, Counter = 0;
543  If_CluCopy( pGunc, pTruth, nVars );
544  // undo permutation
545  do {
546  fChange = 0;
547  for ( i = 0; i < nVars-1; i++ )
548  {
549  if ( pCanonPerm[i] < pCanonPerm[i+1] )
550  continue;
551 
552  Counter++;
553  fChange = 1;
554 
555  Temp = pCanonPerm[i];
556  pCanonPerm[i] = pCanonPerm[i+1];
557  pCanonPerm[i+1] = Temp;
558 
559  If_CluSwapAdjacent( pOut, pIn, i, nVars );
560  pTemp = pIn; pIn = pOut; pOut = pTemp;
561  }
562  } while ( fChange );
563  if ( Counter & 1 )
564  If_CluCopy( pOut, pIn, nVars );
565  // undo phase
566  for ( i = 0; i < nVars; i++ )
567  if ( (uCanonPhase >> i) & 1 )
568  If_CluChangePhase( pTruth, nVars, i );
569  // compare
570  if ( !If_CluEqual(pTruth0, pTruth, nVars) )
571  {
572  Kit_DsdPrintFromTruth( (unsigned*)pTruth0, nVars ); printf( "\n" );
573  Kit_DsdPrintFromTruth( (unsigned*)pGunc, nVars ); printf( "\n" );
574  Kit_DsdPrintFromTruth( (unsigned*)pTruth, nVars ); printf( "\n" );
575  printf( "SemiCanonical verification FAILED!\n" );
576  }
577 }
578 
579 
580 void If_CluPrintGroup( If_Grp_t * g )
581 {
582  int i;
583  printf( "Vars = %d ", g->nVars );
584  printf( "Myu = %d {", g->nMyu );
585  for ( i = 0; i < g->nVars; i++ )
586  printf( " %c", 'a' + g->pVars[i] );
587  printf( " }\n" );
588 }
589 
590 void If_CluPrintConfig( int nVars, If_Grp_t * g, If_Grp_t * r, word BStruth, word * pFStruth )
591 {
592  assert( r->nVars == nVars - g->nVars + 1 + (g->nMyu > 2) );
593  If_CluPrintGroup( g );
594  if ( g->nVars < 6 )
595  BStruth = If_CluAdjust( BStruth, g->nVars );
596  Kit_DsdPrintFromTruth( (unsigned *)&BStruth, g->nVars );
597  printf( "\n" );
598  If_CluPrintGroup( r );
599  if ( r->nVars < 6 )
600  pFStruth[0] = If_CluAdjust( pFStruth[0], r->nVars );
601  Kit_DsdPrintFromTruth( (unsigned *)pFStruth, r->nVars );
602  printf( "\n" );
603 }
604 
605 
606 void If_CluInitTruthTables()
607 {
608  int i, k;
609  assert( CLU_VAR_MAX <= 16 );
610  for ( i = 0; i < 6; i++ )
611  for ( k = 0; k < CLU_WRD_MAX; k++ )
612  TruthAll[i][k] = Truth6[i];
613  for ( i = 6; i < CLU_VAR_MAX; i++ )
614  for ( k = 0; k < CLU_WRD_MAX; k++ )
615  TruthAll[i][k] = ((k >> (i-6)) & 1) ? ~(word)0 : 0;
616 
617 // Extra_PrintHex( stdout, TruthAll[6], 8 ); printf( "\n" );
618 // Extra_PrintHex( stdout, TruthAll[7], 8 ); printf( "\n" );
619 }
620 
621 
622 // verification
623 static void If_CluComposeLut( int nVars, If_Grp_t * g, word * t, word f[6][CLU_WRD_MAX], word * r )
624 {
625  word c[CLU_WRD_MAX];
626  int m, v;
627  If_CluClear( r, nVars );
628  for ( m = 0; m < (1<<g->nVars); m++ )
629  {
630  if ( !((t[m >> 6] >> (m & 63)) & 1) )
631  continue;
632  If_CluFill( c, nVars );
633  for ( v = 0; v < g->nVars; v++ )
634  if ( (m >> v) & 1 )
635  If_CluAnd( c, c, f[v], nVars );
636  else
637  If_CluSharp( c, c, f[v], nVars );
638  If_CluOr( r, r, c, nVars );
639  }
640 }
641 void If_CluVerify( word * pF, int nVars, If_Grp_t * g, If_Grp_t * r, word BStruth, word * pFStruth )
642 {
643  word pTTFans[6][CLU_WRD_MAX], pTTWire[CLU_WRD_MAX], pTTRes[CLU_WRD_MAX];
644  int i;
645  assert( g->nVars <= 6 && r->nVars <= 6 );
646 
647  if ( TruthAll[0][0] == 0 )
648  If_CluInitTruthTables();
649 
650  for ( i = 0; i < g->nVars; i++ )
651  If_CluCopy( pTTFans[i], TruthAll[(int)g->pVars[i]], nVars );
652  If_CluComposeLut( nVars, g, &BStruth, pTTFans, pTTWire );
653 
654  for ( i = 0; i < r->nVars; i++ )
655  if ( r->pVars[i] == nVars )
656  If_CluCopy( pTTFans[i], pTTWire, nVars );
657  else
658  If_CluCopy( pTTFans[i], TruthAll[(int)r->pVars[i]], nVars );
659  If_CluComposeLut( nVars, r, pFStruth, pTTFans, pTTRes );
660 
661  if ( !If_CluEqual(pTTRes, pF, nVars) )
662  {
663  printf( "\n" );
664  If_CluPrintConfig( nVars, g, r, BStruth, pFStruth );
665  Kit_DsdPrintFromTruth( (unsigned*)pTTRes, nVars ); printf( "\n" );
666  Kit_DsdPrintFromTruth( (unsigned*)pF, nVars ); printf( "\n" );
667 // Extra_PrintHex( stdout, (unsigned *)pF, nVars ); printf( "\n" );
668  printf( "Verification FAILED!\n" );
669  }
670 // else
671 // printf( "Verification succeed!\n" );
672 }
673 void If_CluVerify3( word * pF, int nVars, If_Grp_t * g, If_Grp_t * g2, If_Grp_t * r, word BStruth, word BStruth2, word FStruth )
674 {
675  word pTTFans[6][CLU_WRD_MAX], pTTWire[CLU_WRD_MAX], pTTWire2[CLU_WRD_MAX], pTTRes[CLU_WRD_MAX];
676  int i;
677  assert( g->nVars >= 2 && g2->nVars >= 2 && r->nVars >= 2 );
678  assert( g->nVars <= 6 && g2->nVars <= 6 && r->nVars <= 6 );
679 
680  if ( TruthAll[0][0] == 0 )
681  If_CluInitTruthTables();
682 
683  for ( i = 0; i < g->nVars; i++ )
684  If_CluCopy( pTTFans[i], TruthAll[(int)g->pVars[i]], nVars );
685  If_CluComposeLut( nVars, g, &BStruth, pTTFans, pTTWire );
686 
687  for ( i = 0; i < g2->nVars; i++ )
688  If_CluCopy( pTTFans[i], TruthAll[(int)g2->pVars[i]], nVars );
689  If_CluComposeLut( nVars, g2, &BStruth2, pTTFans, pTTWire2 );
690 
691  for ( i = 0; i < r->nVars; i++ )
692  if ( r->pVars[i] == nVars )
693  If_CluCopy( pTTFans[i], pTTWire, nVars );
694  else if ( r->pVars[i] == nVars + 1 )
695  If_CluCopy( pTTFans[i], pTTWire2, nVars );
696  else
697  If_CluCopy( pTTFans[i], TruthAll[(int)r->pVars[i]], nVars );
698  If_CluComposeLut( nVars, r, &FStruth, pTTFans, pTTRes );
699 
700  if ( !If_CluEqual(pTTRes, pF, nVars) )
701  {
702  printf( "%d\n", nVars );
703 // If_CluPrintConfig( nVars, g, r, BStruth, pFStruth );
704 // Extra_PrintHex( stdout, (unsigned *)pF, nVars ); printf( "\n" );
705 
706  Kit_DsdPrintFromTruth( (unsigned*)&BStruth, g->nVars ); printf( " " ); If_CluPrintGroup(g); // printf( "\n" );
707  Kit_DsdPrintFromTruth( (unsigned*)&BStruth2, g2->nVars ); printf( " " ); If_CluPrintGroup(g2); // printf( "\n" );
708  Kit_DsdPrintFromTruth( (unsigned*)&FStruth, r->nVars ); printf( " " ); If_CluPrintGroup(r); // printf( "\n" );
709 
710  Kit_DsdPrintFromTruth( (unsigned*)pTTWire, nVars ); printf( "\n" );
711  Kit_DsdPrintFromTruth( (unsigned*)pTTWire2, nVars ); printf( "\n" );
712  Kit_DsdPrintFromTruth( (unsigned*)pTTRes, nVars ); printf( "\n" );
713  Kit_DsdPrintFromTruth( (unsigned*)pF, nVars ); printf( "\n" );
714 // Extra_PrintHex( stdout, (unsigned *)pF, nVars ); printf( "\n" );
715  printf( "Verification FAILED!\n" );
716  }
717 // else
718 // printf( "Verification succeed!\n" );
719 }
720 
721 
722 
723 void If_CluSwapVars( word * pTruth, int nVars, int * V2P, int * P2V, int iVar, int jVar )
724 {
725  word low2High, high2Low, temp;
726  int nWords = If_CluWordNum(nVars);
727  int shift, step, iStep, jStep;
728  int w = 0, i = 0, j = 0;
729  static word PPMasks[6][6] = {
730  { ABC_CONST(0x2222222222222222), ABC_CONST(0x0A0A0A0A0A0A0A0A), ABC_CONST(0x00AA00AA00AA00AA), ABC_CONST(0x0000AAAA0000AAAA), ABC_CONST(0x00000000AAAAAAAA), ABC_CONST(0xAAAAAAAAAAAAAAAA) },
731  { ABC_CONST(0x0000000000000000), ABC_CONST(0x0C0C0C0C0C0C0C0C), ABC_CONST(0x00CC00CC00CC00CC), ABC_CONST(0x0000CCCC0000CCCC), ABC_CONST(0x00000000CCCCCCCC), ABC_CONST(0xCCCCCCCCCCCCCCCC) },
732  { ABC_CONST(0x0000000000000000), ABC_CONST(0x0000000000000000), ABC_CONST(0x00F000F000F000F0), ABC_CONST(0x0000F0F00000F0F0), ABC_CONST(0x00000000F0F0F0F0), ABC_CONST(0xF0F0F0F0F0F0F0F0) },
733  { ABC_CONST(0x0000000000000000), ABC_CONST(0x0000000000000000), ABC_CONST(0x0000000000000000), ABC_CONST(0x0000FF000000FF00), ABC_CONST(0x00000000FF00FF00), ABC_CONST(0xFF00FF00FF00FF00) },
734  { ABC_CONST(0x0000000000000000), ABC_CONST(0x0000000000000000), ABC_CONST(0x0000000000000000), ABC_CONST(0x0000000000000000), ABC_CONST(0x00000000FFFF0000), ABC_CONST(0xFFFF0000FFFF0000) },
735  { ABC_CONST(0x0000000000000000), ABC_CONST(0x0000000000000000), ABC_CONST(0x0000000000000000), ABC_CONST(0x0000000000000000), ABC_CONST(0x0000000000000000), ABC_CONST(0xFFFFFFFF00000000) }
736  };
737  if( iVar == jVar )
738  return;
739  if( jVar < iVar )
740  {
741  int varTemp = jVar;
742  jVar = iVar;
743  iVar = varTemp;
744  }
745  if ( iVar <= 5 && jVar <= 5 )
746  {
747  shift = (1 << jVar) - (1 << iVar);
748  for ( w = 0; w < nWords; w++ )
749  {
750  low2High = (pTruth[w] & PPMasks[iVar][jVar - 1] ) << shift;
751  pTruth[w] &= ~PPMasks[iVar][jVar - 1];
752  high2Low = (pTruth[w] & (PPMasks[iVar][jVar - 1] << shift )) >> shift;
753  pTruth[w] &= ~ (PPMasks[iVar][jVar - 1] << shift);
754  pTruth[w] = pTruth[w] | low2High | high2Low;
755  }
756  }
757  else if( iVar <= 5 && jVar > 5 )
758  {
759  step = If_CluWordNum(jVar + 1)/2;
760  shift = 1 << iVar;
761  for ( w = 0; w < nWords; w += 2*step )
762  {
763  for (j = 0; j < step; j++)
764  {
765  low2High = (pTruth[w + j] & PPMasks[iVar][5]) >> shift;
766  pTruth[w + j] &= ~PPMasks[iVar][5];
767  high2Low = (pTruth[w + step + j] & (PPMasks[iVar][5] >> shift)) << shift;
768  pTruth[w + step + j] &= ~(PPMasks[iVar][5] >> shift);
769  pTruth[w + j] |= high2Low;
770  pTruth[w + step + j] |= low2High;
771  }
772  }
773  }
774  else
775  {
776  iStep = If_CluWordNum(iVar + 1)/2;
777  jStep = If_CluWordNum(jVar + 1)/2;
778  for (w = 0; w < nWords; w += 2*jStep)
779  {
780  for (i = 0; i < jStep; i += 2*iStep)
781  {
782  for (j = 0; j < iStep; j++)
783  {
784  temp = pTruth[w + iStep + i + j];
785  pTruth[w + iStep + i + j] = pTruth[w + jStep + i + j];
786  pTruth[w + jStep + i + j] = temp;
787  }
788  }
789  }
790  }
791  if ( V2P && P2V )
792  {
793  V2P[P2V[iVar]] = jVar;
794  V2P[P2V[jVar]] = iVar;
795  P2V[iVar] ^= P2V[jVar];
796  P2V[jVar] ^= P2V[iVar];
797  P2V[iVar] ^= P2V[jVar];
798  }
799 }
800 void If_CluReverseOrder( word * pTruth, int nVars, int * V2P, int * P2V, int iVarStart )
801 {
802  int i, j, k;
803  for ( k = 0; k < (nVars-iVarStart)/2 ; k++ )
804  {
805  i = iVarStart + k;
806  j = nVars - 1 - k;
807  If_CluSwapVars( pTruth, nVars, V2P, P2V, i, j );
808  }
809 }
810 
811 // moves one var (v) to the given position (p)
812 void If_CluMoveVar2( word * pF, int nVars, int * Var2Pla, int * Pla2Var, int v, int p )
813 {
814  If_CluSwapVars( pF, nVars, Var2Pla, Pla2Var, Var2Pla[v], p );
815 }
816 
817 // moves one var (v) to the given position (p)
818 void If_CluMoveVar( word * pF, int nVars, int * Var2Pla, int * Pla2Var, int v, int p )
819 {
820  word pG[CLU_WRD_MAX], * pIn = pF, * pOut = pG, * pTemp;
821  int iPlace0, iPlace1, Count = 0;
822  assert( v >= 0 && v < nVars );
823  while ( Var2Pla[v] < p )
824  {
825  iPlace0 = Var2Pla[v];
826  iPlace1 = Var2Pla[v]+1;
827  If_CluSwapAdjacent( pOut, pIn, iPlace0, nVars );
828  pTemp = pIn; pIn = pOut, pOut = pTemp;
829  Var2Pla[Pla2Var[iPlace0]]++;
830  Var2Pla[Pla2Var[iPlace1]]--;
831  Pla2Var[iPlace0] ^= Pla2Var[iPlace1];
832  Pla2Var[iPlace1] ^= Pla2Var[iPlace0];
833  Pla2Var[iPlace0] ^= Pla2Var[iPlace1];
834  Count++;
835  }
836  while ( Var2Pla[v] > p )
837  {
838  iPlace0 = Var2Pla[v]-1;
839  iPlace1 = Var2Pla[v];
840  If_CluSwapAdjacent( pOut, pIn, iPlace0, nVars );
841  pTemp = pIn; pIn = pOut, pOut = pTemp;
842  Var2Pla[Pla2Var[iPlace0]]++;
843  Var2Pla[Pla2Var[iPlace1]]--;
844  Pla2Var[iPlace0] ^= Pla2Var[iPlace1];
845  Pla2Var[iPlace1] ^= Pla2Var[iPlace0];
846  Pla2Var[iPlace0] ^= Pla2Var[iPlace1];
847  Count++;
848  }
849  if ( Count & 1 )
850  If_CluCopy( pF, pIn, nVars );
851  assert( Pla2Var[p] == v );
852 }
853 
854 // moves vars to be the most signiticant ones (Group[0] is MSB)
855 void If_CluMoveGroupToMsb( word * pF, int nVars, int * V2P, int * P2V, If_Grp_t * g )
856 {
857  int v;
858  for ( v = 0; v < g->nVars; v++ )
859  If_CluMoveVar( pF, nVars, V2P, P2V, g->pVars[g->nVars - 1 - v], nVars - 1 - v );
860 }
861 
862 
863 // reverses the variable order
864 void If_CluReverseOrder_old( word * pF, int nVars, int * V2P, int * P2V, int iVarStart )
865 {
866  word pG[CLU_WRD_MAX];
867  int v;
868 
869  If_CluCopy( pG, pF, nVars );
870 
871 // for ( v = 0; v < nVars; v++ )
872 // printf( "%c ", 'a' + P2V[v] );
873 // printf( " --- " );
874 
875  for ( v = iVarStart; v < nVars; v++ )
876  If_CluMoveVar( pF, nVars, V2P, P2V, P2V[iVarStart], nVars - 1 - (v - iVarStart) );
877 
878 // for ( v = 0; v < nVars; v++ )
879 // printf( "%c ", 'a' + P2V[v] );
880 // printf( "\n" );
881 
882 // if ( iVarStart > 0 )
883 // return;
884 
885  If_CluReverseOrder( pG, nVars, NULL, NULL, iVarStart );
886  if ( If_CluEqual( pG, pF, nVars ) )
887  {
888 // printf( "+" );
889  }
890  else
891  {
892 /*
893  printf( "\n" );
894  Kit_DsdPrintFromTruth( (unsigned*)pF, nVars ); printf( "\n" );
895  Kit_DsdPrintFromTruth( (unsigned*)pG, nVars );
896  printf( "\n" );
897 */
898  printf( "%d ", nVars );
899  }
900 }
901 
902 // return the number of cofactors w.r.t. the topmost vars (nBSsize)
903 int If_CluCountCofs( word * pF, int nVars, int nBSsize, int iShift, word pCofs[3][CLU_WRD_MAX/4] )
904 {
905  word iCofs[128], iCof, Result = 0;
906  word * pCofA, * pCofB;
907  int nMints = (1 << nBSsize);
908  int i, c, w, nCofs;
909  assert( nBSsize >= 2 && nBSsize <= 7 && nBSsize < nVars );
910  if ( nVars - nBSsize < 6 )
911  {
912  int nShift = (1 << (nVars - nBSsize));
913  word Mask = ((((word)1) << nShift) - 1);
914  for ( nCofs = i = 0; i < nMints; i++ )
915  {
916  iCof = (pF[(iShift + i * nShift) / 64] >> ((iShift + i * nShift) & 63)) & Mask;
917  for ( c = 0; c < nCofs; c++ )
918  if ( iCof == iCofs[c] )
919  break;
920  if ( c == nCofs )
921  iCofs[nCofs++] = iCof;
922  if ( pCofs && iCof != iCofs[0] )
923  Result |= (((word)1) << i);
924  if ( nCofs == 5 )
925  break;
926  }
927  if ( nCofs <= 2 && pCofs )
928  {
929  assert( nBSsize <= 6 );
930  pCofs[0][0] = iCofs[0];
931  pCofs[1][0] = (nCofs == 2) ? iCofs[1] : iCofs[0];
932  pCofs[2][0] = Result;
933  }
934  }
935  else
936  {
937  int nWords = If_CluWordNum( nVars - nBSsize );
938  assert( nWords * nMints == If_CluWordNum(nVars) );
939  for ( nCofs = i = 0; i < nMints; i++ )
940  {
941  pCofA = pF + i * nWords;
942  for ( c = 0; c < nCofs; c++ )
943  {
944  pCofB = pF + iCofs[c] * nWords;
945  for ( w = 0; w < nWords; w++ )
946  if ( pCofA[w] != pCofB[w] )
947  break;
948  if ( w == nWords )
949  break;
950  }
951  if ( c == nCofs )
952  iCofs[nCofs++] = i;
953  if ( pCofs )
954  {
955  assert( nBSsize <= 6 );
956  pCofB = pF + iCofs[0] * nWords;
957  for ( w = 0; w < nWords; w++ )
958  if ( pCofA[w] != pCofB[w] )
959  break;
960  if ( w != nWords )
961  Result |= (((word)1) << i);
962  }
963  if ( nCofs == 5 )
964  break;
965  }
966  if ( nCofs <= 2 && pCofs )
967  {
968  If_CluCopy( pCofs[0], pF + iCofs[0] * nWords, nVars - nBSsize );
969  If_CluCopy( pCofs[1], pF + ((nCofs == 2) ? iCofs[1] : iCofs[0]) * nWords, nVars - nBSsize );
970  pCofs[2][0] = Result;
971  }
972  }
973  assert( nCofs >= 1 && nCofs <= 5 );
974  return nCofs;
975 }
976 
977 // return the number of cofactors w.r.t. the topmost vars (nBSsize)
978 int If_CluCountCofs4( word * pF, int nVars, int nBSsize, word pCofs[6][CLU_WRD_MAX/4] )
979 {
980  word iCofs[128], iCof, Result0 = 0, Result1 = 0;
981  int nMints = (1 << nBSsize);
982  int i, c, nCofs;
983  assert( pCofs );
984  assert( nBSsize >= 2 && nBSsize <= 6 && nBSsize < nVars );
985  if ( nVars - nBSsize < 6 )
986  {
987  int nShift = (1 << (nVars - nBSsize));
988  word Mask = ((((word)1) << nShift) - 1);
989  for ( nCofs = i = 0; i < nMints; i++ )
990  {
991  iCof = (pF[(i * nShift) / 64] >> ((i * nShift) & 63)) & Mask;
992  for ( c = 0; c < nCofs; c++ )
993  if ( iCof == iCofs[c] )
994  break;
995  if ( c == nCofs )
996  iCofs[nCofs++] = iCof;
997  if ( c == 1 || c == 3 )
998  Result0 |= (((word)1) << i);
999  if ( c == 2 || c == 3 )
1000  Result1 |= (((word)1) << i);
1001  }
1002  assert( nCofs >= 3 && nCofs <= 4 );
1003  pCofs[0][0] = iCofs[0];
1004  pCofs[1][0] = iCofs[1];
1005  pCofs[2][0] = iCofs[2];
1006  pCofs[3][0] = (nCofs == 4) ? iCofs[3] : iCofs[2];
1007  pCofs[4][0] = Result0;
1008  pCofs[5][0] = Result1;
1009  }
1010  else
1011  assert( 0 );
1012  return nCofs;
1013 }
1014 
1015 void If_CluCofactors( word * pF, int nVars, int iVar, word * pCof0, word * pCof1 )
1016 {
1017  int nWords = If_CluWordNum( nVars );
1018  assert( iVar < nVars );
1019  if ( iVar < 6 )
1020  {
1021  int i, Shift = (1 << iVar);
1022  for ( i = 0; i < nWords; i++ )
1023  {
1024  pCof0[i] = (pF[i] & ~Truth6[iVar]) | ((pF[i] & ~Truth6[iVar]) << Shift);
1025  pCof1[i] = (pF[i] & Truth6[iVar]) | ((pF[i] & Truth6[iVar]) >> Shift);
1026  }
1027  }
1028  else
1029  {
1030  int i, k, Step = (1 << (iVar - 6));
1031  for ( k = 0; k < nWords; k += 2*Step )
1032  {
1033  for ( i = 0; i < Step; i++ )
1034  {
1035  pCof0[i] = pCof0[Step+i] = pF[i];
1036  pCof1[i] = pCof1[Step+i] = pF[Step+i];
1037  }
1038  pF += 2*Step;
1039  pCof0 += 2*Step;
1040  pCof1 += 2*Step;
1041  }
1042  }
1043 }
1044 
1045 // returns 1 if we have special case of cofactors; otherwise, returns 0
1046 int If_CluDetectSpecialCaseCofs( word * pF, int nVars, int iVar )
1047 {
1048  word Cof0, Cof1;
1049  int State[6] = {0};
1050  int i, nWords = If_CluWordNum( nVars );
1051  assert( iVar < nVars );
1052  if ( iVar < 6 )
1053  {
1054  int Shift = (1 << iVar);
1055  for ( i = 0; i < nWords; i++ )
1056  {
1057  Cof0 = (pF[i] & ~Truth6[iVar]);
1058  Cof1 = ((pF[i] & Truth6[iVar]) >> Shift);
1059 
1060  if ( Cof0 == 0 )
1061  State[0]++;
1062  else if ( Cof0 == ~Truth6[iVar] )
1063  State[1]++;
1064  else if ( Cof1 == 0 )
1065  State[2]++;
1066  else if ( Cof1 == ~Truth6[iVar] )
1067  State[3]++;
1068  else if ( Cof0 == ~Cof1 )
1069  State[4]++;
1070  else if ( Cof0 == Cof1 )
1071  State[5]++;
1072  }
1073  }
1074  else
1075  {
1076  int k, Step = (1 << (iVar - 6));
1077  for ( k = 0; k < nWords; k += 2*Step )
1078  {
1079  for ( i = 0; i < Step; i++ )
1080  {
1081  Cof0 = pF[i];
1082  Cof1 = pF[Step+i];
1083 
1084  if ( Cof0 == 0 )
1085  State[0]++;
1086  else if ( Cof0 == ~(word)0 )
1087  State[1]++;
1088  else if ( Cof1 == 0 )
1089  State[2]++;
1090  else if ( Cof1 == ~(word)0 )
1091  State[3]++;
1092  else if ( Cof0 == ~Cof1 )
1093  State[4]++;
1094  else if ( Cof0 == Cof1 )
1095  State[5]++;
1096  }
1097  pF += 2*Step;
1098  }
1099  nWords /= 2;
1100  }
1101  assert( State[5] != nWords );
1102  for ( i = 0; i < 5; i++ )
1103  {
1104  assert( State[i] <= nWords );
1105  if ( State[i] == nWords )
1106  return i;
1107  }
1108  return -1;
1109 }
1110 
1111 // returns 1 if we have special case of cofactors; otherwise, returns 0
1112 If_Grp_t If_CluDecUsingCofs( word * pTruth, int nVars, int nLutLeaf )
1113 {
1114  If_Grp_t G = {0};
1115  word pF2[CLU_WRD_MAX], * pF = pF2;
1116  int Var2Pla[CLU_VAR_MAX+2], Pla2Var[CLU_VAR_MAX+2];
1117  int V2P[CLU_VAR_MAX+2], P2V[CLU_VAR_MAX+2];
1118  int nVarsNeeded = nVars - nLutLeaf;
1119  int v, i, k, iVar, State;
1120 //Kit_DsdPrintFromTruth( (unsigned*)pTruth, nVars ); printf( "\n" );
1121  // create local copy
1122  If_CluCopy( pF, pTruth, nVars );
1123  for ( k = 0; k < nVars; k++ )
1124  Var2Pla[k] = Pla2Var[k] = k;
1125  // find decomposable vars
1126  for ( i = 0; i < nVarsNeeded; i++ )
1127  {
1128  for ( v = nVars - 1; v >= 0; v-- )
1129  {
1130  State = If_CluDetectSpecialCaseCofs( pF, nVars, v );
1131  if ( State == -1 )
1132  continue;
1133  // update the variable place
1134  iVar = Pla2Var[v];
1135  while ( Var2Pla[iVar] < nVars - 1 )
1136  {
1137  int iPlace0 = Var2Pla[iVar];
1138  int iPlace1 = Var2Pla[iVar]+1;
1139  Var2Pla[Pla2Var[iPlace0]]++;
1140  Var2Pla[Pla2Var[iPlace1]]--;
1141  Pla2Var[iPlace0] ^= Pla2Var[iPlace1];
1142  Pla2Var[iPlace1] ^= Pla2Var[iPlace0];
1143  Pla2Var[iPlace0] ^= Pla2Var[iPlace1];
1144  }
1145  // move this variable to the top
1146  for ( k = 0; k < nVars; k++ )
1147  V2P[k] = P2V[k] = k;
1148 //Kit_DsdPrintFromTruth( (unsigned*)pF, nVars ); printf( "\n" );
1149  If_CluMoveVar( pF, nVars, V2P, P2V, v, nVars - 1 );
1150 //Kit_DsdPrintFromTruth( (unsigned*)pF, nVars ); printf( "\n" );
1151  // choose cofactor to follow
1152  iVar = nVars - 1;
1153  if ( State == 0 || State == 1 ) // need cof1
1154  {
1155  if ( iVar < 6 )
1156  pF[0] = (pF[0] & Truth6[iVar]) | ((pF[0] & Truth6[iVar]) >> (1 << iVar));
1157  else
1158  pF += If_CluWordNum( nVars ) / 2;
1159  }
1160  else // need cof0
1161  {
1162  if ( iVar < 6 )
1163  pF[0] = (pF[0] & ~Truth6[iVar]) | ((pF[0] & ~Truth6[iVar]) << (1 << iVar));
1164  }
1165  // update the variable count
1166  nVars--;
1167  break;
1168  }
1169  if ( v == -1 )
1170  return G;
1171  }
1172  // create the resulting group
1173  G.nVars = nLutLeaf;
1174  G.nMyu = 2;
1175  for ( v = 0; v < G.nVars; v++ )
1176  G.pVars[v] = Pla2Var[v];
1177  return G;
1178 }
1179 
1180 
1181 
1182 // deriving decomposition
1183 word If_CluDeriveDisjoint( word * pF, int nVars, int * V2P, int * P2V, If_Grp_t * g, If_Grp_t * r )
1184 {
1185  word pCofs[3][CLU_WRD_MAX/4];
1186  int i, RetValue, nFSset = nVars - g->nVars;
1187  RetValue = If_CluCountCofs( pF, nVars, g->nVars, 0, pCofs );
1188 // assert( RetValue == 2 );
1189 
1190  if ( nFSset < 6 )
1191  pF[0] = (pCofs[1][0] << (1 << nFSset)) | pCofs[0][0];
1192  else
1193  {
1194  If_CluCopy( pF, pCofs[0], nFSset );
1195  If_CluCopy( pF + If_CluWordNum(nFSset), pCofs[1], nFSset );
1196  }
1197  // create the resulting group
1198  if ( r )
1199  {
1200  r->nVars = nFSset + 1;
1201  r->nMyu = 0;
1202  for ( i = 0; i < nFSset; i++ )
1203  r->pVars[i] = P2V[i];
1204  r->pVars[nFSset] = nVars;
1205  }
1206  return pCofs[2][0];
1207 }
1208 void If_CluDeriveDisjoint4( word * pF, int nVars, int * V2P, int * P2V, If_Grp_t * g, If_Grp_t * r, word * pTruth0, word * pTruth1 )
1209 {
1210  word pCofs[6][CLU_WRD_MAX/4];
1211  word Cof0, Cof1;
1212  int i, RetValue, nFSset = nVars - g->nVars;
1213 
1214  assert( g->nVars <= 6 && nFSset <= 4 );
1215 
1216  RetValue = If_CluCountCofs4( pF, nVars, g->nVars, pCofs );
1217  if ( RetValue != 3 && RetValue != 4 )
1218  printf( "If_CluDeriveDisjoint4(): Error!!!\n" );
1219 
1220  Cof0 = (pCofs[1][0] << (1 << nFSset)) | pCofs[0][0];
1221  Cof1 = (pCofs[3][0] << (1 << nFSset)) | pCofs[2][0];
1222  pF[0] = (Cof1 << (1 << (nFSset+1))) | Cof0;
1223  pF[0] = If_CluAdjust( pF[0], nFSset + 2 );
1224 
1225  // create the resulting group
1226  r->nVars = nFSset + 2;
1227  r->nMyu = 0;
1228  for ( i = 0; i < nFSset; i++ )
1229  r->pVars[i] = P2V[i];
1230  r->pVars[nFSset] = nVars;
1231  r->pVars[nFSset+1] = nVars+1;
1232 
1233  *pTruth0 = If_CluAdjust( pCofs[4][0], g->nVars );
1234  *pTruth1 = If_CluAdjust( pCofs[5][0], g->nVars );
1235 }
1236 
1237 word If_CluDeriveNonDisjoint( word * pF, int nVars, int * V2P, int * P2V, If_Grp_t * g, If_Grp_t * r )
1238 {
1239  word pCofs[2][CLU_WRD_MAX];
1240  word Truth0, Truth1, Truth;
1241  int i, nFSset = nVars - g->nVars, nFSset1 = nFSset + 1;
1242  If_CluCofactors( pF, nVars, nVars - 1, pCofs[0], pCofs[1] );
1243 
1244 // Extra_PrintHex( stdout, (unsigned *)pCofs[0], nVars ); printf( "\n" );
1245 // Extra_PrintHex( stdout, (unsigned *)pCofs[1], nVars ); printf( "\n" );
1246 
1247  g->nVars--;
1248  Truth0 = If_CluDeriveDisjoint( pCofs[0], nVars - 1, V2P, P2V, g, NULL );
1249  Truth1 = If_CluDeriveDisjoint( pCofs[1], nVars - 1, V2P, P2V, g, NULL );
1250  Truth = (Truth1 << (1 << g->nVars)) | Truth0;
1251  g->nVars++;
1252  if ( nFSset1 < 6 )
1253  pF[0] = (pCofs[1][0] << (1 << nFSset1)) | pCofs[0][0];
1254  else
1255  {
1256  If_CluCopy( pF, pCofs[0], nFSset1 );
1257  If_CluCopy( pF + If_CluWordNum(nFSset1), pCofs[1], nFSset1 );
1258  }
1259 
1260 // Extra_PrintHex( stdout, (unsigned *)&Truth0, 6 ); printf( "\n" );
1261 // Extra_PrintHex( stdout, (unsigned *)&Truth1, 6 ); printf( "\n" );
1262 // Extra_PrintHex( stdout, (unsigned *)&pCofs[0][0], 6 ); printf( "\n" );
1263 // Extra_PrintHex( stdout, (unsigned *)&pCofs[1][0], 6 ); printf( "\n" );
1264 // Extra_PrintHex( stdout, (unsigned *)&Truth, 6 ); printf( "\n" );
1265 // Extra_PrintHex( stdout, (unsigned *)&pF[0], 6 ); printf( "\n" );
1266 
1267  // create the resulting group
1268  r->nVars = nFSset + 2;
1269  r->nMyu = 0;
1270  for ( i = 0; i < nFSset; i++ )
1271  r->pVars[i] = P2V[i];
1272  r->pVars[nFSset] = nVars;
1273  r->pVars[nFSset+1] = g->pVars[g->nVars - 1];
1274  return Truth;
1275 }
1276 
1277 // check non-disjoint decomposition
1278 int If_CluCheckNonDisjointGroup( word * pF, int nVars, int * V2P, int * P2V, If_Grp_t * g )
1279 {
1280  int v, i, nCofsBest2;
1281  if ( (g->nMyu == 3 || g->nMyu == 4) )
1282  {
1283  word pCofs[2][CLU_WRD_MAX];
1284  // try cofactoring w.r.t. each variable
1285  for ( v = 0; v < g->nVars; v++ )
1286  {
1287  If_CluCofactors( pF, nVars, V2P[(int)g->pVars[v]], pCofs[0], pCofs[1] );
1288  nCofsBest2 = If_CluCountCofs( pCofs[0], nVars, g->nVars, 0, NULL );
1289  if ( nCofsBest2 > 2 )
1290  continue;
1291  nCofsBest2 = If_CluCountCofs( pCofs[1], nVars, g->nVars, 0, NULL );
1292  if ( nCofsBest2 > 2 )
1293  continue;
1294  // found good shared variable - move to the end
1295  If_CluMoveVar( pF, nVars, V2P, P2V, g->pVars[v], nVars-1 );
1296  for ( i = 0; i < g->nVars; i++ )
1297  g->pVars[i] = P2V[nVars-g->nVars+i];
1298  return 1;
1299  }
1300  }
1301  return 0;
1302 }
1303 
1304 
1305 // finds a good var group (cof count < 6; vars are MSBs)
1306 If_Grp_t If_CluFindGroup( word * pF, int nVars, int iVarStart, int iVarStop, int * V2P, int * P2V, int nBSsize, int fDisjoint )
1307 {
1308  int fVerbose = 0;
1309  int nRounds = 2;//nBSsize;
1310  If_Grp_t G = {0}, * g = &G;//, BestG = {0};
1311  int i, r, v, nCofs, VarBest, nCofsBest2;
1312  assert( nVars > nBSsize && nVars >= nBSsize + iVarStart && nVars <= CLU_VAR_MAX );
1313  assert( nBSsize >= 2 && nBSsize <= 6 );
1314  assert( !iVarStart || !iVarStop );
1315  // start with the default group
1316  g->nVars = nBSsize;
1317  g->nMyu = If_CluCountCofs( pF, nVars, nBSsize, 0, NULL );
1318  for ( i = 0; i < nBSsize; i++ )
1319  g->pVars[i] = P2V[nVars-nBSsize+i];
1320  // check if good enough
1321  if ( g->nMyu == 2 )
1322  return G;
1323  if ( !fDisjoint && If_CluCheckNonDisjointGroup( pF, nVars, V2P, P2V, g ) )
1324  {
1325 // BestG = G;
1326  return G;
1327  }
1328  if ( nVars == nBSsize + iVarStart )
1329  {
1330  g->nVars = 0;
1331  return G;
1332  }
1333 
1334  if ( fVerbose )
1335  {
1336  printf( "Iter %2d ", -1 );
1337  If_CluPrintGroup( g );
1338  }
1339 
1340  // try to find better group
1341  for ( r = 0; r < nRounds; r++ )
1342  {
1343  if ( nBSsize < nVars-1 )
1344  {
1345  // find the best var to add
1346  VarBest = P2V[nVars-1-nBSsize];
1347  nCofsBest2 = If_CluCountCofs( pF, nVars, nBSsize+1, 0, NULL );
1348  for ( v = nVars-2-nBSsize; v >= iVarStart; v-- )
1349  {
1350 // If_CluMoveVar( pF, nVars, V2P, P2V, P2V[v], nVars-1-nBSsize );
1351  If_CluMoveVar2( pF, nVars, V2P, P2V, P2V[v], nVars-1-nBSsize );
1352  nCofs = If_CluCountCofs( pF, nVars, nBSsize+1, 0, NULL );
1353  if ( nCofsBest2 >= nCofs )
1354  {
1355  nCofsBest2 = nCofs;
1356  VarBest = P2V[nVars-1-nBSsize];
1357  }
1358  }
1359  // go back
1360 // If_CluMoveVar( pF, nVars, V2P, P2V, VarBest, nVars-1-nBSsize );
1361  If_CluMoveVar2( pF, nVars, V2P, P2V, VarBest, nVars-1-nBSsize );
1362  // update best bound set
1363  nCofs = If_CluCountCofs( pF, nVars, nBSsize+1, 0, NULL );
1364  assert( nCofs == nCofsBest2 );
1365  }
1366 
1367  // find the best var to remove
1368  VarBest = P2V[nVars-1-nBSsize];
1369  nCofsBest2 = If_CluCountCofs( pF, nVars, nBSsize, 0, NULL );
1370  for ( v = nVars-nBSsize; v < nVars-iVarStop; v++ )
1371  {
1372 // If_CluMoveVar( pF, nVars, V2P, P2V, P2V[v], nVars-1-nBSsize );
1373  If_CluMoveVar2( pF, nVars, V2P, P2V, P2V[v], nVars-1-nBSsize );
1374  nCofs = If_CluCountCofs( pF, nVars, nBSsize, 0, NULL );
1375  if ( nCofsBest2 >= nCofs )
1376  {
1377  nCofsBest2 = nCofs;
1378  VarBest = P2V[nVars-1-nBSsize];
1379  }
1380  }
1381 
1382  // go back
1383 // If_CluMoveVar( pF, nVars, V2P, P2V, VarBest, nVars-1-nBSsize );
1384  If_CluMoveVar2( pF, nVars, V2P, P2V, VarBest, nVars-1-nBSsize );
1385  // update best bound set
1386  nCofs = If_CluCountCofs( pF, nVars, nBSsize, 0, NULL );
1387  assert( nCofs == nCofsBest2 );
1388  if ( g->nMyu >= nCofs )
1389  {
1390  g->nVars = nBSsize;
1391  g->nMyu = nCofs;
1392  for ( i = 0; i < nBSsize; i++ )
1393  g->pVars[i] = P2V[nVars-nBSsize+i];
1394  }
1395 
1396  if ( fVerbose )
1397  {
1398  printf( "Iter %2d ", r );
1399  If_CluPrintGroup( g );
1400  }
1401 
1402  // check if good enough
1403  if ( g->nMyu == 2 )
1404  return G;
1405  if ( !fDisjoint && If_CluCheckNonDisjointGroup( pF, nVars, V2P, P2V, g ) )
1406  {
1407 // BestG = G;
1408  return G;
1409  }
1410  }
1411 
1412  assert( r == nRounds );
1413  g->nVars = 0;
1414  return G;
1415 // return BestG;
1416 }
1417 
1418 
1419 // double check that the given group has a decomposition
1420 void If_CluCheckGroup( word * pTruth, int nVars, If_Grp_t * g )
1421 {
1422  word pF[CLU_WRD_MAX];
1423  int v, nCofs, V2P[CLU_VAR_MAX], P2V[CLU_VAR_MAX];
1424  assert( g->nVars >= 2 && g->nVars <= 6 ); // vars
1425  assert( g->nMyu >= 2 && g->nMyu <= 4 ); // cofs
1426  // create permutation
1427  for ( v = 0; v < nVars; v++ )
1428  V2P[v] = P2V[v] = v;
1429  // create truth table
1430  If_CluCopy( pF, pTruth, nVars );
1431  // move group up
1432  If_CluMoveGroupToMsb( pF, nVars, V2P, P2V, g );
1433  // check the number of cofactors
1434  nCofs = If_CluCountCofs( pF, nVars, g->nVars, 0, NULL );
1435  if ( nCofs != g->nMyu )
1436  printf( "Group check 0 has failed.\n" );
1437  // check compatible
1438  if ( nCofs > 2 )
1439  {
1440  nCofs = If_CluCountCofs( pF, nVars-1, g->nVars-1, 0, NULL );
1441  if ( nCofs > 2 )
1442  printf( "Group check 1 has failed.\n" );
1443  nCofs = If_CluCountCofs( pF, nVars-1, g->nVars-1, (1 << (nVars-1)), NULL );
1444  if ( nCofs > 2 )
1445  printf( "Group check 2 has failed.\n" );
1446  }
1447 }
1448 
1449 
1450 // double check that the permutation derived is correct
1451 void If_CluCheckPerm( word * pTruth, word * pF, int nVars, int * V2P, int * P2V )
1452 {
1453  int i;
1454  for ( i = 0; i < nVars; i++ )
1455  If_CluMoveVar( pF, nVars, V2P, P2V, i, i );
1456 
1457  if ( !If_CluEqual( pTruth, pF, nVars ) )
1458  printf( "Permutation FAILED.\n" );
1459 // else
1460 // printf( "Permutation successful\n" );
1461 }
1462 
1463 
1464 
1465 
1466 static inline int If_CluSuppIsMinBase( int Supp )
1467 {
1468  return (Supp & (Supp+1)) == 0;
1469 }
1470 static inline int If_CluHasVar( word * t, int nVars, int iVar )
1471 {
1472  int nWords = If_CluWordNum( nVars );
1473  assert( iVar < nVars );
1474  if ( iVar < 6 )
1475  {
1476  int i, Shift = (1 << iVar);
1477  for ( i = 0; i < nWords; i++ )
1478  if ( (t[i] & ~Truth6[iVar]) != ((t[i] & Truth6[iVar]) >> Shift) )
1479  return 1;
1480  return 0;
1481  }
1482  else
1483  {
1484  int i, k, Step = (1 << (iVar - 6));
1485  for ( k = 0; k < nWords; k += 2*Step )
1486  {
1487  for ( i = 0; i < Step; i++ )
1488  if ( t[i] != t[Step+i] )
1489  return 1;
1490  t += 2*Step;
1491  }
1492  return 0;
1493  }
1494 }
1495 static inline int If_CluSupport( word * t, int nVars )
1496 {
1497  int v, Supp = 0;
1498  for ( v = 0; v < nVars; v++ )
1499  if ( If_CluHasVar( t, nVars, v ) )
1500  Supp |= (1 << v);
1501  return Supp;
1502 }
1503 int If_CluSupportSize( word * t, int nVars )
1504 {
1505  int v, SuppSize = 0;
1506  for ( v = 0; v < nVars; v++ )
1507  if ( If_CluHasVar( t, nVars, v ) )
1508  SuppSize++;
1509  return SuppSize;
1510 }
1511 static inline void If_CluTruthShrink( word * pF, int nVars, int nVarsAll, unsigned Phase )
1512 {
1513  word pG[CLU_WRD_MAX], * pIn = pF, * pOut = pG, * pTemp;
1514  int i, k, Var = 0, Counter = 0;
1515  assert( nVarsAll <= 16 );
1516  for ( i = 0; i < nVarsAll; i++ )
1517  if ( Phase & (1 << i) )
1518  {
1519  for ( k = i-1; k >= Var; k-- )
1520  {
1521  If_CluSwapAdjacent( pOut, pIn, k, nVarsAll );
1522  pTemp = pIn; pIn = pOut, pOut = pTemp;
1523  Counter++;
1524  }
1525  Var++;
1526  }
1527  assert( Var == nVars );
1528  // swap if it was moved an odd number of times
1529  if ( Counter & 1 )
1530  If_CluCopy( pOut, pIn, nVarsAll );
1531 }
1532 int If_CluMinimumBase( word * t, int * pSupp, int nVarsAll, int * pnVars )
1533 {
1534  int v, iVar = 0, uSupp = 0;
1535  assert( nVarsAll <= 16 );
1536  for ( v = 0; v < nVarsAll; v++ )
1537  if ( If_CluHasVar( t, nVarsAll, v ) )
1538  {
1539  uSupp |= (1 << v);
1540  if ( pSupp )
1541  pSupp[iVar] = pSupp[v];
1542  iVar++;
1543  }
1544  if ( pnVars )
1545  *pnVars = iVar;
1546  if ( If_CluSuppIsMinBase( uSupp ) )
1547  return 0;
1548  If_CluTruthShrink( t, iVar, nVarsAll, uSupp );
1549  return 1;
1550 }
1551 
1552 // returns the best group found
1553 If_Grp_t If_CluCheck( If_Man_t * p, word * pTruth0, int nVars, int iVarStart, int iVarStop, int nLutLeaf, int nLutRoot,
1554  If_Grp_t * pR, word * pFunc0, word * pFunc1, word * pLeftOver, int fHashing )
1555 {
1556 // int fEnableHashing = 0;
1557  If_Grp_t G1 = {0}, R = {0};
1558  unsigned * pHashed = NULL;
1559  word Truth, pTruth[CLU_WRD_MAX], pF[CLU_WRD_MAX];//, pG[CLU_WRD_MAX];
1560  int V2P[CLU_VAR_MAX+2], P2V[CLU_VAR_MAX+2], pCanonPerm[CLU_VAR_MAX];
1561  int i, nSupp, uCanonPhase;
1562  int nLutSize = p ? p->pPars->nLutSize : nVars;
1563  assert( nVars <= CLU_VAR_MAX );
1564  assert( nVars <= nLutLeaf + nLutRoot - 1 );
1565 
1566  if ( pR )
1567  {
1568  pR->nVars = 0;
1569  *pFunc0 = 0;
1570  *pFunc1 = 0;
1571  }
1572 
1573  // canonicize truth table
1574  If_CluCopy( pTruth, pTruth0, nLutSize );
1575 
1576  if ( 0 )
1577  {
1578  uCanonPhase = If_CluSemiCanonicize( pTruth, nVars, pCanonPerm );
1579  If_CluAdjustBig( pTruth, nVars, nLutSize );
1580  }
1581 
1582 // If_CluSemiCanonicizeVerify( pTruth, pTruth0, nVars, pCanonPerm, uCanonPhase );
1583 // If_CluCopy( pTruth, pTruth0, nLutSize );
1584 
1585  /*
1586  {
1587  int pCanonPerm[32];
1588  short pStore[32];
1589  unsigned uCanonPhase;
1590  If_CluCopy( pF, pTruth, nVars );
1591  uCanonPhase = Kit_TruthSemiCanonicize( pF, pG, nVars, pCanonPerm );
1592  G1.nVars = 1;
1593  return G1;
1594  }
1595 */
1596  // check minnimum base
1597  If_CluCopy( pF, pTruth, nVars );
1598  for ( i = 0; i < nVars; i++ )
1599  V2P[i] = P2V[i] = i;
1600  // check support
1601  nSupp = If_CluSupport( pF, nVars );
1602 //Extra_PrintBinary( stdout, &nSupp, 16 ); printf( "\n" );
1603  if ( !nSupp || !If_CluSuppIsMinBase(nSupp) )
1604  {
1605 // assert( 0 );
1606  return G1;
1607  }
1608 
1609  // check hash table
1610  if ( p && fHashing )
1611  {
1612  pHashed = If_CluHashLookup( p, pTruth, 0 );
1613  if ( pHashed && *pHashed != CLU_UNUSED )
1614  If_CluUns2Grp( *pHashed, &G1 );
1615  }
1616 
1617  // update the variable order so that the first var was the last one
1618  if ( iVarStop )
1619  If_CluMoveVar( pF, nVars, V2P, P2V, 0, nVars-1 );
1620 
1621  if ( G1.nVars == 0 )
1622  {
1623  s_Count2++;
1624 
1625  // detect easy cofs
1626  if ( iVarStart == 0 )
1627  G1 = If_CluDecUsingCofs( pTruth, nVars, nLutLeaf );
1628  if ( G1.nVars == 0 )
1629  {
1630  // perform testing
1631  G1 = If_CluFindGroup( pF, nVars, iVarStart, iVarStop, V2P, P2V, nLutLeaf, nLutLeaf + nLutRoot == nVars + 1 );
1632  // If_CluCheckPerm( pTruth, pF, nVars, V2P, P2V );
1633  if ( G1.nVars == 0 )
1634  {
1635  // perform testing with a smaller set
1636  if ( nVars < nLutLeaf + nLutRoot - 2 )
1637  {
1638  nLutLeaf--;
1639  G1 = If_CluFindGroup( pF, nVars, iVarStart, iVarStop, V2P, P2V, nLutLeaf, nLutLeaf + nLutRoot == nVars + 1 );
1640  nLutLeaf++;
1641  }
1642  // perform testing with a smaller set
1643  if ( nLutLeaf > 4 && nVars < nLutLeaf + nLutRoot - 3 )
1644  {
1645  nLutLeaf--;
1646  nLutLeaf--;
1647  G1 = If_CluFindGroup( pF, nVars, iVarStart, iVarStop, V2P, P2V, nLutLeaf, nLutLeaf + nLutRoot == nVars + 1 );
1648  nLutLeaf++;
1649  nLutLeaf++;
1650  }
1651  if ( G1.nVars == 0 )
1652  {
1653  // perform testing with a different order
1654  If_CluReverseOrder( pF, nVars, V2P, P2V, iVarStart );
1655  G1 = If_CluFindGroup( pF, nVars, iVarStart, iVarStop, V2P, P2V, nLutLeaf, nLutLeaf + nLutRoot == nVars + 1 );
1656 
1657  // check permutation
1658  // If_CluCheckPerm( pTruth, pF, nVars, V2P, P2V );
1659  if ( G1.nVars == 0 )
1660  {
1661  // remember free set, just in case
1662 // for ( i = 0; i < nVars - nLutLeaf; i++ )
1663 /// G1.pVars[nLutLeaf+i] = P2V[i];
1664  // if <XY>, this will not be used
1665  // if <XYZ>, this will not be hashed
1666 
1667  /*
1668  if ( nVars == 6 )
1669  {
1670  Extra_PrintHex( stdout, (unsigned *)pF, nVars ); printf( " " );
1671  Kit_DsdPrintFromTruth( (unsigned*)pF, nVars ); printf( "\n" );
1672  if ( !If_CutPerformCheck07( (unsigned *)pF, 6, 6, NULL ) )
1673  printf( "no\n" );
1674  }
1675  */
1676  if ( pHashed )
1677  *pHashed = If_CluGrp2Uns( &G1 );
1678  return G1;
1679  }
1680  }
1681  }
1682  }
1683  }
1684 
1685  // derive
1686  if ( pR )
1687  {
1688  int iNewPos;
1689 
1690  If_CluMoveGroupToMsb( pF, nVars, V2P, P2V, &G1 );
1691  if ( G1.nMyu == 2 )
1692  {
1693  Truth = If_CluDeriveDisjoint( pF, nVars, V2P, P2V, &G1, &R );
1694  iNewPos = R.nVars - 1;
1695  }
1696  else
1697  {
1698  Truth = If_CluDeriveNonDisjoint( pF, nVars, V2P, P2V, &G1, &R );
1699  iNewPos = R.nVars - 2;
1700  }
1701  assert( R.pVars[iNewPos] == nVars );
1702 
1703  // adjust the functions
1704  Truth = If_CluAdjust( Truth, G1.nVars );
1705  if ( R.nVars < 6 )
1706  pF[0] = If_CluAdjust( pF[0], R.nVars );
1707 
1708 // Kit_DsdPrintFromTruth( (unsigned*)&Truth, G1.nVars ); printf( " ...1\n" );
1709 // Kit_DsdPrintFromTruth( (unsigned*)pF, R.nVars ); printf( " ...1\n" );
1710 
1711  // update the variable order of R so that the new var was the first one
1712 // if ( iVarStart == 0 )
1713  {
1714  int k, V2P2[CLU_VAR_MAX+2], P2V2[CLU_VAR_MAX+2];
1715  assert( iNewPos >= iVarStart );
1716  for ( k = 0; k < R.nVars; k++ )
1717  V2P2[k] = P2V2[k] = k;
1718  If_CluMoveVar( pF, R.nVars, V2P2, P2V2, iNewPos, iVarStart );
1719  for ( k = iNewPos; k > iVarStart; k-- )
1720  R.pVars[k] = R.pVars[k-1];
1721  R.pVars[iVarStart] = nVars;
1722  }
1723 
1724 // Kit_DsdPrintFromTruth( (unsigned*)pF, R.nVars ); printf( " ...2\n" );
1725 
1726  if ( pLeftOver )
1727  {
1728  if ( R.nVars < 6 )
1729  *pLeftOver = If_CluAdjust( pF[0], R.nVars );
1730  else
1731  If_CluCopy( pLeftOver, pF, R.nVars );
1732  If_CluAdjustBig( pLeftOver, R.nVars, nLutSize );
1733  }
1734 
1735  // perform checking
1736  if ( 0 )
1737  {
1738  If_CluCheckGroup( pTruth, nVars, &G1 );
1739  If_CluVerify( pTruth, nVars, &G1, &R, Truth, pF );
1740  }
1741 
1742  // save functions
1743  *pR = R;
1744  if ( pFunc0 )
1745  *pFunc0 = pF[0];
1746  if ( pFunc1 )
1747  *pFunc1 = Truth;
1748  }
1749 
1750  if ( pHashed )
1751  *pHashed = If_CluGrp2Uns( &G1 );
1752  return G1;
1753 }
1754 
1755 /*
1756 static inline word Abc_Tt6Cofactor0( word t, int iVar )
1757 {
1758  assert( iVar >= 0 && iVar < 6 );
1759  return (t &~Truth6[iVar]) | ((t &~Truth6[iVar]) << (1<<iVar));
1760 }
1761 static inline word Abc_Tt6Cofactor1( word t, int iVar )
1762 {
1763  assert( iVar >= 0 && iVar < 6 );
1764  return (t & Truth6[iVar]) | ((t & Truth6[iVar]) >> (1<<iVar));
1765 }
1766 */
1767 int If_CluCheckDecInAny( word t, int nVars )
1768 {
1769  int v, u, Cof2[2], Cof4[4];
1770  for ( v = 0; v < nVars; v++ )
1771  {
1772  Cof2[0] = Abc_Tt6Cofactor0( t, v );
1773  Cof2[1] = Abc_Tt6Cofactor1( t, v );
1774  for ( u = v+1; u < nVars; u++ )
1775  {
1776  Cof4[0] = Abc_Tt6Cofactor0( Cof2[0], u );
1777  Cof4[1] = Abc_Tt6Cofactor1( Cof2[0], u );
1778  Cof4[2] = Abc_Tt6Cofactor0( Cof2[1], u );
1779  Cof4[3] = Abc_Tt6Cofactor1( Cof2[1], u );
1780  if ( Cof4[0] == Cof4[1] && Cof4[0] == Cof4[2] )
1781  return 1;
1782  if ( Cof4[0] == Cof4[2] && Cof4[0] == Cof4[3] )
1783  return 1;
1784  if ( Cof4[0] == Cof4[1] && Cof4[0] == Cof4[3] )
1785  return 1;
1786  if ( Cof4[1] == Cof4[2] && Cof4[1] == Cof4[3] )
1787  return 1;
1788  }
1789  }
1790  return 0;
1791 }
1792 int If_CluCheckDecIn( word t, int nVars )
1793 {
1794  int v, u, Cof2[2], Cof4[4];
1795 // for ( v = 0; v < nVars; v++ )
1796  for ( v = 0; v < 1; v++ ) // restrict to the first (decomposed) input
1797  {
1798  Cof2[0] = Abc_Tt6Cofactor0( t, v );
1799  Cof2[1] = Abc_Tt6Cofactor1( t, v );
1800  for ( u = v+1; u < nVars; u++ )
1801  {
1802  Cof4[0] = Abc_Tt6Cofactor0( Cof2[0], u );
1803  Cof4[1] = Abc_Tt6Cofactor1( Cof2[0], u );
1804  Cof4[2] = Abc_Tt6Cofactor0( Cof2[1], u );
1805  Cof4[3] = Abc_Tt6Cofactor1( Cof2[1], u );
1806  if ( Cof4[0] == Cof4[1] && Cof4[0] == Cof4[2] )
1807  return 1;
1808  if ( Cof4[0] == Cof4[2] && Cof4[0] == Cof4[3] )
1809  return 1;
1810  if ( Cof4[0] == Cof4[1] && Cof4[0] == Cof4[3] )
1811  return 1;
1812  if ( Cof4[1] == Cof4[2] && Cof4[1] == Cof4[3] )
1813  return 1;
1814  }
1815  }
1816  return 0;
1817 }
1818 int If_CluCheckDecInU( word t, int nVars )
1819 {
1820  int v, u, Cof2[2], Cof4[4];
1821 // for ( v = 0; v < nVars; v++ )
1822  for ( v = 0; v < 1; v++ ) // restrict to the first (decomposed) input
1823  {
1824  Cof2[0] = Abc_Tt6Cofactor0( t, v );
1825  Cof2[1] = Abc_Tt6Cofactor1( t, v );
1826  for ( u = v+1; u < nVars; u++ )
1827  {
1828  Cof4[0] = Abc_Tt6Cofactor0( Cof2[0], u ); // 00
1829  Cof4[1] = Abc_Tt6Cofactor1( Cof2[0], u ); // 01
1830  Cof4[2] = Abc_Tt6Cofactor0( Cof2[1], u ); // 10
1831  Cof4[3] = Abc_Tt6Cofactor1( Cof2[1], u ); // 11
1832  if ( Cof4[0] == Cof4[1] && Cof4[0] == Cof4[2] ) // F * a
1833  return 1;
1834  if ( Cof4[0] == Cof4[2] && Cof4[0] == Cof4[3] ) // !F * a
1835  return 1;
1836  }
1837  }
1838  return 0;
1839 }
1840 int If_CluCheckDecOut( word t, int nVars )
1841 {
1842  int v;
1843  for ( v = 0; v < nVars; v++ )
1844  if (
1845  (t & Truth6[v]) == 0 || // F * !a
1846  (~t & Truth6[v]) == 0 || // !F * !a
1847  (t & ~Truth6[v]) == 0 || // F * a
1848  (~t & ~Truth6[v]) == 0 // !F * a
1849  )
1850  return 1;
1851  return 0;
1852 }
1853 int If_CluCheckDecOutU( word t, int nVars )
1854 {
1855  int v;
1856  for ( v = 0; v < nVars; v++ )
1857  if (
1858  (t & ~Truth6[v]) == 0 || // F * a
1859  (~t & ~Truth6[v]) == 0 // !F * a
1860  )
1861  return 1;
1862  return 0;
1863 }
1864 
1865 int If_CutPerformCheck45( If_Man_t * p, unsigned * pTruth, int nVars, int nLeaves, char * pStr )
1866 {
1867  // 5LUT -> 4LUT
1868  If_Grp_t G, R;
1869  word Func0, Func1;
1870  G = If_CluCheck( p, (word *)pTruth, nLeaves, 0, 0, 5, 4, &R, &Func0, &Func1, NULL, 0 );
1871  if ( G.nVars == 0 )
1872  return 0;
1873  Func0 = If_CluAdjust( Func0, R.nVars );
1874  Func1 = If_CluAdjust( Func1, G.nVars );
1875 #if 0
1876  Kit_DsdPrintFromTruth( pTruth, nVars ); printf( "\n" );
1877  Kit_DsdPrintFromTruth( (unsigned*)&Func0, R.nVars ); printf( "\n" );
1878  Kit_DsdPrintFromTruth( (unsigned*)&Func1, G.nVars ); printf( "\n" );
1879  If_CluPrintGroup( &R );
1880  If_CluPrintGroup( &G );
1881 #endif
1882  if ( G.nVars < 5 || (p->pPars->fEnableCheck75 && If_CluCheckDecOut(Func1, 5)) || (p->pPars->fEnableCheck75u && If_CluCheckDecOutU(Func1, 5)) )
1883  return 1;
1884  return 0;
1885 }
1886 int If_CutPerformCheck54( If_Man_t * p, unsigned * pTruth, int nVars, int nLeaves, char * pStr )
1887 {
1888  // 4LUT -> 5LUT
1889  If_Grp_t G, R;
1890  word Func0, Func1;
1891  G = If_CluCheck( p, (word *)pTruth, nLeaves, 0, 0, 4, 5, &R, &Func0, &Func1, NULL, 0 );
1892  if ( G.nVars == 0 )
1893  return 0;
1894  Func0 = If_CluAdjust( Func0, R.nVars );
1895  Func1 = If_CluAdjust( Func1, G.nVars );
1896 #if 0
1897  Kit_DsdPrintFromTruth( pTruth, nVars ); printf( "\n" );
1898  Kit_DsdPrintFromTruth( (unsigned*)&Func0, R.nVars ); printf( "\n" );
1899  Kit_DsdPrintFromTruth( (unsigned*)&Func1, G.nVars ); printf( "\n" );
1900  If_CluPrintGroup( &R );
1901  If_CluPrintGroup( &G );
1902 #endif
1903  if ( R.nVars < 5 || (p->pPars->fEnableCheck75 && If_CluCheckDecIn(Func0, 5)) || (p->pPars->fEnableCheck75u && If_CluCheckDecInU(Func0, 5)) )
1904  return 1;
1905  return 0;
1906 }
1907 
1908 // returns the best group found
1909 If_Grp_t If_CluCheck3( If_Man_t * p, word * pTruth0, int nVars, int nLutLeaf, int nLutLeaf2, int nLutRoot,
1910  If_Grp_t * pR, If_Grp_t * pG2, word * pFunc0, word * pFunc1, word * pFunc2 )
1911 {
1912  int fEnableHashing = 0;
1913  static int Counter = 0;
1914  unsigned * pHashed = NULL;
1915  word pLeftOver[CLU_WRD_MAX], Func0, Func1, Func2;
1916  If_Grp_t G1 = {0}, G2 = {0}, R = {0}, R2 = {0};
1917  int i;
1918  Counter++;
1919 // if ( Counter == 37590 )
1920 // {
1921 // int ns = 0;
1922 // }
1923 
1924  // check hash table
1925  if ( p && fEnableHashing )
1926  {
1927  pHashed = If_CluHashLookup( p, pTruth0, 1 );
1928  if ( pHashed && *pHashed != CLU_UNUSED )
1929  {
1930  If_CluUns2Grp( *pHashed, &G1 );
1931  return G1;
1932  }
1933  }
1934  s_Count3++;
1935 
1936  // check two-node decomposition
1937  G1 = If_CluCheck( p, pTruth0, nVars, 0, 0, nLutLeaf, nLutRoot + nLutLeaf2 - 1, &R2, &Func0, &Func1, pLeftOver, 0 );
1938  // decomposition does not exist
1939  if ( G1.nVars == 0 )
1940  {
1941  // check for decomposition with two outputs
1942  if ( (G1.nMyu == 3 || G1.nMyu == 4) && nLutLeaf == nLutLeaf2 && nVars - nLutLeaf + 2 <= nLutRoot )
1943  {
1944  int V2P[CLU_VAR_MAX+2], P2V[CLU_VAR_MAX+2];
1945  word Func0, Func1, Func2;
1946  int iVar0, iVar1;
1947 
1948  G1.nVars = nLutLeaf;
1949  If_CluCopy( pLeftOver, pTruth0, nVars );
1950  for ( i = 0; i < nVars; i++ )
1951  V2P[i] = P2V[i] = i;
1952 
1953  If_CluMoveGroupToMsb( pLeftOver, nVars, V2P, P2V, &G1 );
1954  If_CluDeriveDisjoint4( pLeftOver, nVars, V2P, P2V, &G1, &R, &Func1, &Func2 );
1955 
1956  // move the two vars to the front
1957  for ( i = 0; i < R.nVars; i++ )
1958  V2P[i] = P2V[i] = i;
1959  If_CluMoveVar( pLeftOver, R.nVars, V2P, P2V, R.nVars-2, 0 );
1960  If_CluMoveVar( pLeftOver, R.nVars, V2P, P2V, R.nVars-1, 1 );
1961  iVar0 = R.pVars[R.nVars-2];
1962  iVar1 = R.pVars[R.nVars-1];
1963  for ( i = R.nVars-1; i > 1; i-- )
1964  R.pVars[i] = R.pVars[i-2];
1965  R.pVars[0] = iVar0;
1966  R.pVars[1] = iVar1;
1967 
1968  Func0 = pLeftOver[0];
1969  If_CluVerify3( pTruth0, nVars, &G1, &G1, &R, Func1, Func2, Func0 );
1970  if ( pFunc1 && pFunc2 )
1971  {
1972  *pFunc0 = Func0;
1973  *pFunc1 = Func1;
1974  *pFunc2 = Func2;
1975  *pG2 = G1;
1976  *pR = R;
1977  }
1978 
1979  if ( pHashed )
1980  *pHashed = If_CluGrp2Uns( &G1 );
1981 // Kit_DsdPrintFromTruth( (unsigned*)pTruth0, nVars ); printf( "\n" );
1982 // If_CluPrintGroup( &G1 );
1983  return G1;
1984  }
1985 
1986 /*
1987 // if ( nVars == 6 )
1988  {
1989 // Extra_PrintHex( stdout, (unsigned *)pTruth0, nVars ); printf( " " );
1990  Kit_DsdPrintFromTruth( (unsigned*)pTruth0, nVars ); printf( "\n" );
1991  if ( p != NULL )
1992  If_CluCheck3( NULL, pTruth0, nVars, nLutLeaf, nLutLeaf2, nLutRoot, pR, pG2, pFunc0, pFunc1, pFunc2 );
1993  }
1994 */
1995  if ( pHashed )
1996  *pHashed = If_CluGrp2Uns( &G1 );
1997  return G1;
1998  }
1999  // decomposition exists and sufficient
2000  if ( R2.nVars <= nLutRoot )
2001  {
2002  if ( pG2 ) *pG2 = G2;
2003  if ( pR ) *pR = R2;
2004  if ( pFunc0 ) *pFunc0 = Func0;
2005  if ( pFunc1 ) *pFunc1 = Func1;
2006  if ( pFunc2 ) *pFunc2 = 0;
2007  if ( pHashed )
2008  *pHashed = If_CluGrp2Uns( &G1 );
2009  return G1;
2010  }
2011 
2012  // try second decomposition
2013  {
2014  int Test = 0;
2015  if ( Test )
2016  {
2017  Kit_DsdPrintFromTruth( (unsigned*)&pLeftOver, R2.nVars ); printf( "\n" );
2018  }
2019  }
2020 
2021  // the new variable is at the bottom - skip it (iVarStart = 1)
2022  if ( p->pPars->nStructType == 0 ) // allowed
2023  G2 = If_CluCheck( p, pLeftOver, R2.nVars, 0, 0, nLutLeaf2, nLutRoot, &R, &Func0, &Func2, NULL, 0 );
2024  else if ( p->pPars->nStructType == 1 ) // not allowed
2025  G2 = If_CluCheck( p, pLeftOver, R2.nVars, 1, 0, nLutLeaf2, nLutRoot, &R, &Func0, &Func2, NULL, 0 );
2026  else if ( p->pPars->nStructType == 2 ) // required
2027  G2 = If_CluCheck( p, pLeftOver, R2.nVars, 0, 1, nLutLeaf2, nLutRoot, &R, &Func0, &Func2, NULL, 0 );
2028  else assert( 0 );
2029 
2030  if ( G2.nVars == 0 )
2031  {
2032  if ( pHashed )
2033  *pHashed = If_CluGrp2Uns( &G2 );
2034  return G2;
2035  }
2036  // remap variables
2037  for ( i = 0; i < G2.nVars; i++ )
2038  {
2039  assert( G2.pVars[i] < R2.nVars );
2040  G2.pVars[i] = R2.pVars[ (int)G2.pVars[i] ];
2041  }
2042  // remap variables
2043  for ( i = 0; i < R.nVars; i++ )
2044  {
2045  if ( R.pVars[i] == R2.nVars )
2046  R.pVars[i] = nVars + 1;
2047  else
2048  R.pVars[i] = R2.pVars[ (int)R.pVars[i] ];
2049  }
2050 
2051  // decomposition exist
2052  if ( pG2 ) *pG2 = G2;
2053  if ( pR ) *pR = R;
2054  if ( pFunc0 ) *pFunc0 = Func0;
2055  if ( pFunc1 ) *pFunc1 = Func1;
2056  if ( pFunc2 ) *pFunc2 = Func2;
2057  if ( pHashed )
2058  *pHashed = If_CluGrp2Uns( &G1 );
2059 
2060  // verify
2061 // If_CluVerify3( pTruth0, nVars, &G1, &G2, &R, Func1, Func2, Func0 );
2062  return G1;
2063 }
2064 
2065 // returns the best group found
2066 int If_CluCheckExt( void * pMan, word * pTruth, int nVars, int nLutLeaf, int nLutRoot,
2067  char * pLut0, char * pLut1, word * pFunc0, word * pFunc1 )
2068 {
2069  If_Man_t * p = (If_Man_t *)pMan;
2070  If_Grp_t G, R;
2071  G = If_CluCheck( p, pTruth, nVars, 0, 0, nLutLeaf, nLutRoot, &R, pFunc0, pFunc1, NULL, 0 );
2072  memcpy( pLut0, &R, sizeof(If_Grp_t) );
2073  memcpy( pLut1, &G, sizeof(If_Grp_t) );
2074 // memcpy( pLut2, &G2, sizeof(If_Grp_t) );
2075  return (G.nVars > 0);
2076 }
2077 
2078 // returns the best group found
2079 int If_CluCheckExt3( void * pMan, word * pTruth, int nVars, int nLutLeaf, int nLutLeaf2, int nLutRoot,
2080  char * pLut0, char * pLut1, char * pLut2, word * pFunc0, word * pFunc1, word * pFunc2 )
2081 {
2082  If_Man_t * p = (If_Man_t *)pMan;
2083  If_Grp_t G, G2, R;
2084  G = If_CluCheck3( p, pTruth, nVars, nLutLeaf, nLutLeaf2, nLutRoot, &R, &G2, pFunc0, pFunc1, pFunc2 );
2085  memcpy( pLut0, &R, sizeof(If_Grp_t) );
2086  memcpy( pLut1, &G, sizeof(If_Grp_t) );
2087  memcpy( pLut2, &G2, sizeof(If_Grp_t) );
2088  return (G.nVars > 0);
2089 }
2090 
2091 
2092 // computes delay of the decomposition
2093 float If_CluDelayMax( If_Grp_t * g, float * pDelays )
2094 {
2095  float Delay = 0.0;
2096  int i;
2097  for ( i = 0; i < g->nVars; i++ )
2098  Delay = Abc_MaxFloat( Delay, pDelays[(int)g->pVars[i]] );
2099  return Delay;
2100 }
2101 
2102 // returns delay of the decomposition; sets area of the cut as its cost
2103 float If_CutDelayLutStruct( If_Man_t * p, If_Cut_t * pCut, char * pStr, float WireDelay )
2104 {
2105  float Delays[CLU_VAR_MAX+2];
2106  int fUsed[CLU_VAR_MAX+2] = {0};
2107  If_Obj_t * pLeaf;
2108  If_Grp_t G1 = {0}, G2 = {0}, G3 = {0};
2109  int nLeaves = If_CutLeaveNum(pCut);
2110  int i, nLutLeaf, nLutRoot;
2111  // mark the cut as user cut
2112 // pCut->fUser = 1;
2113  // quit if parameters are wrong
2114  if ( strlen(pStr) != 2 )
2115  {
2116  printf( "Wrong LUT struct (%s)\n", pStr );
2117  return ABC_INFINITY;
2118  }
2119  nLutLeaf = pStr[0] - '0';
2120  if ( nLutLeaf < 3 || nLutLeaf > 6 )
2121  {
2122  printf( "Leaf size (%d) should belong to {3,4,5,6}.\n", nLutLeaf );
2123  return ABC_INFINITY;
2124  }
2125  nLutRoot = pStr[1] - '0';
2126  if ( nLutRoot < 3 || nLutRoot > 6 )
2127  {
2128  printf( "Root size (%d) should belong to {3,4,5,6}.\n", nLutRoot );
2129  return ABC_INFINITY;
2130  }
2131  if ( nLeaves > nLutLeaf + nLutRoot - 1 )
2132  {
2133  printf( "The cut size (%d) is too large for the LUT structure %d%d.\n", If_CutLeaveNum(pCut), nLutLeaf, nLutRoot );
2134  return ABC_INFINITY;
2135  }
2136 
2137  // remember the delays
2138  If_CutForEachLeaf( p, pCut, pLeaf, i )
2139  Delays[i] = If_ObjCutBest(pLeaf)->Delay;
2140 
2141  // consider easy case
2142  if ( nLeaves <= Abc_MaxInt( nLutLeaf, nLutRoot ) )
2143  {
2144  char * pPerm = If_CutPerm( pCut );
2145  assert( nLeaves <= 6 );
2146  for ( i = 0; i < nLeaves; i++ )
2147  {
2148  pPerm[i] = 1;
2149  G1.pVars[i] = i;
2150  }
2151  G1.nVars = nLeaves;
2152  return 1.0 + If_CluDelayMax( &G1, Delays );
2153  }
2154 
2155  // derive the first group
2156  G1 = If_CluCheck( p, If_CutTruthW(p, pCut), nLeaves, 0, 0, nLutLeaf, nLutRoot, NULL, NULL, NULL, NULL, 1 );
2157  if ( G1.nVars == 0 )
2158  return ABC_INFINITY;
2159 
2160  // compute the delay
2161  Delays[nLeaves] = If_CluDelayMax( &G1, Delays ) + ((WireDelay == 0.0)?1.0:WireDelay);
2162  if ( G2.nVars )
2163  Delays[nLeaves+1] = If_CluDelayMax( &G2, Delays ) + ((WireDelay == 0.0)?1.0:WireDelay);
2164 
2165  // mark used groups
2166  for ( i = 0; i < G1.nVars; i++ )
2167  fUsed[(int)G1.pVars[i]] = 1;
2168  for ( i = 0; i < G2.nVars; i++ )
2169  fUsed[(int)G2.pVars[i]] = 1;
2170  // mark unused groups
2171  assert( G1.nMyu >= 2 && G1.nMyu <= 4 );
2172  if ( G1.nMyu > 2 )
2173  fUsed[(int)G1.pVars[G1.nVars-1]] = 0;
2174  assert( !G2.nVars || (G2.nMyu >= 2 && G2.nMyu <= 4) );
2175  if ( G2.nMyu > 2 )
2176  fUsed[(int)G2.pVars[G2.nVars-1]] = 0;
2177 
2178  // create remaining group
2179  assert( G3.nVars == 0 );
2180  for ( i = 0; i < nLeaves; i++ )
2181  if ( !fUsed[i] )
2182  G3.pVars[(int)G3.nVars++] = i;
2183  G3.pVars[(int)G3.nVars++] = nLeaves;
2184  if ( G2.nVars )
2185  G3.pVars[(int)G3.nVars++] = nLeaves+1;
2186  assert( G1.nVars + G2.nVars + G3.nVars == nLeaves +
2187  (G1.nVars > 0) + (G2.nVars > 0) + (G1.nMyu > 2) + (G2.nMyu > 2) );
2188  // what if both non-disjoint vars are the same???
2189 
2190  pCut->Cost = 2 + (G2.nVars > 0);
2191  return 1.0 + If_CluDelayMax( &G3, Delays );
2192 }
2193 
2194 //#define IF_TRY_NEW
2195 
2196 #ifdef IF_TRY_NEW
2197 static Vec_Mem_t * s_vTtMem = NULL;
2198 static Vec_Mem_t * s_vTtMem2 = NULL;
2199 int If_TtMemCutNum() { return Vec_MemEntryNum(s_vTtMem); }
2200 int If_TtMemCutNum2() { return Vec_MemEntryNum(s_vTtMem2); }
2201 // printf( "Unique TTs = %d. Unique classes = %d. ", If_TtMemCutNum(), If_TtMemCutNum2() );
2202 // printf( "Check2 = %d. Check3 = %d.\n", s_Count2, s_Count3 );
2203 #endif
2204 
2205 /**Function*************************************************************
2206 
2207  Synopsis [Performs additional check.]
2208 
2209  Description []
2210 
2211  SideEffects []
2212 
2213  SeeAlso []
2214 
2215 ***********************************************************************/
2216 int If_CutPerformCheck16( If_Man_t * p, unsigned * pTruth0, int nVars, int nLeaves, char * pStr )
2217 {
2218  unsigned pTruth[IF_MAX_FUNC_LUTSIZE > 5 ? 1 << (IF_MAX_FUNC_LUTSIZE - 5) : 1];
2219  If_Grp_t G1 = {0};//, G3 = {0};
2220  int i, nLutLeaf, nLutLeaf2, nLutRoot, Length;
2221  // stretch the truth table
2222  assert( nVars >= 6 );
2223  memcpy( pTruth, pTruth0, sizeof(word) * Abc_TtWordNum(nVars) );
2224  Abc_TtStretch6( (word *)pTruth, nLeaves, p->pPars->nLutSize );
2225 
2226 #ifdef IF_TRY_NEW
2227  {
2228  word pCopy[1024];
2229  int nWords = Abc_TruthWordNum(nVars);
2230  int iNum;
2231  if ( s_vTtMem == NULL )
2232  {
2233  s_vTtMem = Vec_MemAlloc( Abc_Truth6WordNum(nVars), 12 ); // 32 KB/page for 6-var functions
2234  Vec_MemHashAlloc( s_vTtMem, 10000 );
2235  }
2236  if ( s_vTtMem2 == NULL )
2237  {
2238  s_vTtMem2 = Vec_MemAlloc( Abc_Truth6WordNum(nVars), 12 ); // 32 KB/page for 6-var functions
2239  Vec_MemHashAlloc( s_vTtMem2, 10000 );
2240  }
2241  memcpy( pCopy, pTruth, sizeof(word) * Abc_Truth6WordNum(nVars) );
2242  if ( pCopy[0] & 1 )
2243  for ( i = 0; i < nWords; i++ )
2244  pCopy[i] = ~pCopy[i];
2245  iNum = Vec_MemHashInsert( s_vTtMem, pCopy );
2246  if ( iNum == Vec_MemEntryNum(s_vTtMem) - 1 )
2247  {
2248  int pCanonPerm[16];
2249  char pCanonPermC[16];
2250  Abc_TtCanonicize( pCopy, nVars, pCanonPermC );
2251 // If_CluSemiCanonicize( pCopy, nVars, pCanonPerm );
2252  Vec_MemHashInsert( s_vTtMem2, pCopy );
2253  }
2254  }
2255 #endif
2256 
2257  // if cutmin is disabled, minimize the function
2258  if ( !p->pPars->fCutMin )
2259  nLeaves = Abc_TtMinBase( (word *)pTruth, NULL, nLeaves, nVars );
2260 
2261  // quit if parameters are wrong
2262  Length = strlen(pStr);
2263  if ( Length != 2 && Length != 3 )
2264  {
2265  printf( "Wrong LUT struct (%s)\n", pStr );
2266  return 0;
2267  }
2268  for ( i = 0; i < Length; i++ )
2269  if ( pStr[i] - '0' < 3 || pStr[i] - '0' > 6 )
2270  {
2271  printf( "The LUT size (%d) should belong to {3,4,5,6}.\n", pStr[i] - '0' );
2272  return 0;
2273  }
2274 
2275  nLutLeaf = pStr[0] - '0';
2276  nLutLeaf2 = ( Length == 3 ) ? pStr[1] - '0' : 0;
2277  nLutRoot = pStr[Length-1] - '0';
2278  if ( nLeaves > nLutLeaf - 1 + (nLutLeaf2 ? nLutLeaf2 - 1 : 0) + nLutRoot )
2279  {
2280  printf( "The cut size (%d) is too large for the LUT structure %s.\n", nLeaves, pStr );
2281  return 0;
2282  }
2283  // consider easy case
2284  if ( nLeaves <= Abc_MaxInt( nLutLeaf2, Abc_MaxInt(nLutLeaf, nLutRoot) ) )
2285  return 1;
2286 
2287  // derive the first group
2288  if ( Length == 2 )
2289  G1 = If_CluCheck( p, (word *)pTruth, nLeaves, 0, 0, nLutLeaf, nLutRoot, NULL, NULL, NULL, NULL, 1 );
2290  else
2291  G1 = If_CluCheck3( p, (word *)pTruth, nLeaves, nLutLeaf, nLutLeaf2, nLutRoot, NULL, NULL, NULL, NULL, NULL );
2292 
2293 // if ( G1.nVars > 0 )
2294 // If_CluPrintGroup( &G1 );
2295 
2296  return (int)(G1.nVars > 0);
2297 }
2298 
2299 
2300 // testing procedure
2301 void If_CluTest()
2302 {
2303 // word t = 0xff00f0f0ccccaaaa;
2304 // word t = 0xfedcba9876543210;
2305 // word t = 0xec64000000000000;
2306 // word t = 0x0100200000000001;
2307 // word t2[4] = { 0x0000800080008000, 0x8000000000008000, 0x8000000080008000, 0x0000000080008000 };
2308 // word t = 0x07770FFF07770FFF;
2309 // word t = 0x002000D000D00020;
2310 // word t = 0x000F000E000F000F;
2311 // word t = 0xF7FFF7F7F7F7F7F7;
2312 // word t = 0x0234AFDE23400BCE;
2313 // word t = 0x0080008880A088FF;
2314 // word s = t;
2315 // word t = 0xFFBBBBFFF0B0B0F0;
2316  word t = ABC_CONST(0x6DD9926D962D6996);
2317  int nVars = 6;
2318  int nLutLeaf = 4;
2319  int nLutLeaf2 = 4;
2320  int nLutRoot = 4;
2321 /*
2322  word t2[2] = { 0x7f807f807f80807f, 0x7f807f807f807f80 };
2323  int nVars = 7;
2324  int nLutLeaf = 3;
2325  int nLutLeaf2 = 3;
2326  int nLutRoot = 3;
2327 */
2328 
2329  If_Grp_t G;
2330  If_Grp_t G2, R;
2331  word Func0, Func1, Func2;
2332 
2333 
2334  return;
2335 
2336 /*
2337  int pCanonPerm[CLU_VAR_MAX];
2338  int uCanonPhase;
2339 
2340  Kit_DsdPrintFromTruth( (unsigned*)&s, nVars ); printf( "\n" );
2341  uCanonPhase = If_CluSemiCanonicize( &s, nVars, pCanonPerm );
2342  Kit_DsdPrintFromTruth( (unsigned*)&s, nVars ); printf( "\n" );
2343 
2344  If_CluSemiCanonicizeVerify( &s, &t, nVars, pCanonPerm, uCanonPhase );
2345 */
2346 
2347  Kit_DsdPrintFromTruth( (unsigned*)&t, nVars ); printf( "\n" );
2348  G = If_CluCheck3( NULL, &t, nVars, nLutLeaf, nLutLeaf2, nLutRoot, &R, &G2, &Func0, &Func1, &Func2 );
2349  If_CluPrintGroup( &G );
2350  If_CluPrintGroup( &G2 );
2351  If_CluPrintGroup( &R );
2352 
2353 // If_CluVerify3( &t, nVars, &G, &G2, &R, Func1, Func2, Func0 );
2354 
2355  return;
2356 
2357 // If_CutPerformCheck07( NULL, (unsigned *)&t, 6, 6, NULL );
2358 // return;
2359 
2360 // Kit_DsdPrintFromTruth( (unsigned*)&t, nVars ); printf( "\n" );
2361 // G = If_CluCheck( NULL, &t, nVars, 0, nLutLeaf, nLutRoot, NULL, NULL, NULL, NULL, 0 );
2362 // If_CluPrintGroup( &G );
2363 }
2364 
2365 
2366 
2367 
2368 ////////////////////////////////////////////////////////////////////////
2369 /// END OF FILE ///
2370 ////////////////////////////////////////////////////////////////////////
2371 
2372 
2373 ABC_NAMESPACE_IMPL_END
2374 
memset
char * memset()
If_Man_t_::vObjs
Vec_Ptr_t * vObjs
Definition: if.h:189
Vec_Ptr_t
typedefABC_NAMESPACE_HEADER_START struct Vec_Ptr_t_ Vec_Ptr_t
INCLUDES ///.
Definition: vecPtr.h:42
If_CluEqual
static int If_CluEqual(word *pOut, word *pIn, int nVars)
Definition: ifDec16.c:344
If_CluVerify3
void If_CluVerify3(word *pF, int nVars, If_Grp_t *g, If_Grp_t *g2, If_Grp_t *r, word BStruth, word BStruth2, word FStruth)
Definition: ifDec16.c:673
Abc_TtMinBase
static int Abc_TtMinBase(word *pTruth, int *pVars, int nVars, int nVarsAll)
Definition: utilTruth.h:1395
If_Par_t_::nLutSize
int nLutSize
Definition: if.h:103
If_Hte_t_::pNext
If_Hte_t * pNext
Definition: ifDec16.c:49
If_CutPerformCheck16
int If_CutPerformCheck16(If_Man_t *p, unsigned *pTruth0, int nVars, int nLeaves, char *pStr)
Definition: ifDec16.c:2216
If_CluCheckDecInU
int If_CluCheckDecInU(word t, int nVars)
Definition: ifDec16.c:1818
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
If_CluCheckDecOut
int If_CluCheckDecOut(word t, int nVars)
Definition: ifDec16.c:1840
If_Hte_t_::pTruth
word pTruth[1]
Definition: ifDec16.c:52
If_CluAdjustBig
static void If_CluAdjustBig(word *pF, int nVarsCur, int nVarsMax)
Definition: ifDec16.c:390
If_CluSwapAdjacent
static void If_CluSwapAdjacent(word *pOut, word *pIn, int iVar, int nVars)
Definition: ifDec16.c:402
If_CluHashPrintStats
void If_CluHashPrintStats(If_Man_t *p, int t)
Definition: ifDec16.c:164
If_Obj_t_
Definition: if.h:303
If_CluCheck
If_Grp_t If_CluCheck(If_Man_t *p, word *pTruth0, int nVars, int iVarStart, int iVarStop, int nLutLeaf, int nLutRoot, If_Grp_t *pR, word *pFunc0, word *pFunc1, word *pLeftOver, int fHashing)
Definition: ifDec16.c:1553
If_CluTest
void If_CluTest()
Definition: ifDec16.c:2301
If_Cut_t_
Definition: if.h:275
Vec_MemHashAlloc
static void Vec_MemHashAlloc(Vec_Mem_t *p, int nTableSize)
Definition: vecMem.h:305
s_Count2
int s_Count2
Definition: ifDec16.c:79
Abc_Truth6WordNum
static int Abc_Truth6WordNum(int nVars)
Definition: abc_global.h:257
If_CutForEachLeaf
#define If_CutForEachLeaf(p, pCut, pLeaf, i)
Definition: if.h:474
If_CutLeaveNum
static int If_CutLeaveNum(If_Cut_t *pCut)
Definition: if.h:390
If_CutPerm
static char * If_CutPerm(If_Cut_t *pCut)
Definition: if.h:397
If_CluHashTableCheck
void If_CluHashTableCheck(If_Man_t *p)
Definition: ifDec16.c:144
If_CluReverseOrder
void If_CluReverseOrder(word *pTruth, int nVars, int *V2P, int *P2V, int iVarStart)
Definition: ifDec16.c:800
Vec_Mem_t
typedefABC_NAMESPACE_IMPL_START struct Vec_Mem_t_ Vec_Mem_t
DECLARATIONS ///.
Definition: utilMem.c:35
memcpy
char * memcpy()
Vec_MemEntryNum
static int Vec_MemEntryNum(Vec_Mem_t *p)
Definition: vecMem.h:151
Vec_PtrPush
static void Vec_PtrPush(Vec_Ptr_t *p, void *Entry)
Definition: vecPtr.h:606
Vec_IntSetEntry
static void Vec_IntSetEntry(Vec_Int_t *p, int i, int Entry)
Definition: bblif.c:418
If_CluSemiCanonicizeVerify
void If_CluSemiCanonicizeVerify(word *pTruth, word *pTruth0, int nVars, int *pCanonPerm, unsigned uCanonPhase)
Definition: ifDec16.c:539
If_ObjCutBest
static If_Cut_t * If_ObjCutBest(If_Obj_t *pObj)
Definition: if.h:401
PMasks
static word PMasks[5][3]
Definition: ifDec16.c:56
If_CluCheck3
If_Grp_t If_CluCheck3(If_Man_t *p, word *pTruth0, int nVars, int nLutLeaf, int nLutLeaf2, int nLutRoot, If_Grp_t *pR, If_Grp_t *pG2, word *pFunc0, word *pFunc1, word *pFunc2)
Definition: ifDec16.c:1909
If_CluHashLookup
unsigned * If_CluHashLookup(If_Man_t *p, word *pTruth, int t)
Definition: ifDec16.c:233
Abc_TruthWordNum
static int Abc_TruthWordNum(int nVars)
Definition: abc_global.h:256
CLU_UNUSED
#define CLU_UNUSED
Definition: ifDec16.c:34
Abc_Tt6Cofactor0
static word Abc_Tt6Cofactor0(word t, int iVar)
Definition: utilTruth.h:370
Abc_MaxInt
static int Abc_MaxInt(int a, int b)
Definition: abc_global.h:238
If_CluCountCofs4
int If_CluCountCofs4(word *pF, int nVars, int nBSsize, word pCofs[6][CLU_WRD_MAX/4])
Definition: ifDec16.c:978
If_CluReverseOrder_old
void If_CluReverseOrder_old(word *pF, int nVars, int *V2P, int *P2V, int iVarStart)
Definition: ifDec16.c:864
Vec_PtrSize
static int Vec_PtrSize(Vec_Ptr_t *p)
Definition: vecPtr.h:295
If_CluCheckExt
int If_CluCheckExt(void *pMan, word *pTruth, int nVars, int nLutLeaf, int nLutRoot, char *pLut0, char *pLut1, word *pFunc0, word *pFunc1)
Definition: ifDec16.c:2066
If_CluClear
static void If_CluClear(word *pIn, int nVars)
Definition: ifDec16.c:326
If_CluCheckDecOutU
int If_CluCheckDecOutU(word t, int nVars)
Definition: ifDec16.c:1853
nWords
int nWords
Definition: abcNpn.c:127
If_CluHashFindMedian
int If_CluHashFindMedian(If_Man_t *p, int t)
Definition: ifDec16.c:180
Abc_MaxFloat
static float Abc_MaxFloat(float a, float b)
Definition: abc_global.h:243
Kit_DsdPrintFromTruth
void Kit_DsdPrintFromTruth(unsigned *pTruth, int nVars)
Definition: kitDsd.c:490
If_Par_t_::fEnableCheck75u
int fEnableCheck75u
Definition: if.h:132
If_CluSemiCanonicize
unsigned If_CluSemiCanonicize(word *pTruth, int nVars, int *pCanonPerm)
Definition: ifDec16.c:485
If_CluWordNum
static int If_CluWordNum(int nVars)
Definition: ifDec16.c:130
If_CluAnd
static void If_CluAnd(word *pRes, word *pIn1, word *pIn2, int nVars)
Definition: ifDec16.c:352
If_Cut_t_::Cost
unsigned Cost
Definition: if.h:284
Mem_FixedStart
Mem_Fixed_t * Mem_FixedStart(int nEntrySize)
FUNCTION DEFINITIONS ///.
Definition: mem.c:100
If_CutTruthW
static word * If_CutTruthW(If_Man_t *p, If_Cut_t *pCut)
Definition: if.h:421
Vec_MemAlloc
static Vec_Mem_t * Vec_MemAlloc(int nCap)
FUNCTION DEFINITIONS ///.
Definition: utilMem.c:70
If_Par_t_::fEnableCheck75
int fEnableCheck75
Definition: if.h:131
Abc_MinInt
static int Abc_MinInt(int a, int b)
Definition: abc_global.h:239
If_CluSuppIsMinBase
static int If_CluSuppIsMinBase(int Supp)
Definition: ifDec16.c:1466
Vec_IntStart
static Vec_Int_t * Vec_IntStart(int nSize)
Definition: bblif.c:172
If_CluComposeLut
static void If_CluComposeLut(int nVars, If_Grp_t *g, word *t, word f[6][CLU_WRD_MAX], word *r)
Definition: ifDec16.c:623
If_Man_t_::pHashTable
void ** pHashTable[2]
Definition: if.h:268
If_CluMinimumBase
int If_CluMinimumBase(word *t, int *pSupp, int nVarsAll, int *pnVars)
Definition: ifDec16.c:1532
If_CluCopy
static void If_CluCopy(word *pOut, word *pIn, int nVars)
Definition: ifDec16.c:338
If_CluOr
static void If_CluOr(word *pRes, word *pIn1, word *pIn2, int nVars)
Definition: ifDec16.c:364
If_CluTruthShrink
static void If_CluTruthShrink(word *pF, int nVars, int nVarsAll, unsigned Phase)
Definition: ifDec16.c:1511
If_Man_t_::nTableSize
int nTableSize[2]
Definition: if.h:266
Abc_Tt6Cofactor1
static word Abc_Tt6Cofactor1(word t, int iVar)
Definition: utilTruth.h:375
If_CluDecUsingCofs
If_Grp_t If_CluDecUsingCofs(word *pTruth, int nVars, int nLutLeaf)
Definition: ifDec16.c:1112
If_Grp_t_::nMyu
char nMyu
Definition: ifDec16.c:41
Vec_IntAddToEntry
static void Vec_IntAddToEntry(Vec_Int_t *p, int i, int Addition)
Definition: bblif.c:302
If_CluSharp
static void If_CluSharp(word *pRes, word *pIn1, word *pIn2, int nVars)
Definition: ifDec16.c:358
If_CluPrimeCudd
unsigned int If_CluPrimeCudd(unsigned int p)
Definition: ifDec16.c:104
If_CluSupportSize
int If_CluSupportSize(word *t, int nVars)
Definition: ifDec16.c:1503
TruthAll
static word TruthAll[CLU_VAR_MAX][CLU_WRD_MAX]
Definition: ifDec16.c:72
If_CluPrintConfig
void If_CluPrintConfig(int nVars, If_Grp_t *g, If_Grp_t *r, word BStruth, word *pFStruth)
Definition: ifDec16.c:590
If_Man_t_
Definition: if.h:180
If_CutDelayLutStruct
float If_CutDelayLutStruct(If_Man_t *p, If_Cut_t *pCut, char *pStr, float WireDelay)
Definition: ifDec16.c:2103
Vec_IntEntry
static int Vec_IntEntry(Vec_Int_t *p, int i)
Definition: bblif.c:268
If_CluPrintGroup
void If_CluPrintGroup(If_Grp_t *g)
Definition: ifDec16.c:580
word
unsigned __int64 word
DECLARATIONS ///.
Definition: kitPerm.c:36
ABC_NAMESPACE_IMPL_END
#define ABC_NAMESPACE_IMPL_END
Definition: abc_global.h:108
CLU_VAR_MAX
#define CLU_VAR_MAX
DECLARATIONS ///.
Definition: ifDec16.c:31
if
if(last==0)
Definition: sparse_int.h:34
Abc_TtStretch6
static void Abc_TtStretch6(word *pInOut, int nVarS, int nVarB)
Definition: utilTruth.h:693
If_CluHasVar
static int If_CluHasVar(word *t, int nVars, int iVar)
Definition: ifDec16.c:1470
memcmp
int memcmp()
IF_MAX_FUNC_LUTSIZE
#define IF_MAX_FUNC_LUTSIZE
Definition: if.h:54
If_CluCheckDecInAny
int If_CluCheckDecInAny(word t, int nVars)
Definition: ifDec16.c:1767
If_CluDelayMax
float If_CluDelayMax(If_Grp_t *g, float *pDelays)
Definition: ifDec16.c:2093
Counter
static int Counter
Definition: extraBddMisc.c:1877
Mem_FixedEntryRecycle
void Mem_FixedEntryRecycle(Mem_Fixed_t *p, char *pEntry)
Definition: mem.c:219
If_CluFill
static void If_CluFill(word *pIn, int nVars)
Definition: ifDec16.c:332
If_Man_t_::pMemEntries
Mem_Fixed_t * pMemEntries
Definition: if.h:269
If_CluCofactors
void If_CluCofactors(word *pF, int nVars, int iVar, word *pCof0, word *pCof1)
Definition: ifDec16.c:1015
pPerm
static int pPerm[13719]
Definition: rwrTemp.c:32
Truth6
static word Truth6[6]
Definition: ifDec16.c:64
If_Hte_t_::Group
unsigned Group
Definition: ifDec16.c:50
If_CluCheckExt3
int If_CluCheckExt3(void *pMan, word *pTruth, int nVars, int nLutLeaf, int nLutLeaf2, int nLutRoot, char *pLut0, char *pLut1, char *pLut2, word *pFunc0, word *pFunc1, word *pFunc2)
Definition: ifDec16.c:2079
ABC_NAMESPACE_IMPL_START
#define ABC_NAMESPACE_IMPL_START
Definition: abc_global.h:107
If_CluCheckPerm
void If_CluCheckPerm(word *pTruth, word *pF, int nVars, int *V2P, int *P2V)
Definition: ifDec16.c:1451
If_CluCountOnesInCofs
void If_CluCountOnesInCofs(word *pTruth, int nVars, int *pStore)
Definition: ifDec16.c:465
If_CluDeriveNonDisjoint
word If_CluDeriveNonDisjoint(word *pF, int nVars, int *V2P, int *P2V, If_Grp_t *g, If_Grp_t *r)
Definition: ifDec16.c:1237
Truth
static ABC_NAMESPACE_IMPL_START word Truth[8]
DECLARATIONS ///.
Definition: giaShrink6.c:32
If_Man_t_::pPars
If_Par_t * pPars
Definition: if.h:184
If_Grp_t_::pVars
char pVars[CLU_VAR_MAX]
Definition: ifDec16.c:42
If_CutPerformCheck45
int If_CutPerformCheck45(If_Man_t *p, unsigned *pTruth, int nVars, int nLeaves, char *pStr)
Definition: ifDec16.c:1865
If_CluMoveGroupToMsb
void If_CluMoveGroupToMsb(word *pF, int nVars, int *V2P, int *P2V, If_Grp_t *g)
Definition: ifDec16.c:855
CLU_MEM_MAX
#define CLU_MEM_MAX
Definition: ifDec16.c:33
Vec_PtrAlloc
static Vec_Ptr_t * Vec_PtrAlloc(int nCap)
FUNCTION DEFINITIONS ///.
Definition: vecPtr.h:83
Abc_TtWordNum
static int Abc_TtWordNum(int nVars)
Definition: utilTruth.h:169
If_CluChangePhase
void If_CluChangePhase(word *pF, int nVars, int iVar)
Definition: ifDec16.c:439
If_CluDeriveDisjoint4
void If_CluDeriveDisjoint4(word *pF, int nVars, int *V2P, int *P2V, If_Grp_t *g, If_Grp_t *r, word *pTruth0, word *pTruth1)
Definition: ifDec16.c:1208
ABC_CONST
#define ABC_CONST(number)
PARAMETERS ///.
Definition: abc_global.h:206
If_CluDetectSpecialCaseCofs
int If_CluDetectSpecialCaseCofs(word *pF, int nVars, int iVar)
Definition: ifDec16.c:1046
If_CutPerformCheck54
int If_CutPerformCheck54(If_Man_t *p, unsigned *pTruth, int nVars, int nLeaves, char *pStr)
Definition: ifDec16.c:1886
If_CluInitTruthTables
void If_CluInitTruthTables()
Definition: ifDec16.c:606
If_CluAdjust
static word If_CluAdjust(word t, int nVars)
Definition: ifDec16.c:370
ABC_CALLOC
#define ABC_CALLOC(type, num)
Definition: abc_global.h:230
If_CluDeriveDisjoint
word If_CluDeriveDisjoint(word *pF, int nVars, int *V2P, int *P2V, If_Grp_t *g, If_Grp_t *r)
Definition: ifDec16.c:1183
Minisat::Var
int Var
Definition: SolverTypes.h:42
Abc_TtCanonicize
unsigned Abc_TtCanonicize(word *pTruth, int nVars, char *pCanonPerm)
FUNCTION DECLARATIONS ///.
Definition: dauCanon.c:895
If_Grp_t_::nVars
char nVars
Definition: ifDec16.c:40
If_CluSupport
static int If_CluSupport(word *t, int nVars)
Definition: ifDec16.c:1495
If_CluCountOnes
static int If_CluCountOnes(word t)
Definition: ifDec16.c:134
If_CluUns2Grp
static void If_CluUns2Grp(unsigned Group, If_Grp_t *pG)
Definition: ifDec16.c:96
If_CluVerify
void If_CluVerify(word *pF, int nVars, If_Grp_t *g, If_Grp_t *r, word BStruth, word *pFStruth)
Definition: ifDec16.c:641
If_CluHashKey
int If_CluHashKey(word *pTruth, int nWords, int Size)
Definition: ifDec16.c:214
If_Par_t_::fCutMin
int fCutMin
Definition: if.h:120
If_CluFindGroup
If_Grp_t If_CluFindGroup(word *pF, int nVars, int iVarStart, int iVarStop, int *V2P, int *P2V, int nBSsize, int fDisjoint)
Definition: ifDec16.c:1306
Vec_MemHashInsert
static int Vec_MemHashInsert(Vec_Mem_t *p, word *pEntry)
Definition: vecMem.h:351
If_CluMoveVar2
void If_CluMoveVar2(word *pF, int nVars, int *Var2Pla, int *Pla2Var, int v, int p)
Definition: ifDec16.c:812
ABC_INFINITY
#define ABC_INFINITY
MACRO DEFINITIONS ///.
Definition: abc_global.h:216
If_CluMoveVar
void If_CluMoveVar(word *pF, int nVars, int *Var2Pla, int *Pla2Var, int v, int p)
Definition: ifDec16.c:818
assert
#define assert(ex)
Definition: util_old.h:213
If_Par_t_::nCutsMax
int nCutsMax
Definition: if.h:104
strlen
int strlen()
If_Hte_t_::Counter
unsigned Counter
Definition: ifDec16.c:51
If_Grp_t_
Definition: ifDec16.c:38
s_vTtMem
static Vec_Mem_t * s_vTtMem
Definition: giaMf.c:117
If_Man_t_::nTableEntries
int nTableEntries[2]
Definition: if.h:267
If_CluCheckGroup
void If_CluCheckGroup(word *pTruth, int nVars, If_Grp_t *g)
Definition: ifDec16.c:1420
Extra_PrintBinary
void Extra_PrintBinary(FILE *pFile, unsigned Sign[], int nBits)
Definition: extraUtilFile.c:497
If_CluCheckNonDisjointGroup
int If_CluCheckNonDisjointGroup(word *pF, int nVars, int *V2P, int *P2V, If_Grp_t *g)
Definition: ifDec16.c:1278
Vec_IntFree
static void Vec_IntFree(Vec_Int_t *p)
Definition: bblif.c:235
If_Par_t_::nStructType
int nStructType
Definition: if.h:112
Vec_PtrForEachEntry
#define Vec_PtrForEachEntry(Type, vVec, pEntry, i)
MACRO DEFINITIONS ///.
Definition: vecPtr.h:55
CLU_WRD_MAX
#define CLU_WRD_MAX
Definition: ifDec16.c:32
If_CluGrp2Uns
static unsigned If_CluGrp2Uns(If_Grp_t *pG)
FUNCTION DEFINITIONS ///.
Definition: ifDec16.c:86
Mem_FixedEntryFetch
char * Mem_FixedEntryFetch(Mem_Fixed_t *p)
Definition: mem.c:168
If_Cut_t_::Delay
float Delay
Definition: if.h:280
If_Hte_t_
Definition: ifDec16.c:47
If_CluCountCofs
int If_CluCountCofs(word *pF, int nVars, int nBSsize, int iShift, word pCofs[3][CLU_WRD_MAX/4])
Definition: ifDec16.c:903
If_CluSwapVars
void If_CluSwapVars(word *pTruth, int nVars, int *V2P, int *P2V, int iVar, int jVar)
Definition: ifDec16.c:723
s_Count3
int s_Count3
Definition: ifDec16.c:80
If_CluCheckDecIn
int If_CluCheckDecIn(word t, int nVars)
Definition: ifDec16.c:1792
Vec_PtrFree
static void Vec_PtrFree(Vec_Ptr_t *p)
Definition: vecPtr.h:223