abc-master
 All Data Structures Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros
dauCanon.c
Go to the documentation of this file.
1 /**CFile****************************************************************
2 
3  FileName [dauCanon.c]
4 
5  SystemName [ABC: Logic synthesis and verification system.]
6 
7  PackageName [DAG-aware unmapping.]
8 
9  Synopsis [Canonical form computation.]
10 
11  Author [Alan Mishchenko]
12 
13  Affiliation [UC Berkeley]
14 
15  Date [Ver. 1.0. Started - June 20, 2005.]
16 
17  Revision [$Id: dauCanon.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
18 
19 ***********************************************************************/
20 
21 #include "dauInt.h"
22 #include "misc/util/utilTruth.h"
23 
24 ABC_NAMESPACE_IMPL_START
25 
26 ////////////////////////////////////////////////////////////////////////
27 /// DECLARATIONS ///
28 ////////////////////////////////////////////////////////////////////////
29 
30 static word s_CMasks6[5] = {
31  ABC_CONST(0x1111111111111111),
32  ABC_CONST(0x0303030303030303),
33  ABC_CONST(0x000F000F000F000F),
34  ABC_CONST(0x000000FF000000FF),
35  ABC_CONST(0x000000000000FFFF)
36 };
37 
38 ////////////////////////////////////////////////////////////////////////
39 /// FUNCTION DEFINITIONS ///
40 ////////////////////////////////////////////////////////////////////////
41 
42 /**Function*************************************************************
43 
44  Synopsis [Compares Cof0 and Cof1.]
45 
46  Description []
47 
48  SideEffects []
49 
50  SeeAlso []
51 
52 ***********************************************************************/
53 static inline int Abc_TtCompare1VarCofs( word * pTruth, int nWords, int iVar )
54 {
55  if ( nWords == 1 )
56  {
57  word Cof0 = pTruth[0] & s_Truths6Neg[iVar];
58  word Cof1 = (pTruth[0] >> (1 << iVar)) & s_Truths6Neg[iVar];
59  if ( Cof0 != Cof1 )
60  return Cof0 < Cof1 ? -1 : 1;
61  return 0;
62  }
63  if ( iVar <= 5 )
64  {
65  word Cof0, Cof1;
66  int w, shift = (1 << iVar);
67  for ( w = 0; w < nWords; w++ )
68  {
69  Cof0 = pTruth[w] & s_Truths6Neg[iVar];
70  Cof1 = (pTruth[w] >> shift) & s_Truths6Neg[iVar];
71  if ( Cof0 != Cof1 )
72  return Cof0 < Cof1 ? -1 : 1;
73  }
74  return 0;
75  }
76  // if ( iVar > 5 )
77  {
78  word * pLimit = pTruth + nWords;
79  int i, iStep = Abc_TtWordNum(iVar);
80  assert( nWords >= 2 );
81  for ( ; pTruth < pLimit; pTruth += 2*iStep )
82  for ( i = 0; i < iStep; i++ )
83  if ( pTruth[i] != pTruth[i + iStep] )
84  return pTruth[i] < pTruth[i + iStep] ? -1 : 1;
85  return 0;
86  }
87 }
88 static inline int Abc_TtCompare1VarCofsRev( word * pTruth, int nWords, int iVar )
89 {
90  if ( nWords == 1 )
91  {
92  word Cof0 = pTruth[0] & s_Truths6Neg[iVar];
93  word Cof1 = (pTruth[0] >> (1 << iVar)) & s_Truths6Neg[iVar];
94  if ( Cof0 != Cof1 )
95  return Cof0 < Cof1 ? -1 : 1;
96  return 0;
97  }
98  if ( iVar <= 5 )
99  {
100  word Cof0, Cof1;
101  int w, shift = (1 << iVar);
102  for ( w = nWords - 1; w >= 0; w-- )
103  {
104  Cof0 = pTruth[w] & s_Truths6Neg[iVar];
105  Cof1 = (pTruth[w] >> shift) & s_Truths6Neg[iVar];
106  if ( Cof0 != Cof1 )
107  return Cof0 < Cof1 ? -1 : 1;
108  }
109  return 0;
110  }
111  // if ( iVar > 5 )
112  {
113  word * pLimit = pTruth + nWords;
114  int i, iStep = Abc_TtWordNum(iVar);
115  assert( nWords >= 2 );
116  for ( pLimit -= 2*iStep; pLimit >= pTruth; pLimit -= 2*iStep )
117  for ( i = iStep - 1; i >= 0; i-- )
118  if ( pLimit[i] != pLimit[i + iStep] )
119  return pLimit[i] < pLimit[i + iStep] ? -1 : 1;
120  return 0;
121  }
122 }
123 
124 /**Function*************************************************************
125 
126  Synopsis [Checks equality of pairs of cofactors w.r.t. adjacent variables.]
127 
128  Description []
129 
130  SideEffects []
131 
132  SeeAlso []
133 
134 ***********************************************************************/
135 static inline int Abc_TtCheckEqual2VarCofs( word * pTruth, int nWords, int iVar, int Num1, int Num2 )
136 {
137  assert( Num1 < Num2 && Num2 < 4 );
138  if ( nWords == 1 )
139  return ((pTruth[0] >> (Num2 * (1 << iVar))) & s_CMasks6[iVar]) == ((pTruth[0] >> (Num1 * (1 << iVar))) & s_CMasks6[iVar]);
140  if ( iVar <= 4 )
141  {
142  int w, shift = (1 << iVar);
143  for ( w = 0; w < nWords; w++ )
144  if ( ((pTruth[w] >> Num2 * shift) & s_CMasks6[iVar]) != ((pTruth[w] >> Num1 * shift) & s_CMasks6[iVar]) )
145  return 0;
146  return 1;
147  }
148  if ( iVar == 5 )
149  {
150  unsigned * pTruthU = (unsigned *)pTruth;
151  unsigned * pLimitU = (unsigned *)(pTruth + nWords);
152  assert( nWords >= 2 );
153  for ( ; pTruthU < pLimitU; pTruthU += 4 )
154  if ( pTruthU[Num2] != pTruthU[Num1] )
155  return 0;
156  return 1;
157  }
158  // if ( iVar > 5 )
159  {
160  word * pLimit = pTruth + nWords;
161  int i, iStep = Abc_TtWordNum(iVar);
162  assert( nWords >= 4 );
163  for ( ; pTruth < pLimit; pTruth += 4*iStep )
164  for ( i = 0; i < iStep; i++ )
165  if ( pTruth[i+Num2*iStep] != pTruth[i+Num1*iStep] )
166  return 0;
167  return 1;
168  }
169 }
170 
171 /**Function*************************************************************
172 
173  Synopsis [Compares pairs of cofactors w.r.t. adjacent variables.]
174 
175  Description []
176 
177  SideEffects []
178 
179  SeeAlso []
180 
181 ***********************************************************************/
182 static inline int Abc_TtCompare2VarCofs( word * pTruth, int nWords, int iVar, int Num1, int Num2 )
183 {
184  assert( Num1 < Num2 && Num2 < 4 );
185  if ( nWords == 1 )
186  {
187  word Cof1 = (pTruth[0] >> (Num1 * (1 << iVar))) & s_CMasks6[iVar];
188  word Cof2 = (pTruth[0] >> (Num2 * (1 << iVar))) & s_CMasks6[iVar];
189  if ( Cof1 != Cof2 )
190  return Cof1 < Cof2 ? -1 : 1;
191  return 0;
192  }
193  if ( iVar <= 4 )
194  {
195  word Cof1, Cof2;
196  int w, shift = (1 << iVar);
197  for ( w = 0; w < nWords; w++ )
198  {
199  Cof1 = (pTruth[w] >> Num1 * shift) & s_CMasks6[iVar];
200  Cof2 = (pTruth[w] >> Num2 * shift) & s_CMasks6[iVar];
201  if ( Cof1 != Cof2 )
202  return Cof1 < Cof2 ? -1 : 1;
203  }
204  return 0;
205  }
206  if ( iVar == 5 )
207  {
208  unsigned * pTruthU = (unsigned *)pTruth;
209  unsigned * pLimitU = (unsigned *)(pTruth + nWords);
210  assert( nWords >= 2 );
211  for ( ; pTruthU < pLimitU; pTruthU += 4 )
212  if ( pTruthU[Num1] != pTruthU[Num2] )
213  return pTruthU[Num1] < pTruthU[Num2] ? -1 : 1;
214  return 0;
215  }
216  // if ( iVar > 5 )
217  {
218  word * pLimit = pTruth + nWords;
219  int i, iStep = Abc_TtWordNum(iVar);
220  int Offset1 = Num1*iStep;
221  int Offset2 = Num2*iStep;
222  assert( nWords >= 4 );
223  for ( ; pTruth < pLimit; pTruth += 4*iStep )
224  for ( i = 0; i < iStep; i++ )
225  if ( pTruth[i + Offset1] != pTruth[i + Offset2] )
226  return pTruth[i + Offset1] < pTruth[i + Offset2] ? -1 : 1;
227  return 0;
228  }
229 }
230 static inline int Abc_TtCompare2VarCofsRev( word * pTruth, int nWords, int iVar, int Num1, int Num2 )
231 {
232  assert( Num1 < Num2 && Num2 < 4 );
233  if ( nWords == 1 )
234  {
235  word Cof1 = (pTruth[0] >> (Num1 * (1 << iVar))) & s_CMasks6[iVar];
236  word Cof2 = (pTruth[0] >> (Num2 * (1 << iVar))) & s_CMasks6[iVar];
237  if ( Cof1 != Cof2 )
238  return Cof1 < Cof2 ? -1 : 1;
239  return 0;
240  }
241  if ( iVar <= 4 )
242  {
243  word Cof1, Cof2;
244  int w, shift = (1 << iVar);
245  for ( w = nWords - 1; w >= 0; w-- )
246  {
247  Cof1 = (pTruth[w] >> Num1 * shift) & s_CMasks6[iVar];
248  Cof2 = (pTruth[w] >> Num2 * shift) & s_CMasks6[iVar];
249  if ( Cof1 != Cof2 )
250  return Cof1 < Cof2 ? -1 : 1;
251  }
252  return 0;
253  }
254  if ( iVar == 5 )
255  {
256  unsigned * pTruthU = (unsigned *)pTruth;
257  unsigned * pLimitU = (unsigned *)(pTruth + nWords);
258  assert( nWords >= 2 );
259  for ( pLimitU -= 4; pLimitU >= pTruthU; pLimitU -= 4 )
260  if ( pLimitU[Num1] != pLimitU[Num2] )
261  return pLimitU[Num1] < pLimitU[Num2] ? -1 : 1;
262  return 0;
263  }
264  // if ( iVar > 5 )
265  {
266  word * pLimit = pTruth + nWords;
267  int i, iStep = Abc_TtWordNum(iVar);
268  int Offset1 = Num1*iStep;
269  int Offset2 = Num2*iStep;
270  assert( nWords >= 4 );
271  for ( pLimit -= 4*iStep; pLimit >= pTruth; pLimit -= 4*iStep )
272  for ( i = iStep - 1; i >= 0; i-- )
273  if ( pLimit[i + Offset1] != pLimit[i + Offset2] )
274  return pLimit[i + Offset1] < pLimit[i + Offset2] ? -1 : 1;
275  return 0;
276  }
277 }
278 
279 /**Function*************************************************************
280 
281  Synopsis [Minterm counting in all cofactors.]
282 
283  Description []
284 
285  SideEffects []
286 
287  SeeAlso []
288 
289 ***********************************************************************/
290 static inline int Abc_TtCountOnesInTruth( word * pTruth, int nVars )
291 {
292  int nWords = Abc_TtWordNum( nVars );
293  int k, Counter = 0;
294  for ( k = 0; k < nWords; k++ )
295  if ( pTruth[k] )
296  Counter += Abc_TtCountOnes( pTruth[k] );
297  return Counter;
298 }
299 static inline void Abc_TtCountOnesInCofs( word * pTruth, int nVars, int * pStore )
300 {
301  word Temp;
302  int i, k, Counter, nWords;
303  if ( nVars <= 6 )
304  {
305  for ( i = 0; i < nVars; i++ )
306  pStore[i] = Abc_TtCountOnes( pTruth[0] & s_Truths6Neg[i] );
307  return;
308  }
309  assert( nVars > 6 );
310  nWords = Abc_TtWordNum( nVars );
311  memset( pStore, 0, sizeof(int) * nVars );
312  for ( k = 0; k < nWords; k++ )
313  {
314  // count 1's for the first six variables
315  for ( i = 0; i < 6; i++ )
316  if ( (Temp = (pTruth[k] & s_Truths6Neg[i]) | ((pTruth[k+1] & s_Truths6Neg[i]) << (1 << i))) )
317  pStore[i] += Abc_TtCountOnes( Temp );
318  // count 1's for all other variables
319  if ( pTruth[k] )
320  {
321  Counter = Abc_TtCountOnes( pTruth[k] );
322  for ( i = 6; i < nVars; i++ )
323  if ( (k & (1 << (i-6))) == 0 )
324  pStore[i] += Counter;
325  }
326  k++;
327  // count 1's for all other variables
328  if ( pTruth[k] )
329  {
330  Counter = Abc_TtCountOnes( pTruth[k] );
331  for ( i = 6; i < nVars; i++ )
332  if ( (k & (1 << (i-6))) == 0 )
333  pStore[i] += Counter;
334  }
335  }
336 }
337 
338 /**Function*************************************************************
339 
340  Synopsis [Minterm counting in all cofactors.]
341 
342  Description []
343 
344  SideEffects []
345 
346  SeeAlso []
347 
348 ***********************************************************************/
349 static inline void Abc_TtCountOnesInCofsSlow( word * pTruth, int nVars, int * pStore )
350 {
351  static int bit_count[256] = {
352  0,1,1,2,1,2,2,3,1,2,2,3,2,3,3,4,1,2,2,3,2,3,3,4,2,3,3,4,3,4,4,5,
353  1,2,2,3,2,3,3,4,2,3,3,4,3,4,4,5,2,3,3,4,3,4,4,5,3,4,4,5,4,5,5,6,
354  1,2,2,3,2,3,3,4,2,3,3,4,3,4,4,5,2,3,3,4,3,4,4,5,3,4,4,5,4,5,5,6,
355  2,3,3,4,3,4,4,5,3,4,4,5,4,5,5,6,3,4,4,5,4,5,5,6,4,5,5,6,5,6,6,7,
356  1,2,2,3,2,3,3,4,2,3,3,4,3,4,4,5,2,3,3,4,3,4,4,5,3,4,4,5,4,5,5,6,
357  2,3,3,4,3,4,4,5,3,4,4,5,4,5,5,6,3,4,4,5,4,5,5,6,4,5,5,6,5,6,6,7,
358  2,3,3,4,3,4,4,5,3,4,4,5,4,5,5,6,3,4,4,5,4,5,5,6,4,5,5,6,5,6,6,7,
359  3,4,4,5,4,5,5,6,4,5,5,6,5,6,6,7,4,5,5,6,5,6,6,7,5,6,6,7,6,7,7,8
360  };
361  int i, k, nBytes;
362  unsigned char * pTruthC = (unsigned char *)pTruth;
363  nBytes = 8 * Abc_TtWordNum( nVars );
364  memset( pStore, 0, sizeof(int) * nVars );
365  for ( k = 0; k < nBytes; k++ )
366  {
367  pStore[0] += bit_count[ pTruthC[k] & 0x55 ];
368  pStore[1] += bit_count[ pTruthC[k] & 0x33 ];
369  pStore[2] += bit_count[ pTruthC[k] & 0x0F ];
370  for ( i = 3; i < nVars; i++ )
371  if ( (k & (1 << (i-3))) == 0 )
372  pStore[i] += bit_count[pTruthC[k]];
373  }
374 }
375 
376 /**Function*************************************************************
377 
378  Synopsis [Minterm counting in all cofactors.]
379 
380  Description []
381 
382  SideEffects []
383 
384  SeeAlso []
385 
386 ***********************************************************************/
387 int Abc_TtCountOnesInCofsFast6_rec( word Truth, int iVar, int nBytes, int * pStore )
388 {
389  static int bit_count[256] = {
390  0,1,1,2,1,2,2,3,1,2,2,3,2,3,3,4,1,2,2,3,2,3,3,4,2,3,3,4,3,4,4,5,
391  1,2,2,3,2,3,3,4,2,3,3,4,3,4,4,5,2,3,3,4,3,4,4,5,3,4,4,5,4,5,5,6,
392  1,2,2,3,2,3,3,4,2,3,3,4,3,4,4,5,2,3,3,4,3,4,4,5,3,4,4,5,4,5,5,6,
393  2,3,3,4,3,4,4,5,3,4,4,5,4,5,5,6,3,4,4,5,4,5,5,6,4,5,5,6,5,6,6,7,
394  1,2,2,3,2,3,3,4,2,3,3,4,3,4,4,5,2,3,3,4,3,4,4,5,3,4,4,5,4,5,5,6,
395  2,3,3,4,3,4,4,5,3,4,4,5,4,5,5,6,3,4,4,5,4,5,5,6,4,5,5,6,5,6,6,7,
396  2,3,3,4,3,4,4,5,3,4,4,5,4,5,5,6,3,4,4,5,4,5,5,6,4,5,5,6,5,6,6,7,
397  3,4,4,5,4,5,5,6,4,5,5,6,5,6,6,7,4,5,5,6,5,6,6,7,5,6,6,7,6,7,7,8
398  };
399  int nMints0, nMints1;
400  if ( Truth == 0 )
401  return 0;
402  if ( ~Truth == 0 )
403  {
404  int i;
405  for ( i = 0; i <= iVar; i++ )
406  pStore[i] += nBytes * 4;
407  return nBytes * 8;
408  }
409  if ( nBytes == 1 )
410  {
411  assert( iVar == 2 );
412  pStore[0] += bit_count[ Truth & 0x55 ];
413  pStore[1] += bit_count[ Truth & 0x33 ];
414  pStore[2] += bit_count[ Truth & 0x0F ];
415  return bit_count[ Truth & 0xFF ];
416  }
417  nMints0 = Abc_TtCountOnesInCofsFast6_rec( Abc_Tt6Cofactor0(Truth, iVar), iVar - 1, nBytes/2, pStore );
418  nMints1 = Abc_TtCountOnesInCofsFast6_rec( Abc_Tt6Cofactor1(Truth, iVar), iVar - 1, nBytes/2, pStore );
419  pStore[iVar] += nMints0;
420  return nMints0 + nMints1;
421 }
422 
423 int Abc_TtCountOnesInCofsFast_rec( word * pTruth, int iVar, int nWords, int * pStore )
424 {
425  int nMints0, nMints1;
426  if ( nWords == 1 )
427  {
428  assert( iVar == 5 );
429  return Abc_TtCountOnesInCofsFast6_rec( pTruth[0], iVar, 8, pStore );
430  }
431  assert( nWords > 1 );
432  assert( iVar > 5 );
433  if ( pTruth[0] & 1 )
434  {
435  if ( Abc_TtIsConst1( pTruth, nWords ) )
436  {
437  int i;
438  for ( i = 0; i <= iVar; i++ )
439  pStore[i] += nWords * 32;
440  return nWords * 64;
441  }
442  }
443  else
444  {
445  if ( Abc_TtIsConst0( pTruth, nWords ) )
446  return 0;
447  }
448  nMints0 = Abc_TtCountOnesInCofsFast_rec( pTruth, iVar - 1, nWords/2, pStore );
449  nMints1 = Abc_TtCountOnesInCofsFast_rec( pTruth + nWords/2, iVar - 1, nWords/2, pStore );
450  pStore[iVar] += nMints0;
451  return nMints0 + nMints1;
452 }
453 int Abc_TtCountOnesInCofsFast( word * pTruth, int nVars, int * pStore )
454 {
455  memset( pStore, 0, sizeof(int) * nVars );
456  assert( nVars >= 3 );
457  if ( nVars <= 6 )
458  return Abc_TtCountOnesInCofsFast6_rec( pTruth[0], nVars - 1, Abc_TtByteNum( nVars ), pStore );
459  else
460  return Abc_TtCountOnesInCofsFast_rec( pTruth, nVars - 1, Abc_TtWordNum( nVars ), pStore );
461 }
462 
463 
464 /**Function*************************************************************
465 
466  Synopsis []
467 
468  Description []
469 
470  SideEffects []
471 
472  SeeAlso []
473 
474 ***********************************************************************/
475 static inline unsigned Abc_TtSemiCanonicize( word * pTruth, int nVars, char * pCanonPerm, int * pStoreOut )
476 {
477  int fOldSwap = 0;
478  int pStoreIn[17];
479  int * pStore = pStoreOut ? pStoreOut : pStoreIn;
480  int i, nOnes, nWords = Abc_TtWordNum( nVars );
481  unsigned uCanonPhase = 0;
482  assert( nVars <= 16 );
483  for ( i = 0; i < nVars; i++ )
484  pCanonPerm[i] = i;
485  // normalize polarity
486  nOnes = Abc_TtCountOnesInTruth( pTruth, nVars );
487  if ( nOnes > nWords * 32 )
488  {
489  Abc_TtNot( pTruth, nWords );
490  nOnes = nWords*64 - nOnes;
491  uCanonPhase |= (1 << nVars);
492  }
493  // normalize phase
494  Abc_TtCountOnesInCofs( pTruth, nVars, pStore );
495  pStore[nVars] = nOnes;
496  for ( i = 0; i < nVars; i++ )
497  {
498  if ( pStore[i] >= nOnes - pStore[i] )
499  continue;
500  Abc_TtFlip( pTruth, nWords, i );
501  uCanonPhase |= (1 << i);
502  pStore[i] = nOnes - pStore[i];
503  }
504  // normalize permutation
505  if ( fOldSwap )
506  {
507  int fChange;
508  do {
509  fChange = 0;
510  for ( i = 0; i < nVars-1; i++ )
511  {
512  if ( pStore[i] <= pStore[i+1] )
513  // if ( pStore[i] >= pStore[i+1] )
514  continue;
515  ABC_SWAP( int, pCanonPerm[i], pCanonPerm[i+1] );
516  ABC_SWAP( int, pStore[i], pStore[i+1] );
517  if ( ((uCanonPhase >> i) & 1) != ((uCanonPhase >> (i+1)) & 1) )
518  {
519  uCanonPhase ^= (1 << i);
520  uCanonPhase ^= (1 << (i+1));
521  }
522  Abc_TtSwapAdjacent( pTruth, nWords, i );
523  fChange = 1;
524  // nSwaps++;
525  }
526  }
527  while ( fChange );
528  }
529  else
530  {
531  int k, BestK;
532  for ( i = 0; i < nVars - 1; i++ )
533  {
534  BestK = i + 1;
535  for ( k = i + 2; k < nVars; k++ )
536  if ( pStore[BestK] > pStore[k] )
537  // if ( pStore[BestK] < pStore[k] )
538  BestK = k;
539  if ( pStore[i] <= pStore[BestK] )
540  // if ( pStore[i] >= pStore[BestK] )
541  continue;
542  ABC_SWAP( int, pCanonPerm[i], pCanonPerm[BestK] );
543  ABC_SWAP( int, pStore[i], pStore[BestK] );
544  if ( ((uCanonPhase >> i) & 1) != ((uCanonPhase >> BestK) & 1) )
545  {
546  uCanonPhase ^= (1 << i);
547  uCanonPhase ^= (1 << BestK);
548  }
549  Abc_TtSwapVars( pTruth, nVars, i, BestK );
550  // nSwaps++;
551  }
552  }
553  return uCanonPhase;
554 }
555 
556 
557 
558 /**Function*************************************************************
559 
560  Synopsis []
561 
562  Description []
563 
564  SideEffects []
565 
566  SeeAlso []
567 
568 ***********************************************************************/
569 void Abc_TtCofactorTest10( word * pTruth, int nVars, int N )
570 {
571  static word pCopy1[1024];
572  static word pCopy2[1024];
573  int nWords = Abc_TtWordNum( nVars );
574  int i;
575  for ( i = 0; i < nVars - 1; i++ )
576  {
577 // Kit_DsdPrintFromTruth( pTruth, nVars ); printf( "\n" );
578  Abc_TtCopy( pCopy1, pTruth, nWords, 0 );
579  Abc_TtSwapAdjacent( pCopy1, nWords, i );
580 // Kit_DsdPrintFromTruth( pCopy1, nVars ); printf( "\n" );
581  Abc_TtCopy( pCopy2, pTruth, nWords, 0 );
582  Abc_TtSwapVars( pCopy2, nVars, i, i+1 );
583 // Kit_DsdPrintFromTruth( pCopy2, nVars ); printf( "\n" );
584  assert( Abc_TtEqual( pCopy1, pCopy2, nWords ) );
585  }
586 }
587 
588 /**Function*************************************************************
589 
590  Synopsis [Naive evaluation.]
591 
592  Description []
593 
594  SideEffects []
595 
596  SeeAlso []
597 
598 ***********************************************************************/
599 int Abc_Tt6CofactorPermNaive( word * pTruth, int i, int fSwapOnly )
600 {
601  if ( fSwapOnly )
602  {
603  word Copy = Abc_Tt6SwapAdjacent( pTruth[0], i );
604  if ( pTruth[0] > Copy )
605  {
606  pTruth[0] = Copy;
607  return 4;
608  }
609  return 0;
610  }
611  {
612  word Copy = pTruth[0];
613  word Best = pTruth[0];
614  int Config = 0;
615  // PXY
616  // 001
617  Copy = Abc_Tt6Flip( Copy, i );
618  if ( Best > Copy )
619  Best = Copy, Config = 1;
620  // PXY
621  // 011
622  Copy = Abc_Tt6Flip( Copy, i+1 );
623  if ( Best > Copy )
624  Best = Copy, Config = 3;
625  // PXY
626  // 010
627  Copy = Abc_Tt6Flip( Copy, i );
628  if ( Best > Copy )
629  Best = Copy, Config = 2;
630  // PXY
631  // 110
632  Copy = Abc_Tt6SwapAdjacent( Copy, i );
633  if ( Best > Copy )
634  Best = Copy, Config = 6;
635  // PXY
636  // 111
637  Copy = Abc_Tt6Flip( Copy, i+1 );
638  if ( Best > Copy )
639  Best = Copy, Config = 7;
640  // PXY
641  // 101
642  Copy = Abc_Tt6Flip( Copy, i );
643  if ( Best > Copy )
644  Best = Copy, Config = 5;
645  // PXY
646  // 100
647  Copy = Abc_Tt6Flip( Copy, i+1 );
648  if ( Best > Copy )
649  Best = Copy, Config = 4;
650  // PXY
651  // 000
652  Copy = Abc_Tt6SwapAdjacent( Copy, i );
653  assert( Copy == pTruth[0] );
654  assert( Best <= pTruth[0] );
655  pTruth[0] = Best;
656  return Config;
657  }
658 }
659 int Abc_TtCofactorPermNaive( word * pTruth, int i, int nWords, int fSwapOnly )
660 {
661  if ( fSwapOnly )
662  {
663  static word pCopy[1024];
664  Abc_TtCopy( pCopy, pTruth, nWords, 0 );
665  Abc_TtSwapAdjacent( pCopy, nWords, i );
666  if ( Abc_TtCompareRev(pTruth, pCopy, nWords) == 1 )
667  {
668  Abc_TtCopy( pTruth, pCopy, nWords, 0 );
669  return 4;
670  }
671  return 0;
672  }
673  {
674  static word pCopy[1024];
675  static word pBest[1024];
676  int Config = 0;
677  // save two copies
678  Abc_TtCopy( pCopy, pTruth, nWords, 0 );
679  Abc_TtCopy( pBest, pTruth, nWords, 0 );
680  // PXY
681  // 001
682  Abc_TtFlip( pCopy, nWords, i );
683  if ( Abc_TtCompareRev(pBest, pCopy, nWords) == 1 )
684  Abc_TtCopy( pBest, pCopy, nWords, 0 ), Config = 1;
685  // PXY
686  // 011
687  Abc_TtFlip( pCopy, nWords, i+1 );
688  if ( Abc_TtCompareRev(pBest, pCopy, nWords) == 1 )
689  Abc_TtCopy( pBest, pCopy, nWords, 0 ), Config = 3;
690  // PXY
691  // 010
692  Abc_TtFlip( pCopy, nWords, i );
693  if ( Abc_TtCompareRev(pBest, pCopy, nWords) == 1 )
694  Abc_TtCopy( pBest, pCopy, nWords, 0 ), Config = 2;
695  // PXY
696  // 110
697  Abc_TtSwapAdjacent( pCopy, nWords, i );
698  if ( Abc_TtCompareRev(pBest, pCopy, nWords) == 1 )
699  Abc_TtCopy( pBest, pCopy, nWords, 0 ), Config = 6;
700  // PXY
701  // 111
702  Abc_TtFlip( pCopy, nWords, i+1 );
703  if ( Abc_TtCompareRev(pBest, pCopy, nWords) == 1 )
704  Abc_TtCopy( pBest, pCopy, nWords, 0 ), Config = 7;
705  // PXY
706  // 101
707  Abc_TtFlip( pCopy, nWords, i );
708  if ( Abc_TtCompareRev(pBest, pCopy, nWords) == 1 )
709  Abc_TtCopy( pBest, pCopy, nWords, 0 ), Config = 5;
710  // PXY
711  // 100
712  Abc_TtFlip( pCopy, nWords, i+1 );
713  if ( Abc_TtCompareRev(pBest, pCopy, nWords) == 1 )
714  Abc_TtCopy( pBest, pCopy, nWords, 0 ), Config = 4;
715  // PXY
716  // 000
717  Abc_TtSwapAdjacent( pCopy, nWords, i );
718  assert( Abc_TtEqual( pTruth, pCopy, nWords ) );
719  if ( Config == 0 )
720  return 0;
721  assert( Abc_TtCompareRev(pTruth, pBest, nWords) == 1 );
722  Abc_TtCopy( pTruth, pBest, nWords, 0 );
723  return Config;
724  }
725 }
726 
727 
728 /**Function*************************************************************
729 
730  Synopsis [Smart evaluation.]
731 
732  Description []
733 
734  SideEffects []
735 
736  SeeAlso []
737 
738 ***********************************************************************/
739 int Abc_TtCofactorPermConfig( word * pTruth, int i, int nWords, int fSwapOnly, int fNaive )
740 {
741  if ( nWords == 1 )
742  return Abc_Tt6CofactorPermNaive( pTruth, i, fSwapOnly );
743  if ( fNaive )
744  return Abc_TtCofactorPermNaive( pTruth, i, nWords, fSwapOnly );
745  if ( fSwapOnly )
746  {
747  if ( Abc_TtCompare2VarCofsRev( pTruth, nWords, i, 1, 2 ) < 0 ) // Cof1 < Cof2
748  {
749  Abc_TtSwapAdjacent( pTruth, nWords, i );
750  return 4;
751  }
752  return 0;
753  }
754  {
755  int fComp01, fComp02, fComp03, fComp12, fComp13, fComp23, Config = 0;
756  fComp01 = Abc_TtCompare2VarCofsRev( pTruth, nWords, i, 0, 1 );
757  fComp23 = Abc_TtCompare2VarCofsRev( pTruth, nWords, i, 2, 3 );
758  if ( fComp23 >= 0 ) // Cof2 >= Cof3
759  {
760  if ( fComp01 >= 0 ) // Cof0 >= Cof1
761  {
762  fComp13 = Abc_TtCompare2VarCofsRev( pTruth, nWords, i, 1, 3 );
763  if ( fComp13 < 0 ) // Cof1 < Cof3
764  Abc_TtFlip( pTruth, nWords, i + 1 ), Config = 2;
765  else if ( fComp13 == 0 ) // Cof1 == Cof3
766  {
767  fComp02 = Abc_TtCompare2VarCofsRev( pTruth, nWords, i, 0, 2 );
768  if ( fComp02 < 0 )
769  Abc_TtFlip( pTruth, nWords, i + 1 ), Config = 2;
770  }
771  // else Cof1 > Cof3 -- do nothing
772  }
773  else // Cof0 < Cof1
774  {
775  fComp03 = Abc_TtCompare2VarCofsRev( pTruth, nWords, i, 0, 3 );
776  if ( fComp03 < 0 ) // Cof0 < Cof3
777  {
778  Abc_TtFlip( pTruth, nWords, i );
779  Abc_TtFlip( pTruth, nWords, i + 1 ), Config = 3;
780  }
781  else // Cof0 >= Cof3
782  {
783  if ( fComp23 == 0 ) // can flip Cof0 and Cof1
784  Abc_TtFlip( pTruth, nWords, i ), Config = 1;
785  }
786  }
787  }
788  else // Cof2 < Cof3
789  {
790  if ( fComp01 >= 0 ) // Cof0 >= Cof1
791  {
792  fComp12 = Abc_TtCompare2VarCofsRev( pTruth, nWords, i, 1, 2 );
793  if ( fComp12 > 0 ) // Cof1 > Cof2
794  Abc_TtFlip( pTruth, nWords, i ), Config = 1;
795  else if ( fComp12 == 0 ) // Cof1 == Cof2
796  {
797  Abc_TtFlip( pTruth, nWords, i );
798  Abc_TtFlip( pTruth, nWords, i + 1 ), Config = 3;
799  }
800  else // Cof1 < Cof2
801  {
802  Abc_TtFlip( pTruth, nWords, i + 1 ), Config = 2;
803  if ( fComp01 == 0 )
804  Abc_TtFlip( pTruth, nWords, i ), Config ^= 1;
805  }
806  }
807  else // Cof0 < Cof1
808  {
809  fComp02 = Abc_TtCompare2VarCofsRev( pTruth, nWords, i, 0, 2 );
810  if ( fComp02 == -1 ) // Cof0 < Cof2
811  {
812  Abc_TtFlip( pTruth, nWords, i );
813  Abc_TtFlip( pTruth, nWords, i + 1 ), Config = 3;
814  }
815  else if ( fComp02 == 0 ) // Cof0 == Cof2
816  {
817  fComp13 = Abc_TtCompare2VarCofsRev( pTruth, nWords, i, 1, 3 );
818  if ( fComp13 >= 0 ) // Cof1 >= Cof3
819  Abc_TtFlip( pTruth, nWords, i ), Config = 1;
820  else // Cof1 < Cof3
821  {
822  Abc_TtFlip( pTruth, nWords, i );
823  Abc_TtFlip( pTruth, nWords, i + 1 ), Config = 3;
824  }
825  }
826  else // Cof0 > Cof2
827  Abc_TtFlip( pTruth, nWords, i ), Config = 1;
828  }
829  }
830  // perform final swap if needed
831  fComp12 = Abc_TtCompare2VarCofsRev( pTruth, nWords, i, 1, 2 );
832  if ( fComp12 < 0 ) // Cof1 < Cof2
833  Abc_TtSwapAdjacent( pTruth, nWords, i ), Config ^= 4;
834  return Config;
835  }
836 }
837 int Abc_TtCofactorPerm( word * pTruth, int i, int nWords, int fSwapOnly, char * pCanonPerm, unsigned * puCanonPhase, int fNaive )
838 {
839  if ( fSwapOnly )
840  {
841  int Config = Abc_TtCofactorPermConfig( pTruth, i, nWords, 1, 0 );
842  if ( Config )
843  {
844  if ( ((*puCanonPhase >> i) & 1) != ((*puCanonPhase >> (i+1)) & 1) )
845  {
846  *puCanonPhase ^= (1 << i);
847  *puCanonPhase ^= (1 << (i+1));
848  }
849  ABC_SWAP( int, pCanonPerm[i], pCanonPerm[i+1] );
850  }
851  return Config;
852  }
853  {
854  static word pCopy1[1024];
855  int Config;
856  Abc_TtCopy( pCopy1, pTruth, nWords, 0 );
857  Config = Abc_TtCofactorPermConfig( pTruth, i, nWords, 0, fNaive );
858  if ( Config == 0 )
859  return 0;
860  if ( Abc_TtCompareRev(pTruth, pCopy1, nWords) == 1 ) // made it worse
861  {
862  Abc_TtCopy( pTruth, pCopy1, nWords, 0 );
863  return 0;
864  }
865  // improved
866  if ( Config & 1 )
867  *puCanonPhase ^= (1 << i);
868  if ( Config & 2 )
869  *puCanonPhase ^= (1 << (i+1));
870  if ( Config & 4 )
871  {
872  if ( ((*puCanonPhase >> i) & 1) != ((*puCanonPhase >> (i+1)) & 1) )
873  {
874  *puCanonPhase ^= (1 << i);
875  *puCanonPhase ^= (1 << (i+1));
876  }
877  ABC_SWAP( int, pCanonPerm[i], pCanonPerm[i+1] );
878  }
879  return Config;
880  }
881 }
882 
883 /**Function*************************************************************
884 
885  Synopsis [Semi-canonical form computation.]
886 
887  Description []
888 
889  SideEffects []
890 
891  SeeAlso []
892 
893 ***********************************************************************/
894 //#define CANON_VERIFY
895 unsigned Abc_TtCanonicize( word * pTruth, int nVars, char * pCanonPerm )
896 {
897  int pStoreIn[17];
898  unsigned uCanonPhase;
899  int i, k, nWords = Abc_TtWordNum( nVars );
900  int fNaive = 1;
901 
902 #ifdef CANON_VERIFY
903  char pCanonPermCopy[16];
904  static word pCopy1[1024];
905  static word pCopy2[1024];
906  Abc_TtCopy( pCopy1, pTruth, nWords, 0 );
907 #endif
908 
909  uCanonPhase = Abc_TtSemiCanonicize( pTruth, nVars, pCanonPerm, pStoreIn );
910  for ( k = 0; k < 5; k++ )
911  {
912  int fChanges = 0;
913  for ( i = nVars - 2; i >= 0; i-- )
914  if ( pStoreIn[i] == pStoreIn[i+1] )
915  fChanges |= Abc_TtCofactorPerm( pTruth, i, nWords, pStoreIn[i] != pStoreIn[nVars]/2, pCanonPerm, &uCanonPhase, fNaive );
916  if ( !fChanges )
917  break;
918  fChanges = 0;
919  for ( i = 1; i < nVars - 1; i++ )
920  if ( pStoreIn[i] == pStoreIn[i+1] )
921  fChanges |= Abc_TtCofactorPerm( pTruth, i, nWords, pStoreIn[i] != pStoreIn[nVars]/2, pCanonPerm, &uCanonPhase, fNaive );
922  if ( !fChanges )
923  break;
924  }
925 
926 #ifdef CANON_VERIFY
927  Abc_TtCopy( pCopy2, pTruth, nWords, 0 );
928  memcpy( pCanonPermCopy, pCanonPerm, sizeof(char) * nVars );
929  Abc_TtImplementNpnConfig( pCopy2, nVars, pCanonPermCopy, uCanonPhase );
930  if ( !Abc_TtEqual( pCopy1, pCopy2, nWords ) )
931  printf( "Canonical form verification failed!\n" );
932 #endif
933 /*
934  if ( !Abc_TtEqual( pCopy1, pCopy2, nWords ) )
935  {
936  Kit_DsdPrintFromTruth( pCopy1, nVars ); printf( "\n" );
937  Kit_DsdPrintFromTruth( pCopy2, nVars ); printf( "\n" );
938  i = 0;
939  }
940 */
941  return uCanonPhase;
942 }
943 
944 /**Function*************************************************************
945 
946  Synopsis [Semi-canonical form computation.]
947 
948  Description []
949 
950  SideEffects []
951 
952  SeeAlso []
953 
954 ***********************************************************************/
955 static inline int Abc_TtCanonicizePhaseVar6( word * pTruth, int nVars, int v )
956 {
957  int w, nWords = Abc_TtWordNum( nVars );
958  int s, nStep = 1 << (v-6);
959  assert( v >= 6 );
960  for ( w = nWords - 1, s = nWords - nStep; w > 0; w-- )
961  {
962  if ( pTruth[w-nStep] == pTruth[w] )
963  {
964  if ( w == s ) { w = s - nStep; s = w - nStep; }
965  continue;
966  }
967  if ( pTruth[w-nStep] > pTruth[w] )
968  return -1;
969  for ( ; w > 0; w-- )
970  {
971  ABC_SWAP( word, pTruth[w-nStep], pTruth[w] );
972  if ( w == s ) { w = s - nStep; s = w - nStep; }
973  }
974  assert( w == -1 );
975  return 1;
976  }
977  return 0;
978 }
979 static inline int Abc_TtCanonicizePhaseVar5( word * pTruth, int nVars, int v )
980 {
981  int w, nWords = Abc_TtWordNum( nVars );
982  int Shift = 1 << v;
983  word Mask = s_Truths6[v];
984  assert( v < 6 );
985  for ( w = nWords - 1; w >= 0; w-- )
986  {
987  if ( ((pTruth[w] << Shift) & Mask) == (pTruth[w] & Mask) )
988  continue;
989  if ( ((pTruth[w] << Shift) & Mask) > (pTruth[w] & Mask) )
990  return -1;
991 // Extra_PrintHex( stdout, (unsigned *)pTruth, nVars ); printf("\n" );
992  for ( ; w >= 0; w-- )
993  pTruth[w] = ((pTruth[w] << Shift) & Mask) | ((pTruth[w] & Mask) >> Shift);
994 // Extra_PrintHex( stdout, (unsigned *)pTruth, nVars ); printf( " changed %d", v ), printf("\n" );
995  return 1;
996  }
997  return 0;
998 }
999 unsigned Abc_TtCanonicizePhase( word * pTruth, int nVars )
1000 {
1001  unsigned uCanonPhase = 0;
1002  int v, nWords = Abc_TtWordNum( nVars );
1003 // static int Counter = 0;
1004 // Counter++;
1005 
1006 #ifdef CANON_VERIFY
1007  static word pCopy1[1024];
1008  static word pCopy2[1024];
1009  Abc_TtCopy( pCopy1, pTruth, nWords, 0 );
1010 #endif
1011 
1012  if ( (pTruth[nWords-1] >> 63) & 1 )
1013  {
1014  Abc_TtNot( pTruth, nWords );
1015  uCanonPhase ^= (1 << nVars);
1016  }
1017 
1018 // while ( 1 )
1019 // {
1020 // unsigned uCanonPhase2 = uCanonPhase;
1021  for ( v = nVars - 1; v >= 6; v-- )
1022  if ( Abc_TtCanonicizePhaseVar6( pTruth, nVars, v ) == 1 )
1023  uCanonPhase ^= 1 << v;
1024  for ( ; v >= 0; v-- )
1025  if ( Abc_TtCanonicizePhaseVar5( pTruth, nVars, v ) == 1 )
1026  uCanonPhase ^= 1 << v;
1027 // if ( uCanonPhase2 == uCanonPhase )
1028 // break;
1029 // }
1030 
1031 // for ( v = 5; v >= 0; v-- )
1032 // assert( Abc_TtCanonicizePhaseVar5( pTruth, nVars, v ) != 1 );
1033 
1034 #ifdef CANON_VERIFY
1035  Abc_TtCopy( pCopy2, pTruth, nWords, 0 );
1036  Abc_TtImplementNpnConfig( pCopy2, nVars, NULL, uCanonPhase );
1037  if ( !Abc_TtEqual( pCopy1, pCopy2, nWords ) )
1038  printf( "Canonical form verification failed!\n" );
1039 #endif
1040  return uCanonPhase;
1041 }
1042 
1043 
1044 ////////////////////////////////////////////////////////////////////////
1045 /// END OF FILE ///
1046 ////////////////////////////////////////////////////////////////////////
1047 
1048 
1049 ABC_NAMESPACE_IMPL_END
1050 
memset
char * memset()
Abc_TtCountOnesInCofsFast6_rec
int Abc_TtCountOnesInCofsFast6_rec(word Truth, int iVar, int nBytes, int *pStore)
Definition: dauCanon.c:387
Abc_TtCofactorPerm
int Abc_TtCofactorPerm(word *pTruth, int i, int nWords, int fSwapOnly, char *pCanonPerm, unsigned *puCanonPhase, int fNaive)
Definition: dauCanon.c:837
Abc_TtCompare1VarCofsRev
static int Abc_TtCompare1VarCofsRev(word *pTruth, int nWords, int iVar)
Definition: dauCanon.c:88
Abc_TtCanonicizePhaseVar5
static int Abc_TtCanonicizePhaseVar5(word *pTruth, int nVars, int v)
Definition: dauCanon.c:979
Abc_TtCofactorPermNaive
int Abc_TtCofactorPermNaive(word *pTruth, int i, int nWords, int fSwapOnly)
Definition: dauCanon.c:659
Abc_TtIsConst0
static int Abc_TtIsConst0(word *pIn1, int nWords)
Definition: utilTruth.h:293
memcpy
char * memcpy()
Abc_TtCompare2VarCofsRev
static int Abc_TtCompare2VarCofsRev(word *pTruth, int nWords, int iVar, int Num1, int Num2)
Definition: dauCanon.c:230
Abc_Tt6CofactorPermNaive
int Abc_Tt6CofactorPermNaive(word *pTruth, int i, int fSwapOnly)
Definition: dauCanon.c:599
Abc_TtCountOnes
static int Abc_TtCountOnes(word x)
Definition: utilTruth.h:1470
Abc_Tt6Cofactor0
static word Abc_Tt6Cofactor0(word t, int iVar)
Definition: utilTruth.h:370
Abc_TtCanonicizePhaseVar6
static int Abc_TtCanonicizePhaseVar6(word *pTruth, int nVars, int v)
Definition: dauCanon.c:955
bit_count
static int bit_count[256]
Definition: fpgaCut.c:50
Abc_TtCompare1VarCofs
static int Abc_TtCompare1VarCofs(word *pTruth, int nWords, int iVar)
FUNCTION DEFINITIONS ///.
Definition: dauCanon.c:53
nWords
int nWords
Definition: abcNpn.c:127
Abc_TtIsConst1
static int Abc_TtIsConst1(word *pIn1, int nWords)
Definition: utilTruth.h:301
Abc_TtByteNum
static int Abc_TtByteNum(int nVars)
Definition: utilTruth.h:170
ABC_SWAP
#define ABC_SWAP(Type, a, b)
Definition: abc_global.h:218
Abc_Tt6SwapAdjacent
static word Abc_Tt6SwapAdjacent(word Truth, int iVar)
Definition: utilTruth.h:1186
Abc_TtCopy
static void Abc_TtCopy(word *pOut, word *pIn, int nWords, int fCompl)
Definition: utilTruth.h:221
Abc_Tt6Cofactor1
static word Abc_Tt6Cofactor1(word t, int iVar)
Definition: utilTruth.h:375
Abc_TtCofactorTest10
void Abc_TtCofactorTest10(word *pTruth, int nVars, int N)
Definition: dauCanon.c:569
Abc_TtCountOnesInTruth
static int Abc_TtCountOnesInTruth(word *pTruth, int nVars)
Definition: dauCanon.c:290
word
unsigned __int64 word
DECLARATIONS ///.
Definition: kitPerm.c:36
ABC_NAMESPACE_IMPL_END
#define ABC_NAMESPACE_IMPL_END
Definition: abc_global.h:108
Abc_TtCompare2VarCofs
static int Abc_TtCompare2VarCofs(word *pTruth, int nWords, int iVar, int Num1, int Num2)
Definition: dauCanon.c:182
Counter
static int Counter
Definition: extraBddMisc.c:1877
Abc_TtCanonicize
unsigned Abc_TtCanonicize(word *pTruth, int nVars, char *pCanonPerm)
FUNCTION DECLARATIONS ///.
Definition: dauCanon.c:895
Abc_TtImplementNpnConfig
static void Abc_TtImplementNpnConfig(word *pTruth, int nVars, char *pCanonPerm, unsigned uCanonPhase)
Definition: utilTruth.h:1428
s_Truths6Neg
static word s_Truths6Neg[6]
Definition: utilTruth.h:47
Abc_Tt6Flip
static word Abc_Tt6Flip(word Truth, int iVar)
Definition: utilTruth.h:1126
Abc_TtCheckEqual2VarCofs
static int Abc_TtCheckEqual2VarCofs(word *pTruth, int nWords, int iVar, int Num1, int Num2)
Definition: dauCanon.c:135
Abc_TtFlip
static void Abc_TtFlip(word *pTruth, int nWords, int iVar)
Definition: utilTruth.h:1130
ABC_NAMESPACE_IMPL_START
#define ABC_NAMESPACE_IMPL_START
Definition: abc_global.h:107
Truth
static ABC_NAMESPACE_IMPL_START word Truth[8]
DECLARATIONS ///.
Definition: giaShrink6.c:32
s_Truths6
static word s_Truths6[6]
Definition: extraUtilEnum.c:430
Abc_TtSemiCanonicize
static unsigned Abc_TtSemiCanonicize(word *pTruth, int nVars, char *pCanonPerm, int *pStoreOut)
Definition: dauCanon.c:475
Abc_TtCanonicizePhase
unsigned Abc_TtCanonicizePhase(word *pTruth, int nVars)
Definition: dauCanon.c:999
Abc_TtWordNum
static int Abc_TtWordNum(int nVars)
Definition: utilTruth.h:169
ABC_CONST
#define ABC_CONST(number)
PARAMETERS ///.
Definition: abc_global.h:206
Abc_TtCountOnesInCofsSlow
static void Abc_TtCountOnesInCofsSlow(word *pTruth, int nVars, int *pStore)
Definition: dauCanon.c:349
s_CMasks6
static ABC_NAMESPACE_IMPL_START word s_CMasks6[5]
DECLARATIONS ///.
Definition: dauCanon.c:30
Abc_TtEqual
static int Abc_TtEqual(word *pIn1, word *pIn2, int nWords)
Definition: utilTruth.h:269
assert
#define assert(ex)
Definition: util_old.h:213
Abc_TtCountOnesInCofs
static void Abc_TtCountOnesInCofs(word *pTruth, int nVars, int *pStore)
Definition: dauCanon.c:299
Abc_TtCountOnesInCofsFast
int Abc_TtCountOnesInCofsFast(word *pTruth, int nVars, int *pStore)
Definition: dauCanon.c:453
Abc_TtSwapVars
static void Abc_TtSwapVars(word *pTruth, int nVars, int iVar, int jVar)
Definition: utilTruth.h:1228
Abc_TtNot
static void Abc_TtNot(word *pOut, int nWords)
Definition: utilTruth.h:215
Abc_TtCofactorPermConfig
int Abc_TtCofactorPermConfig(word *pTruth, int i, int nWords, int fSwapOnly, int fNaive)
Definition: dauCanon.c:739
Abc_TtCountOnesInCofsFast_rec
int Abc_TtCountOnesInCofsFast_rec(word *pTruth, int iVar, int nWords, int *pStore)
Definition: dauCanon.c:423
Abc_TtSwapAdjacent
static void Abc_TtSwapAdjacent(word *pTruth, int nWords, int iVar)
Definition: utilTruth.h:1190
Abc_TtCompareRev
static int Abc_TtCompareRev(word *pIn1, word *pIn2, int nWords)
Definition: utilTruth.h:285