abc-master
 All Data Structures Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros
luckyFast16.c
Go to the documentation of this file.
1 /**CFile****************************************************************
2 
3  FileName [luckyFast16.c]
4 
5  SystemName [ABC: Logic synthesis and verification system.]
6 
7  PackageName [Semi-canonical form computation package.]
8 
9  Synopsis [Truth table minimization procedures for up to 16 vars.]
10 
11  Author [Jake]
12 
13  Date [Started - September 2012]
14 
15 ***********************************************************************/
16 
17 #include "luckyInt.h"
18 //#define LUCKY_VERIFY
19 
21 
22 static word SFmask[5][4] = {
23  {ABC_CONST(0x8888888888888888),ABC_CONST(0x4444444444444444),ABC_CONST(0x2222222222222222),ABC_CONST(0x1111111111111111)},
24  {ABC_CONST(0xC0C0C0C0C0C0C0C0),ABC_CONST(0x3030303030303030),ABC_CONST(0x0C0C0C0C0C0C0C0C),ABC_CONST(0x0303030303030303)},
25  {ABC_CONST(0xF000F000F000F000),ABC_CONST(0x0F000F000F000F00),ABC_CONST(0x00F000F000F000F0),ABC_CONST(0x000F000F000F000F)},
26  {ABC_CONST(0xFF000000FF000000),ABC_CONST(0x00FF000000FF0000),ABC_CONST(0x0000FF000000FF00),ABC_CONST(0x000000FF000000FF)},
27  {ABC_CONST(0xFFFF000000000000),ABC_CONST(0x0000FFFF00000000),ABC_CONST(0x00000000FFFF0000),ABC_CONST(0x000000000000FFFF)}
28 };
29 
30 // we need next two functions only for verification of lucky method in debugging mode
31 void swapAndFlip(word* pAfter, int nVars, int iVarInPosition, int jVar, char * pCanonPerm, unsigned* pUCanonPhase)
32 {
33  int Temp;
34  swap_ij(pAfter, nVars, iVarInPosition, jVar);
35 
36  Temp = pCanonPerm[iVarInPosition];
37  pCanonPerm[iVarInPosition] = pCanonPerm[jVar];
38  pCanonPerm[jVar] = Temp;
39 
40  if ( ((*pUCanonPhase & (1 << iVarInPosition)) > 0) != ((*pUCanonPhase & (1 << jVar)) > 0) )
41  {
42  *pUCanonPhase ^= (1 << iVarInPosition);
43  *pUCanonPhase ^= (1 << jVar);
44  }
45  if((*pUCanonPhase>>iVarInPosition) & 1)
46  Kit_TruthChangePhase_64bit( pAfter, nVars, iVarInPosition );
47 
48 }
49 int luckyCheck(word* pAfter, word* pBefore, int nVars, char * pCanonPerm, unsigned uCanonPhase)
50 {
51  int i,j;
52  char tempChar;
53  for(j=0;j<nVars;j++)
54  {
55  tempChar = 'a'+ j;
56  for(i=j;i<nVars;i++)
57  {
58  if(tempChar != pCanonPerm[i])
59  continue;
60  swapAndFlip(pAfter , nVars, j, i, pCanonPerm, &uCanonPhase);
61  break;
62  }
63  }
64  if((uCanonPhase>>nVars) & 1)
65  Kit_TruthNot_64bit(pAfter, nVars );
66  if(memcmp(pAfter, pBefore, Kit_TruthWordNum_64bit( nVars )*sizeof(word)) == 0)
67  return 0;
68  else
69  return 1;
70 }
71 
72 ////////////////////////////////////lessThen5/////////////////////////////////////////////////////////////////////////////////////////////
73 
74 // there are 4 parts in every block to compare and rearrange - quoters(0Q,1Q,2Q,3Q)
75 //updataInfo updates CanonPerm and CanonPhase based on what quoter in position iQ and jQ
76 void updataInfo(int iQ, int jQ, int iVar, char * pCanonPerm, unsigned* pCanonPhase)
77 {
78  *pCanonPhase = adjustInfoAfterSwap(pCanonPerm, *pCanonPhase, iVar, ((abs(iQ-jQ)-1)<<2) + iQ );
79 
80 }
81 
82 // returns the first shift from the left in word x that has One bit in it.
83 // blockSize = ShiftSize/4
84 int firstShiftWithOneBit(word x, int blockSize)
85 {
86  int n = 0;
87  if(blockSize == 16){ return 0;}
88  if (x >= ABC_CONST(0x0000000100000000)) {n = n + 32; x = x >> 32;}
89  if(blockSize == 8){ return (64-n)/32;}
90  if (x >= ABC_CONST(0x0000000000010000)) {n = n + 16; x = x >> 16;}
91  if(blockSize == 4){ return (64-n)/16;}
92  if (x >= ABC_CONST(0x0000000000000100)) {n = n + 8; x = x >> 8;}
93  if(blockSize == 2){ return (64-n)/8;}
94  if (x >= ABC_CONST(0x0000000000000010)) {n = n + 4; x = x >> 4;}
95  return (64-n)/4;
96 
97 }
98 
99 // It rearranges InOut (swaps and flips through rearrangement of quoters)
100 // It updates Info at the end
101 void arrangeQuoters_superFast_lessThen5(word* pInOut, int start, int iQ, int jQ, int kQ, int lQ, int iVar, int nWords, char * pCanonPerm, unsigned* pCanonPhase)
102 {
103  int i, blockSize = 1<<iVar;
104 // printf("in arrangeQuoters_superFast_lessThen5\n");
105 // printf("start = %d, iQ = %d,jQ = %d,kQ = %d,lQ = %d, iVar = %d, nWords = %d\n", start, iQ, jQ, kQ , lQ, iVar, nWords);
106  for(i=start;i>=0;i--)
107  {
108  assert( iQ*blockSize < 64 );
109  assert( jQ*blockSize < 64 );
110  assert( kQ*blockSize < 64 );
111  assert( lQ*blockSize < 64 );
112  assert( 3*blockSize < 64 );
113  pInOut[i] = (pInOut[i] & SFmask[iVar][iQ])<<(iQ*blockSize) |
114  (((pInOut[i] & SFmask[iVar][jQ])<<(jQ*blockSize))>>blockSize) |
115  (((pInOut[i] & SFmask[iVar][kQ])<<(kQ*blockSize))>>2*blockSize) |
116  (((pInOut[i] & SFmask[iVar][lQ])<<(lQ*blockSize))>>3*blockSize);
117  }
118  updataInfo(iQ, jQ, iVar, pCanonPerm, pCanonPhase);
119 // printf("out arrangeQuoters_superFast_lessThen5\n");
120 
121 }
122 // static word SFmask[5][4] = {
123 // {0x8888888888888888,0x4444444444444444,0x2222222222222222,0x1111111111111111},
124 // {0xC0C0C0C0C0C0C0C0,0x3030303030303030,0x0C0C0C0C0C0C0C0C,0x0303030303030303},
125 // {0xF000F000F000F000,0x0F000F000F000F00,0x00F000F000F000F0,0x000F000F000F000F},
126 // {0xFF000000FF000000,0x00FF000000FF0000,0x0000FF000000FF00,0x000000FF000000FF},
127 // {0xFFFF000000000000,0x0000FFFF00000000,0x00000000FFFF0000,0x000000000000FFFF}
128 // };
129 //It compares 0Q and 3Q and returns 0 if 0Q is smaller then 3Q ( comparison starts at highest bit) and visa versa
130 // DifStart contains the information about the first different bit in 0Q and 3Q
131 int minTemp0_fast(word* pInOut, int iVar, int nWords, int* pDifStart)
132 {
133  int i, blockSize = 1<<iVar;
134  word temp;
135  for(i=nWords - 1; i>=0; i--)
136  {
137  assert( 3*blockSize < 64 );
138  temp = ((pInOut[i] & SFmask[iVar][0])) ^ ((pInOut[i] & SFmask[iVar][3])<<(3*blockSize));
139  if( temp == 0)
140  continue;
141  else
142  {
143  *pDifStart = i*100 + 20 - firstShiftWithOneBit(temp, blockSize);
144  if( ((pInOut[i] & SFmask[iVar][0])) < ((pInOut[i] & SFmask[iVar][3])<<(3*blockSize)) )
145  return 0;
146  else
147  return 3;
148  }
149  }
150  *pDifStart=0;
151  return 0;
152 
153 }
154 
155 //It compares 1Q and 2Q and returns 1 if 1Q is smaller then 2Q ( comparison starts at highest bit) and visa versa
156 // DifStart contains the information about the first different bit in 1Q and 2Q
157 int minTemp1_fast(word* pInOut, int iVar, int nWords, int* pDifStart)
158 {
159  int i, blockSize = 1<<iVar;
160  word temp;
161  for(i=nWords - 1; i>=0; i--)
162  {
163  assert( 2*blockSize < 64 );
164  temp = ((pInOut[i] & SFmask[iVar][1])<<(blockSize)) ^ ((pInOut[i] & SFmask[iVar][2])<<(2*blockSize));
165  if( temp == 0)
166  continue;
167  else
168  {
169  *pDifStart = i*100 + 20 - firstShiftWithOneBit(temp, blockSize);
170  if( ((pInOut[i] & SFmask[iVar][1])<<(blockSize)) < ((pInOut[i] & SFmask[iVar][2])<<(2*blockSize)) )
171  return 1;
172  else
173  return 2;
174  }
175  }
176  *pDifStart=0;
177  return 1;
178 }
179 
180 //It compares iQ and jQ and returns 0 if iQ is smaller then jQ ( comparison starts at highest bit) and 1 if jQ is
181 // DifStart contains the information about the first different bit in iQ and jQ
182 int minTemp2_fast(word* pInOut, int iVar, int iQ, int jQ, int nWords, int* pDifStart)
183 {
184  int i, blockSize = 1<<iVar;
185  word temp;
186  for(i=nWords - 1; i>=0; i--)
187  {
188  assert( jQ*blockSize < 64 );
189  temp = ((pInOut[i] & SFmask[iVar][iQ])<<(iQ*blockSize)) ^ ((pInOut[i] & SFmask[iVar][jQ])<<(jQ*blockSize));
190  if( temp == 0)
191  continue;
192  else
193  {
194  *pDifStart = i*100 + 20 - firstShiftWithOneBit(temp, blockSize);
195  if( ((pInOut[i] & SFmask[iVar][iQ])<<(iQ*blockSize)) <= ((pInOut[i] & SFmask[iVar][jQ])<<(jQ*blockSize)) )
196  return 0;
197  else
198  return 1;
199  }
200  }
201  *pDifStart=0;
202  return 0;
203 }
204 // same as minTemp2_fast but this one has a start position
205 int minTemp3_fast(word* pInOut, int iVar, int start, int finish, int iQ, int jQ, int* pDifStart)
206 {
207  int i, blockSize = 1<<iVar;
208  word temp;
209  for(i=start; i>=finish; i--)
210  {
211  assert( jQ*blockSize < 64 );
212  temp = ((pInOut[i] & SFmask[iVar][iQ])<<(iQ*blockSize)) ^ ((pInOut[i] & SFmask[iVar][jQ])<<(jQ*blockSize));
213  if( temp == 0)
214  continue;
215  else
216  {
217  *pDifStart = i*100 + 20 - firstShiftWithOneBit(temp, blockSize);
218  if( ((pInOut[i] & SFmask[iVar][iQ])<<(iQ*blockSize)) <= ((pInOut[i] & SFmask[iVar][jQ])<<(jQ*blockSize)) )
219  return 0;
220  else
221  return 1;
222  }
223  }
224  *pDifStart=0;
225  return 0;
226 }
227 
228 // It considers all swap and flip possibilities of iVar and iVar+1 and switches InOut to a minimal of them
229 void minimalSwapAndFlipIVar_superFast_lessThen5(word* pInOut, int iVar, int nWords, char * pCanonPerm, unsigned* pCanonPhase)
230 {
231  int min1, min2, DifStart0, DifStart1, DifStartMin, DifStart4=0;
232  int M[2];
233  M[0] = minTemp0_fast(pInOut, iVar, nWords, &DifStart0); // 0, 3
234  M[1] = minTemp1_fast(pInOut, iVar, nWords, &DifStart1); // 1, 2
235  min1 = minTemp2_fast(pInOut, iVar, M[0], M[1], nWords, &DifStartMin);
236 // printf("\nDifStart0 = %d, DifStart1 = %d, DifStartMin = %d\n",DifStart0, DifStart1, DifStartMin);
237 // printf("M[0] = %d, M[1] = %d, min1 = %d\n", M[0], M[1], min1);
238  if(DifStart0 != DifStart1)
239  {
240 // printf("if\n");
241  if( DifStartMin>=DifStart1 && DifStartMin>=DifStart0 )
242  arrangeQuoters_superFast_lessThen5(pInOut, DifStartMin/100, M[min1], M[(min1+1)&1], 3 - M[(min1+1)&1], 3 - M[min1], iVar, nWords, pCanonPerm, pCanonPhase);
243  else if( DifStart0 > DifStart1)
244  arrangeQuoters_superFast_lessThen5(pInOut,luckyMax(DifStartMin/100, DifStart0/100), M[0], M[1], 3 - M[1], 3 - M[0], iVar, nWords, pCanonPerm, pCanonPhase);
245  else
246  arrangeQuoters_superFast_lessThen5(pInOut,luckyMax(DifStartMin/100, DifStart1/100), M[1], M[0], 3 - M[0], 3 - M[1], iVar, nWords, pCanonPerm, pCanonPhase);
247  }
248  else
249  {
250 // printf("else\n");
251  if(DifStartMin>=DifStart0)
252  arrangeQuoters_superFast_lessThen5(pInOut, DifStartMin/100, M[min1], M[(min1+1)&1], 3 - M[(min1+1)&1], 3 - M[min1], iVar, nWords, pCanonPerm, pCanonPhase);
253  else
254  {
255  min2 = minTemp3_fast(pInOut, iVar, DifStart0/100, DifStartMin/100, 3-M[0], 3-M[1], &DifStart4); // no reuse DifStart1 because DifStart1 = DifStart1=0
256 // printf("after minTemp3_fast min2 = %d, DifStart4 = %d\n", min2, DifStart4);
257  if(DifStart4>DifStartMin)
258  arrangeQuoters_superFast_lessThen5(pInOut, DifStart0/100, M[(min2+1)&1], M[min2], 3 - M[min2], 3 - M[(min2+1)&1], iVar, nWords, pCanonPerm, pCanonPhase);
259  else
260  arrangeQuoters_superFast_lessThen5(pInOut, DifStart0/100, M[min1], M[(min1+1)&1], 3 - M[(min1+1)&1], 3 - M[min1], iVar, nWords, pCanonPerm, pCanonPhase);
261  }
262  }
263 }
264 
265 void minimalSwapAndFlipIVar_superFast_lessThen5_noEBFC(word* pInOut, int iVar, int nWords, char * pCanonPerm, unsigned* pCanonPhase)
266 {
267  int DifStart1;
268  if(minTemp1_fast(pInOut, iVar, nWords, &DifStart1) == 2)
269  arrangeQuoters_superFast_lessThen5(pInOut, DifStart1/100, 0, 2, 1, 3, iVar, nWords, pCanonPerm, pCanonPhase);
270 }
271 ////////////////////////////////////iVar = 5/////////////////////////////////////////////////////////////////////////////////////////////
272 
273 // It rearranges InOut (swaps and flips through rearrangement of quoters)
274 // It updates Info at the end
275 void arrangeQuoters_superFast_iVar5(unsigned* pInOut, unsigned* temp, int start, int iQ, int jQ, int kQ, int lQ, char * pCanonPerm, unsigned* pCanonPhase)
276 {
277  int i,blockSize,shiftSize;
278  unsigned* tempPtr = temp+start;
279 // printf("in arrangeQuoters_superFast_iVar5\n");
280 
281  if(iQ == 0 && jQ == 1)
282  return;
283  blockSize = sizeof(unsigned);
284  shiftSize = 4;
285  for(i=start-1;i>0;i-=shiftSize)
286  {
287  tempPtr -= 1;
288  memcpy(tempPtr, pInOut+i-iQ, blockSize);
289  tempPtr -= 1;
290  memcpy(tempPtr, pInOut+i-jQ, blockSize);
291  tempPtr -= 1;
292  memcpy(tempPtr, pInOut+i-kQ, blockSize);
293  tempPtr -= 1;
294  memcpy(tempPtr, pInOut+i-lQ, blockSize);
295  }
296  memcpy(pInOut, temp, start*sizeof(unsigned));
297  updataInfo(iQ, jQ, 5, pCanonPerm, pCanonPhase);
298 }
299 
300 //It compares 0Q and 3Q and returns 0 if 0Q is smaller then 3Q ( comparison starts at highest bit) and visa versa
301 // DifStart contains the information about the first different bit in 0Q and 3Q
302 int minTemp0_fast_iVar5(unsigned* pInOut, int nWords, int* pDifStart)
303 {
304  int i, temp;
305 // printf("in minTemp0_fast_iVar5\n");
306  for(i=(nWords)*2 - 1; i>=0; i-=4)
307  {
308  temp = CompareWords(pInOut[i],pInOut[i-3]);
309  if(temp == 0)
310  continue;
311  else if(temp == -1)
312  {
313  *pDifStart = i+1;
314  return 0;
315  }
316  else
317  {
318  *pDifStart = i+1;
319  return 3;
320  }
321  }
322  *pDifStart=0;
323  return 0;
324 }
325 
326 //It compares 1Q and 2Q and returns 1 if 1Q is smaller then 2Q ( comparison starts at highest bit) and visa versa
327 // DifStart contains the information about the first different bit in 1Q and 2Q
328 int minTemp1_fast_iVar5(unsigned* pInOut, int nWords, int* pDifStart)
329 {
330  int i, temp;
331 // printf("in minTemp1_fast_iVar5\n");
332  for(i=(nWords)*2 - 2; i>=0; i-=4)
333  {
334  temp = CompareWords(pInOut[i],pInOut[i-1]);
335  if(temp == 0)
336  continue;
337  else if(temp == -1)
338  {
339  *pDifStart = i+2;
340  return 1;
341  }
342  else
343  {
344  *pDifStart = i+2;
345  return 2;
346  }
347  }
348  *pDifStart=0;
349  return 1;
350 }
351 
352 //It compares iQ and jQ and returns 0 if iQ is smaller then jQ ( comparison starts at highest bit) and visa versa
353 // DifStart contains the information about the first different bit in iQ and jQ
354 int minTemp2_fast_iVar5(unsigned* pInOut, int iQ, int jQ, int nWords, int* pDifStart)
355 {
356  int i, temp;
357 // printf("in minTemp2_fast_iVar5\n");
358 
359  for(i=(nWords)*2 - 1; i>=0; i-=4)
360  {
361  temp = CompareWords(pInOut[i-iQ],pInOut[i-jQ]);
362  if(temp == 0)
363  continue;
364  else if(temp == -1)
365  {
366  *pDifStart = i+1;
367  return 0;
368  }
369  else
370  {
371  *pDifStart = i+1;
372  return 1;
373  }
374  }
375  *pDifStart=0;
376  return 0;
377 }
378 
379 // same as minTemp2_fast but this one has a start position
380 int minTemp3_fast_iVar5(unsigned* pInOut, int start, int finish, int iQ, int jQ, int* pDifStart)
381 {
382  int i, temp;
383 // printf("in minTemp3_fast_iVar5\n");
384 
385  for(i=start-1; i>=finish; i-=4)
386  {
387  temp = CompareWords(pInOut[i-iQ],pInOut[i-jQ]);
388  if(temp == 0)
389  continue;
390  else if(temp == -1)
391  {
392  *pDifStart = i+1;
393  return 0;
394  }
395  else
396  {
397  *pDifStart = i+1;
398  return 1;
399  }
400  }
401  *pDifStart=0;
402  return 0;
403 }
404 
405 // It considers all swap and flip possibilities of iVar and iVar+1 and switches InOut to a minimal of them
406 void minimalSwapAndFlipIVar_superFast_iVar5(unsigned* pInOut, int nWords, char * pCanonPerm, unsigned* pCanonPhase)
407 {
408  int min1, min2, DifStart0, DifStart1, DifStartMin;
409  int M[2];
410  unsigned temp[2048];
411 // printf("in minimalSwapAndFlipIVar_superFast_iVar5\n");
412  M[0] = minTemp0_fast_iVar5(pInOut, nWords, &DifStart0); // 0, 3
413  M[1] = minTemp1_fast_iVar5(pInOut, nWords, &DifStart1); // 1, 2
414  min1 = minTemp2_fast_iVar5(pInOut, M[0], M[1], nWords, &DifStartMin);
415  if(DifStart0 != DifStart1)
416  {
417  if( DifStartMin>=DifStart1 && DifStartMin>=DifStart0 )
418  arrangeQuoters_superFast_iVar5(pInOut, temp, DifStartMin, M[min1], M[(min1+1)&1], 3 - M[(min1+1)&1], 3 - M[min1], pCanonPerm, pCanonPhase);
419  else if( DifStart0 > DifStart1)
420  arrangeQuoters_superFast_iVar5(pInOut, temp, luckyMax(DifStartMin,DifStart0), M[0], M[1], 3 - M[1], 3 - M[0], pCanonPerm, pCanonPhase);
421  else
422  arrangeQuoters_superFast_iVar5(pInOut, temp, luckyMax(DifStartMin,DifStart1), M[1], M[0], 3 - M[0], 3 - M[1], pCanonPerm, pCanonPhase);
423  }
424  else
425  {
426  if(DifStartMin>=DifStart0)
427  arrangeQuoters_superFast_iVar5(pInOut, temp, DifStartMin, M[min1], M[(min1+1)&1], 3 - M[(min1+1)&1], 3 - M[min1], pCanonPerm, pCanonPhase);
428  else
429  {
430  min2 = minTemp3_fast_iVar5(pInOut, DifStart0, DifStartMin, 3-M[0], 3-M[1], &DifStart1); // reuse DifStart1 because DifStart1 = DifStart1=0
431  if(DifStart1>DifStartMin)
432  arrangeQuoters_superFast_iVar5(pInOut, temp, DifStart0, M[(min2+1)&1], M[min2], 3 - M[min2], 3 - M[(min2+1)&1], pCanonPerm, pCanonPhase);
433  else
434  arrangeQuoters_superFast_iVar5(pInOut, temp, DifStart0, M[min1], M[(min1+1)&1], 3 - M[(min1+1)&1], 3 - M[min1], pCanonPerm, pCanonPhase);
435  }
436  }
437 }
438 
439 void minimalSwapAndFlipIVar_superFast_iVar5_noEBFC(unsigned* pInOut, int nWords, char * pCanonPerm, unsigned* pCanonPhase)
440 {
441  int DifStart1;
442  unsigned temp[2048];
443  if(minTemp1_fast_iVar5(pInOut, nWords, &DifStart1) == 2)
444  arrangeQuoters_superFast_iVar5(pInOut, temp, DifStart1, 0, 2, 1, 3, pCanonPerm, pCanonPhase);
445 }
446 
447 ////////////////////////////////////moreThen5/////////////////////////////////////////////////////////////////////////////////////////////
448 
449 // It rearranges InOut (swaps and flips through rearrangement of quoters)
450 // It updates Info at the end
451 void arrangeQuoters_superFast_moreThen5(word* pInOut, word* temp, int start, int iQ, int jQ, int kQ, int lQ, int iVar, char * pCanonPerm, unsigned* pCanonPhase)
452 {
453  int i,wordBlock,blockSize,shiftSize;
454  word* tempPtr = temp+start;
455 // printf("in arrangeQuoters_superFast_moreThen5\n");
456 
457  if(iQ == 0 && jQ == 1)
458  return;
459  wordBlock = (1<<(iVar-6));
460  blockSize = wordBlock*sizeof(word);
461  shiftSize = wordBlock*4;
462  for(i=start-wordBlock;i>0;i-=shiftSize)
463  {
464  tempPtr -= wordBlock;
465  memcpy(tempPtr, pInOut+i-iQ*wordBlock, blockSize);
466  tempPtr -= wordBlock;
467  memcpy(tempPtr, pInOut+i-jQ*wordBlock, blockSize);
468  tempPtr -= wordBlock;
469  memcpy(tempPtr, pInOut+i-kQ*wordBlock, blockSize);
470  tempPtr -= wordBlock;
471  memcpy(tempPtr, pInOut+i-lQ*wordBlock, blockSize);
472  }
473  memcpy(pInOut, temp, start*sizeof(word));
474  updataInfo(iQ, jQ, iVar, pCanonPerm, pCanonPhase);
475 // printf("out arrangeQuoters_superFast_moreThen5\n");
476 
477 }
478 
479 //It compares 0Q and 3Q and returns 0 if 0Q is smaller then 3Q ( comparison starts at highest bit) and visa versa
480 // DifStart contains the information about the first different bit in 0Q and 3Q
481 int minTemp0_fast_moreThen5(word* pInOut, int iVar, int nWords, int* pDifStart)
482 {
483  int i, j, temp;
484  int wordBlock = 1<<(iVar-6);
485  int wordDif = 3*wordBlock;
486  int shiftBlock = wordBlock*4;
487 // printf("in minTemp0_fast_moreThen5\n");
488 
489  for(i=nWords - 1; i>=0; i-=shiftBlock)
490  for(j=0;j<wordBlock;j++)
491  {
492  temp = CompareWords(pInOut[i-j],pInOut[i-j-wordDif]);
493  if(temp == 0)
494  continue;
495  else if(temp == -1)
496  {
497  *pDifStart = i+1;
498  return 0;
499  }
500  else
501  {
502  *pDifStart = i+1;
503  return 3;
504  }
505  }
506  *pDifStart=0;
507 // printf("out minTemp0_fast_moreThen5\n");
508 
509  return 0;
510 }
511 
512 //It compares 1Q and 2Q and returns 1 if 1Q is smaller then 2Q ( comparison starts at highest bit) and visa versa
513 // DifStart contains the information about the first different bit in 1Q and 2Q
514 int minTemp1_fast_moreThen5(word* pInOut, int iVar, int nWords, int* pDifStart)
515 {
516  int i, j, temp;
517  int wordBlock = 1<<(iVar-6);
518  int shiftBlock = wordBlock*4;
519 // printf("in minTemp1_fast_moreThen5\n");
520 
521  for(i=nWords - wordBlock - 1; i>=0; i-=shiftBlock)
522  for(j=0;j<wordBlock;j++)
523  {
524  temp = CompareWords(pInOut[i-j],pInOut[i-j-wordBlock]);
525  if(temp == 0)
526  continue;
527  else if(temp == -1)
528  {
529  *pDifStart = i+wordBlock+1;
530  return 1;
531  }
532  else
533  {
534  *pDifStart = i+wordBlock+1;
535  return 2;
536  }
537  }
538  *pDifStart=0;
539 // printf("out minTemp1_fast_moreThen5\n");
540 
541  return 1;
542 }
543 
544 //It compares iQ and jQ and returns 0 if iQ is smaller then jQ ( comparison starts at highest bit) and visa versa
545 // DifStart contains the information about the first different bit in iQ and jQ
546 int minTemp2_fast_moreThen5(word* pInOut, int iVar, int iQ, int jQ, int nWords, int* pDifStart)
547 {
548  int i, j, temp;
549  int wordBlock = 1<<(iVar-6);
550  int shiftBlock = wordBlock*4;
551 // printf("in minTemp2_fast_moreThen5\n");
552 
553  for(i=nWords - 1; i>=0; i-=shiftBlock)
554  for(j=0;j<wordBlock;j++)
555  {
556  temp = CompareWords(pInOut[i-j-iQ*wordBlock],pInOut[i-j-jQ*wordBlock]);
557  if(temp == 0)
558  continue;
559  else if(temp == -1)
560  {
561  *pDifStart = i+1;
562  return 0;
563  }
564  else
565  {
566  *pDifStart = i+1;
567  return 1;
568  }
569  }
570  *pDifStart=0;
571 // printf("out minTemp2_fast_moreThen5\n");
572 
573  return 0;
574 }
575 
576 // same as minTemp2_fast but this one has a start position
577 int minTemp3_fast_moreThen5(word* pInOut, int iVar, int start, int finish, int iQ, int jQ, int* pDifStart)
578 {
579  int i, j, temp;
580  int wordBlock = 1<<(iVar-6);
581  int shiftBlock = wordBlock*4;
582 // printf("in minTemp3_fast_moreThen5\n");
583 
584  for(i=start-1; i>=finish; i-=shiftBlock)
585  for(j=0;j<wordBlock;j++)
586  {
587  temp = CompareWords(pInOut[i-j-iQ*wordBlock],pInOut[i-j-jQ*wordBlock]);
588  if(temp == 0)
589  continue;
590  else if(temp == -1)
591  {
592  *pDifStart = i+1;
593  return 0;
594  }
595  else
596  {
597  *pDifStart = i+1;
598  return 1;
599  }
600  }
601  *pDifStart=0;
602 // printf("out minTemp3_fast_moreThen5\n");
603 
604  return 0;
605 }
606 
607 // It considers all swap and flip possibilities of iVar and iVar+1 and switches InOut to a minimal of them
608 void minimalSwapAndFlipIVar_superFast_moreThen5(word* pInOut, int iVar, int nWords, char * pCanonPerm, unsigned* pCanonPhase)
609 {
610  int min1, min2, DifStart0, DifStart1, DifStartMin;
611  int M[2];
612  word temp[1024];
613 // printf("in minimalSwapAndFlipIVar_superFast_moreThen5\n");
614  M[0] = minTemp0_fast_moreThen5(pInOut, iVar, nWords, &DifStart0); // 0, 3
615  M[1] = minTemp1_fast_moreThen5(pInOut, iVar, nWords, &DifStart1); // 1, 2
616  min1 = minTemp2_fast_moreThen5(pInOut, iVar, M[0], M[1], nWords, &DifStartMin);
617  if(DifStart0 != DifStart1)
618  {
619  if( DifStartMin>=DifStart1 && DifStartMin>=DifStart0 )
620  arrangeQuoters_superFast_moreThen5(pInOut, temp, DifStartMin, M[min1], M[(min1+1)&1], 3 - M[(min1+1)&1], 3 - M[min1], iVar, pCanonPerm, pCanonPhase);
621  else if( DifStart0 > DifStart1)
622  arrangeQuoters_superFast_moreThen5(pInOut, temp, luckyMax(DifStartMin,DifStart0), M[0], M[1], 3 - M[1], 3 - M[0], iVar, pCanonPerm, pCanonPhase);
623  else
624  arrangeQuoters_superFast_moreThen5(pInOut, temp, luckyMax(DifStartMin,DifStart1), M[1], M[0], 3 - M[0], 3 - M[1], iVar, pCanonPerm, pCanonPhase);
625  }
626  else
627  {
628  if(DifStartMin>=DifStart0)
629  arrangeQuoters_superFast_moreThen5(pInOut, temp, DifStartMin, M[min1], M[(min1+1)&1], 3 - M[(min1+1)&1], 3 - M[min1], iVar, pCanonPerm, pCanonPhase);
630  else
631  {
632  min2 = minTemp3_fast_moreThen5(pInOut, iVar, DifStart0, DifStartMin, 3-M[0], 3-M[1], &DifStart1); // reuse DifStart1 because DifStart1 = DifStart1=0
633  if(DifStart1>DifStartMin)
634  arrangeQuoters_superFast_moreThen5(pInOut, temp, DifStart0, M[(min2+1)&1], M[min2], 3 - M[min2], 3 - M[(min2+1)&1], iVar, pCanonPerm, pCanonPhase);
635  else
636  arrangeQuoters_superFast_moreThen5(pInOut, temp, DifStart0, M[min1], M[(min1+1)&1], 3 - M[(min1+1)&1], 3 - M[min1], iVar, pCanonPerm, pCanonPhase);
637  }
638  }
639 // printf("out minimalSwapAndFlipIVar_superFast_moreThen5\n");
640 
641 }
642 
643 void minimalSwapAndFlipIVar_superFast_moreThen5_noEBFC(word* pInOut, int iVar, int nWords, char * pCanonPerm, unsigned* pCanonPhase)
644 {
645  int DifStart1;
646  word temp[1024];
647  if(minTemp1_fast_moreThen5(pInOut, iVar, nWords, &DifStart1) == 2)
648  arrangeQuoters_superFast_moreThen5(pInOut, temp, DifStart1, 0, 2, 1, 3, iVar, pCanonPerm, pCanonPhase);
649 }
650 
651 /////////////////////////////////// for all /////////////////////////////////////////////////////////////////////////////////////////////
652 void minimalInitialFlip_fast_16Vars(word* pInOut, int nVars, unsigned* pCanonPhase)
653 {
654  word oneWord=1;
655  if( (pInOut[Kit_TruthWordNum_64bit( nVars ) -1]>>63) & oneWord )
656  {
657  Kit_TruthNot_64bit( pInOut, nVars );
658  (* pCanonPhase) ^=(1<<nVars);
659  }
660 
661 }
662 
663 // this function finds minimal for all TIED(and tied only) iVars
664 //it finds tied vars based on rearranged Store info - group of tied vars has the same bit count in Store
665 int minimalSwapAndFlipIVar_superFast_all(word* pInOut, int nVars, int nWords, int * pStore, char * pCanonPerm, unsigned* pCanonPhase)
666 {
667  int i;
668  word pDuplicate[1024];
669  int bitInfoTemp = pStore[0];
670  memcpy(pDuplicate,pInOut,nWords*sizeof(word));
671 // printf("in minimalSwapAndFlipIVar_superFast_all\n");
672  for(i=0;i<5;i++)
673  {
674  if(bitInfoTemp == pStore[i+1])
675  minimalSwapAndFlipIVar_superFast_lessThen5(pInOut, i, nWords, pCanonPerm, pCanonPhase);
676  else
677  {
678  bitInfoTemp = pStore[i+1];
679  continue;
680  }
681  }
682  if(bitInfoTemp == pStore[i+1])
683  minimalSwapAndFlipIVar_superFast_iVar5((unsigned*) pInOut, nWords, pCanonPerm, pCanonPhase);
684  else
685  bitInfoTemp = pStore[i+1];
686 
687  for(i=6;i<nVars-1;i++)
688  {
689  if(bitInfoTemp == pStore[i+1])
690  minimalSwapAndFlipIVar_superFast_moreThen5(pInOut, i, nWords, pCanonPerm, pCanonPhase);
691  else
692  {
693  bitInfoTemp = pStore[i+1];
694  continue;
695  }
696  }
697 // printf("out minimalSwapAndFlipIVar_superFast_all\n");
698 
699  if(memcmp(pInOut,pDuplicate , nWords*sizeof(word)) == 0)
700  return 0;
701  else
702  return 1;
703 }
704 
705 int minimalSwapAndFlipIVar_superFast_all_noEBFC(word* pInOut, int nVars, int nWords, int * pStore, char * pCanonPerm, unsigned* pCanonPhase)
706 {
707  int i;
708  word pDuplicate[1024];
709  int bitInfoTemp = pStore[0];
710  memcpy(pDuplicate,pInOut,nWords*sizeof(word));
711  for(i=0;i<5;i++)
712  {
713  if(bitInfoTemp == pStore[i+1])
714  minimalSwapAndFlipIVar_superFast_lessThen5_noEBFC(pInOut, i, nWords, pCanonPerm, pCanonPhase);
715  else
716  {
717  bitInfoTemp = pStore[i+1];
718  continue;
719  }
720  }
721  if(bitInfoTemp == pStore[i+1])
722  minimalSwapAndFlipIVar_superFast_iVar5_noEBFC((unsigned*) pInOut, nWords, pCanonPerm, pCanonPhase);
723  else
724  bitInfoTemp = pStore[i+1];
725 
726  for(i=6;i<nVars-1;i++)
727  {
728  if(bitInfoTemp == pStore[i+1])
729  minimalSwapAndFlipIVar_superFast_moreThen5_noEBFC(pInOut, i, nWords, pCanonPerm, pCanonPhase);
730  else
731  {
732  bitInfoTemp = pStore[i+1];
733  continue;
734  }
735  }
736  if(memcmp(pInOut,pDuplicate , nWords*sizeof(word)) == 0)
737  return 0;
738  else
739  return 1;
740 }
741 
742 
743 // old version with out noEBFC
744 // void luckyCanonicizerS_F_first_16Vars(word* pInOut, int nVars, int nWords, int * pStore, char * pCanonPerm, unsigned* pCanonPhase)
745 // {
746 // while( minimalSwapAndFlipIVar_superFast_all(pInOut, nVars, nWords, pStore, pCanonPerm, pCanonPhase) != 0)
747 // continue;
748 // }
749 
750 void luckyCanonicizerS_F_first_16Vars1(word* pInOut, int nVars, int nWords, int * pStore, char * pCanonPerm, unsigned* pCanonPhase)
751 {
752  if(((* pCanonPhase) >> (nVars+1)) & 1)
753  while( minimalSwapAndFlipIVar_superFast_all(pInOut, nVars, nWords, pStore, pCanonPerm, pCanonPhase) != 0)
754  continue;
755  else
756  while( minimalSwapAndFlipIVar_superFast_all_noEBFC(pInOut, nVars, nWords, pStore, pCanonPerm, pCanonPhase) != 0)
757  continue;
758 }
759 
760 void luckyCanonicizerS_F_first_16Vars11(word* pInOut, int nVars, int nWords, int * pStore, char * pCanonPerm, unsigned* pCanonPhase)
761 {
762  word duplicate[1024];
763  char pCanonPerm1[16];
764  unsigned uCanonPhase1;
765 
766  if((* pCanonPhase) >> (nVars+2) )
767  {
768  memcpy(duplicate, pInOut, sizeof(word)*nWords);
769  Kit_TruthNot_64bit(duplicate, nVars);
770  uCanonPhase1 = *pCanonPhase;
771  uCanonPhase1 ^= (1 << nVars);
772  memcpy(pCanonPerm1,pCanonPerm,sizeof(char)*16);
773  luckyCanonicizerS_F_first_16Vars1(pInOut, nVars, nWords, pStore, pCanonPerm, pCanonPhase);
774  luckyCanonicizerS_F_first_16Vars1(duplicate, nVars, nWords, pStore, pCanonPerm1, &uCanonPhase1);
775  if(memCompare(pInOut, duplicate,nVars) == 1)
776  {
777  *pCanonPhase = uCanonPhase1;
778  memcpy(pCanonPerm,pCanonPerm1,sizeof(char)*16);
779  memcpy(pInOut, duplicate, sizeof(word)*nWords);
780  }
781  }
782  else
783  {
784  luckyCanonicizerS_F_first_16Vars1(pInOut, nVars, nWords, pStore, pCanonPerm, pCanonPhase);
785  }
786 }
787 
788 void luckyCanonicizer_final_fast_16Vars(word* pInOut, int nVars, int nWords, int * pStore, char * pCanonPerm, unsigned* pCanonPhase)
789 {
790  assert( nVars > 6 && nVars <= 16 );
791  (* pCanonPhase) = Kit_TruthSemiCanonicize_Yasha1( pInOut, nVars, pCanonPerm, pStore );
792  luckyCanonicizerS_F_first_16Vars1(pInOut, nVars, nWords, pStore, pCanonPerm, pCanonPhase );
793 }
794 
795 void bitReverceOrder(word* x, int nVars)
796 {
797  int i;
798  for(i= nVars-1;i>=0;i--)
799  Kit_TruthChangePhase_64bit( x, nVars, i );
800 }
801 
802 
803 void luckyCanonicizer_final_fast_16Vars1(word* pInOut, int nVars, int nWords, int * pStore, char * pCanonPerm, unsigned* pCanonPhase)
804 {
805  assert( nVars > 6 && nVars <= 16 );
806  (* pCanonPhase) = Kit_TruthSemiCanonicize_Yasha1( pInOut, nVars, pCanonPerm, pStore );
807  luckyCanonicizerS_F_first_16Vars11(pInOut, nVars, nWords, pStore, pCanonPerm, pCanonPhase );
808  bitReverceOrder(pInOut, nVars);
809  (*pCanonPhase) ^= (1<<nVars) -1;
810  luckyCanonicizerS_F_first_16Vars11(pInOut, nVars, nWords, pStore, pCanonPerm, pCanonPhase );
811 // bitReverceOrder(pInOut, nVars);
812 // (*pCanonPhase) ^= (1<<nVars) -1;
813 // luckyCanonicizerS_F_first_16Vars11(pInOut, nVars, nWords, pStore, pCanonPerm, pCanonPhase );
814 }
815 
816 
817 // top-level procedure calling two special cases (nVars <= 6 and nVars <= 16)
818 unsigned luckyCanonicizer_final_fast( word * pInOut, int nVars, char * pCanonPerm )
819 {
820  int nWords;
821  int pStore[16];
822  unsigned uCanonPhase = 0;
823 #ifdef LUCKY_VERIFY
824  word temp[1024] = {0};
825  word duplicate[1024] = {0};
826  Kit_TruthCopy_64bit( duplicate, pInOut, nVars );
827 #endif
828  if ( nVars <= 6 )
829  pInOut[0] = luckyCanonicizer_final_fast_6Vars( pInOut[0], pStore, pCanonPerm, &uCanonPhase);
830  else if ( nVars <= 16 )
831  {
832  nWords = (nVars <= 6) ? 1 : (1 << (nVars - 6));
833  luckyCanonicizer_final_fast_16Vars( pInOut, nVars, nWords, pStore, pCanonPerm, &uCanonPhase );
834  }
835  else assert( 0 );
836 #ifdef LUCKY_VERIFY
837  Kit_TruthCopy_64bit( temp, pInOut, nVars );
838  assert( ! luckyCheck(temp, duplicate, nVars, pCanonPerm, uCanonPhase) );
839 #endif
840  return uCanonPhase;
841 }
842 
843 unsigned luckyCanonicizer_final_fast1( word * pInOut, int nVars, char * pCanonPerm)
844 {
845  int nWords;
846  int pStore[16];
847  unsigned uCanonPhase = 0;
848 #ifdef LUCKY_VERIFY
849  word temp[1024] = {0};
850  word duplicate[1024] = {0};
851  Kit_TruthCopy_64bit( duplicate, pInOut, nVars );
852 #endif
853  if ( nVars <= 6 )
854  pInOut[0] = luckyCanonicizer_final_fast_6Vars1( pInOut[0], pStore, pCanonPerm, &uCanonPhase);
855  else if ( nVars <= 16 )
856  {
857  nWords = 1 << (nVars - 6);
858  luckyCanonicizer_final_fast_16Vars1( pInOut, nVars, nWords, pStore, pCanonPerm, &uCanonPhase );
859  }
860  else assert( 0 );
861 #ifdef LUCKY_VERIFY
862  Kit_TruthCopy_64bit( temp, pInOut, nVars );
863  assert( ! luckyCheck(temp, duplicate, nVars, pCanonPerm, uCanonPhase) );
864 #endif
865  return uCanonPhase;
866 }
867 
868 
870 
871 
872 
int minimalSwapAndFlipIVar_superFast_all(word *pInOut, int nVars, int nWords, int *pStore, char *pCanonPerm, unsigned *pCanonPhase)
Definition: luckyFast16.c:665
int minTemp3_fast_iVar5(unsigned *pInOut, int start, int finish, int iQ, int jQ, int *pDifStart)
Definition: luckyFast16.c:380
void Kit_TruthCopy_64bit(word *pOut, word *pIn, int nVars)
Definition: luckySwap.c:136
void luckyCanonicizerS_F_first_16Vars1(word *pInOut, int nVars, int nWords, int *pStore, char *pCanonPerm, unsigned *pCanonPhase)
Definition: luckyFast16.c:750
unsigned luckyCanonicizer_final_fast(word *pInOut, int nVars, char *pCanonPerm)
Definition: luckyFast16.c:818
void swapAndFlip(word *pAfter, int nVars, int iVarInPosition, int jVar, char *pCanonPerm, unsigned *pUCanonPhase)
Definition: luckyFast16.c:31
static ABC_NAMESPACE_IMPL_START word SFmask[5][4]
Definition: luckyFast16.c:22
void luckyCanonicizer_final_fast_16Vars(word *pInOut, int nVars, int nWords, int *pStore, char *pCanonPerm, unsigned *pCanonPhase)
Definition: luckyFast16.c:788
void arrangeQuoters_superFast_lessThen5(word *pInOut, int start, int iQ, int jQ, int kQ, int lQ, int iVar, int nWords, char *pCanonPerm, unsigned *pCanonPhase)
Definition: luckyFast16.c:101
int Kit_TruthWordNum_64bit(int nVars)
Definition: luckySwap.c:36
char * memcpy()
word luckyCanonicizer_final_fast_6Vars1(word InOut, int *pStore, char *pCanonPerm, unsigned *pCanonPhase)
Definition: luckyFast6.c:270
void luckyCanonicizerS_F_first_16Vars11(word *pInOut, int nVars, int nWords, int *pStore, char *pCanonPerm, unsigned *pCanonPhase)
Definition: luckyFast16.c:760
int minTemp2_fast_moreThen5(word *pInOut, int iVar, int iQ, int jQ, int nWords, int *pDifStart)
Definition: luckyFast16.c:546
int nWords
Definition: abcNpn.c:127
word M(word f1, word f2, int n)
Definition: kitPerm.c:240
void arrangeQuoters_superFast_moreThen5(word *pInOut, word *temp, int start, int iQ, int jQ, int kQ, int lQ, int iVar, char *pCanonPerm, unsigned *pCanonPhase)
Definition: luckyFast16.c:451
void minimalSwapAndFlipIVar_superFast_lessThen5_noEBFC(word *pInOut, int iVar, int nWords, char *pCanonPerm, unsigned *pCanonPhase)
Definition: luckyFast16.c:265
void swap_ij(word *f, int totalVars, int varI, int varJ)
Definition: luckySwapIJ.c:88
int minTemp0_fast_moreThen5(word *pInOut, int iVar, int nWords, int *pDifStart)
Definition: luckyFast16.c:481
int minTemp3_fast_moreThen5(word *pInOut, int iVar, int start, int finish, int iQ, int jQ, int *pDifStart)
Definition: luckyFast16.c:577
void minimalSwapAndFlipIVar_superFast_iVar5(unsigned *pInOut, int nWords, char *pCanonPerm, unsigned *pCanonPhase)
Definition: luckyFast16.c:406
int minTemp2_fast(word *pInOut, int iVar, int iQ, int jQ, int nWords, int *pDifStart)
Definition: luckyFast16.c:182
unsigned adjustInfoAfterSwap(char *pCanonPerm, unsigned uCanonPhase, int iVar, unsigned info)
Definition: luckyFast6.c:51
void minimalSwapAndFlipIVar_superFast_moreThen5(word *pInOut, int iVar, int nWords, char *pCanonPerm, unsigned *pCanonPhase)
Definition: luckyFast16.c:608
int CompareWords(void *p1, void *p2)
unsigned __int64 word
DECLARATIONS ///.
Definition: kitPerm.c:36
void minimalSwapAndFlipIVar_superFast_moreThen5_noEBFC(word *pInOut, int iVar, int nWords, char *pCanonPerm, unsigned *pCanonPhase)
Definition: luckyFast16.c:643
#define ABC_NAMESPACE_IMPL_END
Definition: abc_global.h:108
void minimalSwapAndFlipIVar_superFast_lessThen5(word *pInOut, int iVar, int nWords, char *pCanonPerm, unsigned *pCanonPhase)
Definition: luckyFast16.c:229
int memcmp()
int luckyCheck(word *pAfter, word *pBefore, int nVars, char *pCanonPerm, unsigned uCanonPhase)
Definition: luckyFast16.c:49
void bitReverceOrder(word *x, int nVars)
Definition: luckyFast16.c:795
void minimalSwapAndFlipIVar_superFast_iVar5_noEBFC(unsigned *pInOut, int nWords, char *pCanonPerm, unsigned *pCanonPhase)
Definition: luckyFast16.c:439
int minTemp1_fast_iVar5(unsigned *pInOut, int nWords, int *pDifStart)
Definition: luckyFast16.c:328
int minTemp3_fast(word *pInOut, int iVar, int start, int finish, int iQ, int jQ, int *pDifStart)
Definition: luckyFast16.c:205
void Kit_TruthNot_64bit(word *pIn, int nVars)
Definition: luckySwap.c:130
void updataInfo(int iQ, int jQ, int iVar, char *pCanonPerm, unsigned *pCanonPhase)
Definition: luckyFast16.c:76
void arrangeQuoters_superFast_iVar5(unsigned *pInOut, unsigned *temp, int start, int iQ, int jQ, int kQ, int lQ, char *pCanonPerm, unsigned *pCanonPhase)
Definition: luckyFast16.c:275
#define ABC_NAMESPACE_IMPL_START
Definition: abc_global.h:107
unsigned Kit_TruthSemiCanonicize_Yasha1(word *pInOut, int nVars, char *pCanonPerm, int *pStore)
Definition: luckySwap.c:245
int minTemp1_fast(word *pInOut, int iVar, int nWords, int *pDifStart)
Definition: luckyFast16.c:157
unsigned luckyCanonicizer_final_fast1(word *pInOut, int nVars, char *pCanonPerm)
Definition: luckyFast16.c:843
void luckyCanonicizer_final_fast_16Vars1(word *pInOut, int nVars, int nWords, int *pStore, char *pCanonPerm, unsigned *pCanonPhase)
Definition: luckyFast16.c:803
void minimalInitialFlip_fast_16Vars(word *pInOut, int nVars, unsigned *pCanonPhase)
Definition: luckyFast16.c:652
#define ABC_CONST(number)
PARAMETERS ///.
Definition: abc_global.h:206
int minTemp1_fast_moreThen5(word *pInOut, int iVar, int nWords, int *pDifStart)
Definition: luckyFast16.c:514
int firstShiftWithOneBit(word x, int blockSize)
Definition: luckyFast16.c:84
int minTemp0_fast(word *pInOut, int iVar, int nWords, int *pDifStart)
Definition: luckyFast16.c:131
#define assert(ex)
Definition: util_old.h:213
int minTemp0_fast_iVar5(unsigned *pInOut, int nWords, int *pDifStart)
Definition: luckyFast16.c:302
int minTemp2_fast_iVar5(unsigned *pInOut, int iQ, int jQ, int nWords, int *pDifStart)
Definition: luckyFast16.c:354
ABC_NAMESPACE_IMPL_START int memCompare(word *x, word *y, int nVars)
Definition: lucky.c:22
word luckyCanonicizer_final_fast_6Vars(word InOut, int *pStore, char *pCanonPerm, unsigned *pCanonPhase)
Definition: luckyFast6.c:265
static int luckyMax(int x, int y)
Definition: luckyInt.h:109
void Kit_TruthChangePhase_64bit(word *pInOut, int nVars, int iVar)
Definition: luckySwap.c:100
int minimalSwapAndFlipIVar_superFast_all_noEBFC(word *pInOut, int nVars, int nWords, int *pStore, char *pCanonPerm, unsigned *pCanonPhase)
Definition: luckyFast16.c:705