abc-master
 All Data Structures Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros
kitTruth.c
Go to the documentation of this file.
1 /**CFile****************************************************************
2 
3  FileName [kitTruth.c]
4 
5  SystemName [ABC: Logic synthesis and verification system.]
6 
7  PackageName [Computation kit.]
8 
9  Synopsis [Procedures involving truth tables.]
10 
11  Author [Alan Mishchenko]
12 
13  Affiliation [UC Berkeley]
14 
15  Date [Ver. 1.0. Started - Dec 6, 2006.]
16 
17  Revision [$Id: kitTruth.c,v 1.00 2006/12/06 00:00:00 alanmi Exp $]
18 
19 ***********************************************************************/
20 
21 #include "kit.h"
22 
23 ABC_NAMESPACE_IMPL_START
24 
25 
26 ////////////////////////////////////////////////////////////////////////
27 /// DECLARATIONS ///
28 ////////////////////////////////////////////////////////////////////////
29 
30 ////////////////////////////////////////////////////////////////////////
31 /// FUNCTION DEFINITIONS ///
32 ////////////////////////////////////////////////////////////////////////
33 
34 /**Function*************************************************************
35 
36  Synopsis [Swaps two adjacent variables in the truth table.]
37 
38  Description [Swaps var number Start and var number Start+1 (0-based numbers).
39  The input truth table is pIn. The output truth table is pOut.]
40 
41  SideEffects []
42 
43  SeeAlso []
44 
45 ***********************************************************************/
46 void Kit_TruthSwapAdjacentVars( unsigned * pOut, unsigned * pIn, int nVars, int iVar )
47 {
48  static unsigned PMasks[4][3] = {
49  { 0x99999999, 0x22222222, 0x44444444 },
50  { 0xC3C3C3C3, 0x0C0C0C0C, 0x30303030 },
51  { 0xF00FF00F, 0x00F000F0, 0x0F000F00 },
52  { 0xFF0000FF, 0x0000FF00, 0x00FF0000 }
53  };
54  int nWords = Kit_TruthWordNum( nVars );
55  int i, k, Step, Shift;
56 
57  assert( iVar < nVars - 1 );
58  if ( iVar < 4 )
59  {
60  Shift = (1 << iVar);
61  for ( i = 0; i < nWords; i++ )
62  pOut[i] = (pIn[i] & PMasks[iVar][0]) | ((pIn[i] & PMasks[iVar][1]) << Shift) | ((pIn[i] & PMasks[iVar][2]) >> Shift);
63  }
64  else if ( iVar > 4 )
65  {
66  Step = (1 << (iVar - 5));
67  for ( k = 0; k < nWords; k += 4*Step )
68  {
69  for ( i = 0; i < Step; i++ )
70  pOut[i] = pIn[i];
71  for ( i = 0; i < Step; i++ )
72  pOut[Step+i] = pIn[2*Step+i];
73  for ( i = 0; i < Step; i++ )
74  pOut[2*Step+i] = pIn[Step+i];
75  for ( i = 0; i < Step; i++ )
76  pOut[3*Step+i] = pIn[3*Step+i];
77  pIn += 4*Step;
78  pOut += 4*Step;
79  }
80  }
81  else // if ( iVar == 4 )
82  {
83  for ( i = 0; i < nWords; i += 2 )
84  {
85  pOut[i] = (pIn[i] & 0x0000FFFF) | ((pIn[i+1] & 0x0000FFFF) << 16);
86  pOut[i+1] = (pIn[i+1] & 0xFFFF0000) | ((pIn[i] & 0xFFFF0000) >> 16);
87  }
88  }
89 }
90 
91 /**Function*************************************************************
92 
93  Synopsis [Swaps two adjacent variables in the truth table.]
94 
95  Description [Swaps var number Start and var number Start+1 (0-based numbers).
96  The input truth table is pIn. The output truth table is pOut.]
97 
98  SideEffects []
99 
100  SeeAlso []
101 
102 ***********************************************************************/
103 void Kit_TruthSwapAdjacentVars2( unsigned * pIn, unsigned * pOut, int nVars, int Start )
104 {
105  int nWords = (nVars <= 5)? 1 : (1 << (nVars-5));
106  int i, k, Step;
107 
108  assert( Start < nVars - 1 );
109  switch ( Start )
110  {
111  case 0:
112  for ( i = 0; i < nWords; i++ )
113  pOut[i] = (pIn[i] & 0x99999999) | ((pIn[i] & 0x22222222) << 1) | ((pIn[i] & 0x44444444) >> 1);
114  return;
115  case 1:
116  for ( i = 0; i < nWords; i++ )
117  pOut[i] = (pIn[i] & 0xC3C3C3C3) | ((pIn[i] & 0x0C0C0C0C) << 2) | ((pIn[i] & 0x30303030) >> 2);
118  return;
119  case 2:
120  for ( i = 0; i < nWords; i++ )
121  pOut[i] = (pIn[i] & 0xF00FF00F) | ((pIn[i] & 0x00F000F0) << 4) | ((pIn[i] & 0x0F000F00) >> 4);
122  return;
123  case 3:
124  for ( i = 0; i < nWords; i++ )
125  pOut[i] = (pIn[i] & 0xFF0000FF) | ((pIn[i] & 0x0000FF00) << 8) | ((pIn[i] & 0x00FF0000) >> 8);
126  return;
127  case 4:
128  for ( i = 0; i < nWords; i += 2 )
129  {
130  pOut[i] = (pIn[i] & 0x0000FFFF) | ((pIn[i+1] & 0x0000FFFF) << 16);
131  pOut[i+1] = (pIn[i+1] & 0xFFFF0000) | ((pIn[i] & 0xFFFF0000) >> 16);
132  }
133  return;
134  default:
135  Step = (1 << (Start - 5));
136  for ( k = 0; k < nWords; k += 4*Step )
137  {
138  for ( i = 0; i < Step; i++ )
139  pOut[i] = pIn[i];
140  for ( i = 0; i < Step; i++ )
141  pOut[Step+i] = pIn[2*Step+i];
142  for ( i = 0; i < Step; i++ )
143  pOut[2*Step+i] = pIn[Step+i];
144  for ( i = 0; i < Step; i++ )
145  pOut[3*Step+i] = pIn[3*Step+i];
146  pIn += 4*Step;
147  pOut += 4*Step;
148  }
149  return;
150  }
151 }
152 
153 /**Function*************************************************************
154 
155  Synopsis [Expands the truth table according to the phase.]
156 
157  Description [The input and output truth tables are in pIn/pOut. The current number
158  of variables is nVars. The total number of variables in nVarsAll. The last argument
159  (Phase) contains shows where the variables should go.]
160 
161  SideEffects [The input truth table is modified.]
162 
163  SeeAlso []
164 
165 ***********************************************************************/
166 void Kit_TruthStretch( unsigned * pOut, unsigned * pIn, int nVars, int nVarsAll, unsigned Phase, int fReturnIn )
167 {
168  unsigned * pTemp;
169  int i, k, Var = nVars - 1, Counter = 0;
170  for ( i = nVarsAll - 1; i >= 0; i-- )
171  if ( Phase & (1 << i) )
172  {
173  for ( k = Var; k < i; k++ )
174  {
175  Kit_TruthSwapAdjacentVars( pOut, pIn, nVarsAll, k );
176  pTemp = pIn; pIn = pOut; pOut = pTemp;
177  Counter++;
178  }
179  Var--;
180  }
181  assert( Var == -1 );
182  // swap if it was moved an even number of times
183  if ( fReturnIn ^ !(Counter & 1) )
184  Kit_TruthCopy( pOut, pIn, nVarsAll );
185 }
186 
187 /**Function*************************************************************
188 
189  Synopsis [Shrinks the truth table according to the phase.]
190 
191  Description [The input and output truth tables are in pIn/pOut. The current number
192  of variables is nVars. The total number of variables in nVarsAll. The last argument
193  (Phase) shows what variables should remain.]
194 
195  SideEffects [The input truth table is modified.]
196 
197  SeeAlso []
198 
199 ***********************************************************************/
200 void Kit_TruthShrink( unsigned * pOut, unsigned * pIn, int nVars, int nVarsAll, unsigned Phase, int fReturnIn )
201 {
202  unsigned * pTemp;
203  int i, k, Var = 0, Counter = 0;
204  for ( i = 0; i < nVarsAll; i++ )
205  if ( Phase & (1 << i) )
206  {
207  for ( k = i-1; k >= Var; k-- )
208  {
209  Kit_TruthSwapAdjacentVars( pOut, pIn, nVarsAll, k );
210  pTemp = pIn; pIn = pOut; pOut = pTemp;
211  Counter++;
212  }
213  Var++;
214  }
215  assert( Var == nVars );
216  // swap if it was moved an even number of times
217  if ( fReturnIn ^ !(Counter & 1) )
218  Kit_TruthCopy( pOut, pIn, nVarsAll );
219 }
220 
221 /**Function*************************************************************
222 
223  Synopsis [Implement give permutation.]
224 
225  Description [The input and output truth tables are in pIn/pOut.
226  The number of variables is nVars. Permutation is in pPerm.]
227 
228  SideEffects [The input truth table is modified.]
229 
230  SeeAlso []
231 
232 ***********************************************************************/
233 void Kit_TruthPermute( unsigned * pOut, unsigned * pIn, int nVars, char * pPerm, int fReturnIn )
234 {
235  unsigned * pTemp;
236  int i, Temp, fChange, Counter = 0;
237  do {
238  fChange = 0;
239  for ( i = 0; i < nVars-1; i++ )
240  {
241  assert( pPerm[i] != pPerm[i+1] );
242  if ( pPerm[i] <= pPerm[i+1] )
243  continue;
244  Counter++;
245  fChange = 1;
246 
247  Temp = pPerm[i];
248  pPerm[i] = pPerm[i+1];
249  pPerm[i+1] = Temp;
250 
251  Kit_TruthSwapAdjacentVars( pOut, pIn, nVars, i );
252  pTemp = pIn; pIn = pOut; pOut = pTemp;
253  }
254  } while ( fChange );
255  if ( fReturnIn ^ !(Counter & 1) )
256  Kit_TruthCopy( pOut, pIn, nVars );
257 }
258 
259 /**Function*************************************************************
260 
261  Synopsis [Returns 1 if TT depends on the given variable.]
262 
263  Description []
264 
265  SideEffects []
266 
267  SeeAlso []
268 
269 ***********************************************************************/
270 int Kit_TruthVarInSupport( unsigned * pTruth, int nVars, int iVar )
271 {
272  int nWords = Kit_TruthWordNum( nVars );
273  int i, k, Step;
274 
275  assert( iVar < nVars );
276  switch ( iVar )
277  {
278  case 0:
279  for ( i = 0; i < nWords; i++ )
280  if ( (pTruth[i] & 0x55555555) != ((pTruth[i] & 0xAAAAAAAA) >> 1) )
281  return 1;
282  return 0;
283  case 1:
284  for ( i = 0; i < nWords; i++ )
285  if ( (pTruth[i] & 0x33333333) != ((pTruth[i] & 0xCCCCCCCC) >> 2) )
286  return 1;
287  return 0;
288  case 2:
289  for ( i = 0; i < nWords; i++ )
290  if ( (pTruth[i] & 0x0F0F0F0F) != ((pTruth[i] & 0xF0F0F0F0) >> 4) )
291  return 1;
292  return 0;
293  case 3:
294  for ( i = 0; i < nWords; i++ )
295  if ( (pTruth[i] & 0x00FF00FF) != ((pTruth[i] & 0xFF00FF00) >> 8) )
296  return 1;
297  return 0;
298  case 4:
299  for ( i = 0; i < nWords; i++ )
300  if ( (pTruth[i] & 0x0000FFFF) != ((pTruth[i] & 0xFFFF0000) >> 16) )
301  return 1;
302  return 0;
303  default:
304  Step = (1 << (iVar - 5));
305  for ( k = 0; k < nWords; k += 2*Step )
306  {
307  for ( i = 0; i < Step; i++ )
308  if ( pTruth[i] != pTruth[Step+i] )
309  return 1;
310  pTruth += 2*Step;
311  }
312  return 0;
313  }
314 }
315 
316 /**Function*************************************************************
317 
318  Synopsis [Returns the number of support vars.]
319 
320  Description []
321 
322  SideEffects []
323 
324  SeeAlso []
325 
326 ***********************************************************************/
327 int Kit_TruthSupportSize( unsigned * pTruth, int nVars )
328 {
329  int i, Counter = 0;
330  for ( i = 0; i < nVars; i++ )
331  Counter += Kit_TruthVarInSupport( pTruth, nVars, i );
332  return Counter;
333 }
334 
335 /**Function*************************************************************
336 
337  Synopsis [Returns support of the function.]
338 
339  Description []
340 
341  SideEffects []
342 
343  SeeAlso []
344 
345 ***********************************************************************/
346 unsigned Kit_TruthSupport( unsigned * pTruth, int nVars )
347 {
348  int i, Support = 0;
349  for ( i = 0; i < nVars; i++ )
350  if ( Kit_TruthVarInSupport( pTruth, nVars, i ) )
351  Support |= (1 << i);
352  return Support;
353 }
354 
355 
356 
357 /**Function*************************************************************
358 
359  Synopsis [Computes negative cofactor of the function.]
360 
361  Description []
362 
363  SideEffects []
364 
365  SeeAlso []
366 
367 ***********************************************************************/
368 void Kit_TruthCofactor0( unsigned * pTruth, int nVars, int iVar )
369 {
370  int nWords = Kit_TruthWordNum( nVars );
371  int i, k, Step;
372 
373  assert( iVar < nVars );
374  switch ( iVar )
375  {
376  case 0:
377  for ( i = 0; i < nWords; i++ )
378  pTruth[i] = (pTruth[i] & 0x55555555) | ((pTruth[i] & 0x55555555) << 1);
379  return;
380  case 1:
381  for ( i = 0; i < nWords; i++ )
382  pTruth[i] = (pTruth[i] & 0x33333333) | ((pTruth[i] & 0x33333333) << 2);
383  return;
384  case 2:
385  for ( i = 0; i < nWords; i++ )
386  pTruth[i] = (pTruth[i] & 0x0F0F0F0F) | ((pTruth[i] & 0x0F0F0F0F) << 4);
387  return;
388  case 3:
389  for ( i = 0; i < nWords; i++ )
390  pTruth[i] = (pTruth[i] & 0x00FF00FF) | ((pTruth[i] & 0x00FF00FF) << 8);
391  return;
392  case 4:
393  for ( i = 0; i < nWords; i++ )
394  pTruth[i] = (pTruth[i] & 0x0000FFFF) | ((pTruth[i] & 0x0000FFFF) << 16);
395  return;
396  default:
397  Step = (1 << (iVar - 5));
398  for ( k = 0; k < nWords; k += 2*Step )
399  {
400  for ( i = 0; i < Step; i++ )
401  pTruth[Step+i] = pTruth[i];
402  pTruth += 2*Step;
403  }
404  return;
405  }
406 }
407 
408 /**Function*************************************************************
409 
410  Synopsis [Computes negative cofactor of the function.]
411 
412  Description []
413 
414  SideEffects []
415 
416  SeeAlso []
417 
418 ***********************************************************************/
419 int Kit_TruthCofactor0Count( unsigned * pTruth, int nVars, int iVar )
420 {
421  int nWords = Kit_TruthWordNum( nVars );
422  int i, k, Step, Counter = 0;
423 
424  assert( iVar < nVars );
425  switch ( iVar )
426  {
427  case 0:
428  for ( i = 0; i < nWords; i++ )
429  Counter += Kit_WordCountOnes(pTruth[i] & 0x55555555);
430  return Counter;
431  case 1:
432  for ( i = 0; i < nWords; i++ )
433  Counter += Kit_WordCountOnes(pTruth[i] & 0x33333333);
434  return Counter;
435  case 2:
436  for ( i = 0; i < nWords; i++ )
437  Counter += Kit_WordCountOnes(pTruth[i] & 0x0F0F0F0F);
438  return Counter;
439  case 3:
440  for ( i = 0; i < nWords; i++ )
441  Counter += Kit_WordCountOnes(pTruth[i] & 0x00FF00FF);
442  return Counter;
443  case 4:
444  for ( i = 0; i < nWords; i++ )
445  Counter += Kit_WordCountOnes(pTruth[i] & 0x0000FFFF);
446  return Counter;
447  default:
448  Step = (1 << (iVar - 5));
449  for ( k = 0; k < nWords; k += 2*Step )
450  {
451  for ( i = 0; i < Step; i++ )
452  Counter += Kit_WordCountOnes(pTruth[i]);
453  pTruth += 2*Step;
454  }
455  return Counter;
456  }
457 }
458 
459 /**Function*************************************************************
460 
461  Synopsis [Computes positive cofactor of the function.]
462 
463  Description []
464 
465  SideEffects []
466 
467  SeeAlso []
468 
469 ***********************************************************************/
470 void Kit_TruthCofactor1( unsigned * pTruth, int nVars, int iVar )
471 {
472  int nWords = Kit_TruthWordNum( nVars );
473  int i, k, Step;
474 
475  assert( iVar < nVars );
476  switch ( iVar )
477  {
478  case 0:
479  for ( i = 0; i < nWords; i++ )
480  pTruth[i] = (pTruth[i] & 0xAAAAAAAA) | ((pTruth[i] & 0xAAAAAAAA) >> 1);
481  return;
482  case 1:
483  for ( i = 0; i < nWords; i++ )
484  pTruth[i] = (pTruth[i] & 0xCCCCCCCC) | ((pTruth[i] & 0xCCCCCCCC) >> 2);
485  return;
486  case 2:
487  for ( i = 0; i < nWords; i++ )
488  pTruth[i] = (pTruth[i] & 0xF0F0F0F0) | ((pTruth[i] & 0xF0F0F0F0) >> 4);
489  return;
490  case 3:
491  for ( i = 0; i < nWords; i++ )
492  pTruth[i] = (pTruth[i] & 0xFF00FF00) | ((pTruth[i] & 0xFF00FF00) >> 8);
493  return;
494  case 4:
495  for ( i = 0; i < nWords; i++ )
496  pTruth[i] = (pTruth[i] & 0xFFFF0000) | ((pTruth[i] & 0xFFFF0000) >> 16);
497  return;
498  default:
499  Step = (1 << (iVar - 5));
500  for ( k = 0; k < nWords; k += 2*Step )
501  {
502  for ( i = 0; i < Step; i++ )
503  pTruth[i] = pTruth[Step+i];
504  pTruth += 2*Step;
505  }
506  return;
507  }
508 }
509 
510 /**Function*************************************************************
511 
512  Synopsis [Computes positive cofactor of the function.]
513 
514  Description []
515 
516  SideEffects []
517 
518  SeeAlso []
519 
520 ***********************************************************************/
521 void Kit_TruthCofactor0New( unsigned * pOut, unsigned * pIn, int nVars, int iVar )
522 {
523  int nWords = Kit_TruthWordNum( nVars );
524  int i, k, Step;
525 
526  assert( iVar < nVars );
527  switch ( iVar )
528  {
529  case 0:
530  for ( i = 0; i < nWords; i++ )
531  pOut[i] = (pIn[i] & 0x55555555) | ((pIn[i] & 0x55555555) << 1);
532  return;
533  case 1:
534  for ( i = 0; i < nWords; i++ )
535  pOut[i] = (pIn[i] & 0x33333333) | ((pIn[i] & 0x33333333) << 2);
536  return;
537  case 2:
538  for ( i = 0; i < nWords; i++ )
539  pOut[i] = (pIn[i] & 0x0F0F0F0F) | ((pIn[i] & 0x0F0F0F0F) << 4);
540  return;
541  case 3:
542  for ( i = 0; i < nWords; i++ )
543  pOut[i] = (pIn[i] & 0x00FF00FF) | ((pIn[i] & 0x00FF00FF) << 8);
544  return;
545  case 4:
546  for ( i = 0; i < nWords; i++ )
547  pOut[i] = (pIn[i] & 0x0000FFFF) | ((pIn[i] & 0x0000FFFF) << 16);
548  return;
549  default:
550  Step = (1 << (iVar - 5));
551  for ( k = 0; k < nWords; k += 2*Step )
552  {
553  for ( i = 0; i < Step; i++ )
554  pOut[i] = pOut[Step+i] = pIn[i];
555  pIn += 2*Step;
556  pOut += 2*Step;
557  }
558  return;
559  }
560 }
561 
562 /**Function*************************************************************
563 
564  Synopsis [Computes positive cofactor of the function.]
565 
566  Description []
567 
568  SideEffects []
569 
570  SeeAlso []
571 
572 ***********************************************************************/
573 void Kit_TruthCofactor1New( unsigned * pOut, unsigned * pIn, int nVars, int iVar )
574 {
575  int nWords = Kit_TruthWordNum( nVars );
576  int i, k, Step;
577 
578  assert( iVar < nVars );
579  switch ( iVar )
580  {
581  case 0:
582  for ( i = 0; i < nWords; i++ )
583  pOut[i] = (pIn[i] & 0xAAAAAAAA) | ((pIn[i] & 0xAAAAAAAA) >> 1);
584  return;
585  case 1:
586  for ( i = 0; i < nWords; i++ )
587  pOut[i] = (pIn[i] & 0xCCCCCCCC) | ((pIn[i] & 0xCCCCCCCC) >> 2);
588  return;
589  case 2:
590  for ( i = 0; i < nWords; i++ )
591  pOut[i] = (pIn[i] & 0xF0F0F0F0) | ((pIn[i] & 0xF0F0F0F0) >> 4);
592  return;
593  case 3:
594  for ( i = 0; i < nWords; i++ )
595  pOut[i] = (pIn[i] & 0xFF00FF00) | ((pIn[i] & 0xFF00FF00) >> 8);
596  return;
597  case 4:
598  for ( i = 0; i < nWords; i++ )
599  pOut[i] = (pIn[i] & 0xFFFF0000) | ((pIn[i] & 0xFFFF0000) >> 16);
600  return;
601  default:
602  Step = (1 << (iVar - 5));
603  for ( k = 0; k < nWords; k += 2*Step )
604  {
605  for ( i = 0; i < Step; i++ )
606  pOut[i] = pOut[Step+i] = pIn[Step+i];
607  pIn += 2*Step;
608  pOut += 2*Step;
609  }
610  return;
611  }
612 }
613 
614 /**Function*************************************************************
615 
616  Synopsis [Computes negative cofactor of the function.]
617 
618  Description []
619 
620  SideEffects []
621 
622  SeeAlso []
623 
624 ***********************************************************************/
625 int Kit_TruthVarIsVacuous( unsigned * pOnset, unsigned * pOffset, int nVars, int iVar )
626 {
627  int nWords = Kit_TruthWordNum( nVars );
628  int i, k, Step;
629 
630  assert( iVar < nVars );
631  switch ( iVar )
632  {
633  case 0:
634  for ( i = 0; i < nWords; i++ )
635  if ( ((pOnset[i] & (pOffset[i] >> 1)) | (pOffset[i] & (pOnset[i] >> 1))) & 0x55555555 )
636  return 0;
637  return 1;
638  case 1:
639  for ( i = 0; i < nWords; i++ )
640  if ( ((pOnset[i] & (pOffset[i] >> 2)) | (pOffset[i] & (pOnset[i] >> 2))) & 0x33333333 )
641  return 0;
642  return 1;
643  case 2:
644  for ( i = 0; i < nWords; i++ )
645  if ( ((pOnset[i] & (pOffset[i] >> 4)) | (pOffset[i] & (pOnset[i] >> 4))) & 0x0F0F0F0F )
646  return 0;
647  return 1;
648  case 3:
649  for ( i = 0; i < nWords; i++ )
650  if ( ((pOnset[i] & (pOffset[i] >> 8)) | (pOffset[i] & (pOnset[i] >> 8))) & 0x00FF00FF )
651  return 0;
652  return 1;
653  case 4:
654  for ( i = 0; i < nWords; i++ )
655  if ( ((pOnset[i] & (pOffset[i] >> 16)) | (pOffset[i] & (pOnset[i] >> 16))) & 0x0000FFFF )
656  return 0;
657  return 1;
658  default:
659  Step = (1 << (iVar - 5));
660  for ( k = 0; k < nWords; k += 2*Step )
661  {
662  for ( i = 0; i < Step; i++ )
663  if ( (pOnset[i] & pOffset[Step+i]) | (pOffset[i] & pOnset[Step+i]) )
664  return 0;
665  pOnset += 2*Step;
666  pOffset += 2*Step;
667  }
668  return 1;
669  }
670 }
671 
672 
673 /**Function*************************************************************
674 
675  Synopsis [Existentially quantifies the variable.]
676 
677  Description []
678 
679  SideEffects []
680 
681  SeeAlso []
682 
683 ***********************************************************************/
684 void Kit_TruthExist( unsigned * pTruth, int nVars, int iVar )
685 {
686  int nWords = Kit_TruthWordNum( nVars );
687  int i, k, Step;
688 
689  assert( iVar < nVars );
690  switch ( iVar )
691  {
692  case 0:
693  for ( i = 0; i < nWords; i++ )
694  pTruth[i] |= ((pTruth[i] & 0xAAAAAAAA) >> 1) | ((pTruth[i] & 0x55555555) << 1);
695  return;
696  case 1:
697  for ( i = 0; i < nWords; i++ )
698  pTruth[i] |= ((pTruth[i] & 0xCCCCCCCC) >> 2) | ((pTruth[i] & 0x33333333) << 2);
699  return;
700  case 2:
701  for ( i = 0; i < nWords; i++ )
702  pTruth[i] |= ((pTruth[i] & 0xF0F0F0F0) >> 4) | ((pTruth[i] & 0x0F0F0F0F) << 4);
703  return;
704  case 3:
705  for ( i = 0; i < nWords; i++ )
706  pTruth[i] |= ((pTruth[i] & 0xFF00FF00) >> 8) | ((pTruth[i] & 0x00FF00FF) << 8);
707  return;
708  case 4:
709  for ( i = 0; i < nWords; i++ )
710  pTruth[i] |= ((pTruth[i] & 0xFFFF0000) >> 16) | ((pTruth[i] & 0x0000FFFF) << 16);
711  return;
712  default:
713  Step = (1 << (iVar - 5));
714  for ( k = 0; k < nWords; k += 2*Step )
715  {
716  for ( i = 0; i < Step; i++ )
717  {
718  pTruth[i] |= pTruth[Step+i];
719  pTruth[Step+i] = pTruth[i];
720  }
721  pTruth += 2*Step;
722  }
723  return;
724  }
725 }
726 
727 /**Function*************************************************************
728 
729  Synopsis [Existentially quantifies the variable.]
730 
731  Description []
732 
733  SideEffects []
734 
735  SeeAlso []
736 
737 ***********************************************************************/
738 void Kit_TruthExistNew( unsigned * pRes, unsigned * pTruth, int nVars, int iVar )
739 {
740  int nWords = Kit_TruthWordNum( nVars );
741  int i, k, Step;
742 
743  assert( iVar < nVars );
744  switch ( iVar )
745  {
746  case 0:
747  for ( i = 0; i < nWords; i++ )
748  pRes[i] = pTruth[i] | ((pTruth[i] & 0xAAAAAAAA) >> 1) | ((pTruth[i] & 0x55555555) << 1);
749  return;
750  case 1:
751  for ( i = 0; i < nWords; i++ )
752  pRes[i] = pTruth[i] | ((pTruth[i] & 0xCCCCCCCC) >> 2) | ((pTruth[i] & 0x33333333) << 2);
753  return;
754  case 2:
755  for ( i = 0; i < nWords; i++ )
756  pRes[i] = pTruth[i] | ((pTruth[i] & 0xF0F0F0F0) >> 4) | ((pTruth[i] & 0x0F0F0F0F) << 4);
757  return;
758  case 3:
759  for ( i = 0; i < nWords; i++ )
760  pRes[i] = pTruth[i] | ((pTruth[i] & 0xFF00FF00) >> 8) | ((pTruth[i] & 0x00FF00FF) << 8);
761  return;
762  case 4:
763  for ( i = 0; i < nWords; i++ )
764  pRes[i] = pTruth[i] | ((pTruth[i] & 0xFFFF0000) >> 16) | ((pTruth[i] & 0x0000FFFF) << 16);
765  return;
766  default:
767  Step = (1 << (iVar - 5));
768  for ( k = 0; k < nWords; k += 2*Step )
769  {
770  for ( i = 0; i < Step; i++ )
771  {
772  pRes[i] = pTruth[i] | pTruth[Step+i];
773  pRes[Step+i] = pRes[i];
774  }
775  pRes += 2*Step;
776  pTruth += 2*Step;
777  }
778  return;
779  }
780 }
781 
782 /**Function*************************************************************
783 
784  Synopsis [Existantially quantifies the set of variables.]
785 
786  Description []
787 
788  SideEffects []
789 
790  SeeAlso []
791 
792 ***********************************************************************/
793 void Kit_TruthExistSet( unsigned * pRes, unsigned * pTruth, int nVars, unsigned uMask )
794 {
795  int v;
796  Kit_TruthCopy( pRes, pTruth, nVars );
797  for ( v = 0; v < nVars; v++ )
798  if ( uMask & (1 << v) )
799  Kit_TruthExist( pRes, nVars, v );
800 }
801 
802 /**Function*************************************************************
803 
804  Synopsis [Unversally quantifies the variable.]
805 
806  Description []
807 
808  SideEffects []
809 
810  SeeAlso []
811 
812 ***********************************************************************/
813 void Kit_TruthForall( unsigned * pTruth, int nVars, int iVar )
814 {
815  int nWords = Kit_TruthWordNum( nVars );
816  int i, k, Step;
817 
818  assert( iVar < nVars );
819  switch ( iVar )
820  {
821  case 0:
822  for ( i = 0; i < nWords; i++ )
823  pTruth[i] &= ((pTruth[i] & 0xAAAAAAAA) >> 1) | ((pTruth[i] & 0x55555555) << 1);
824  return;
825  case 1:
826  for ( i = 0; i < nWords; i++ )
827  pTruth[i] &= ((pTruth[i] & 0xCCCCCCCC) >> 2) | ((pTruth[i] & 0x33333333) << 2);
828  return;
829  case 2:
830  for ( i = 0; i < nWords; i++ )
831  pTruth[i] &= ((pTruth[i] & 0xF0F0F0F0) >> 4) | ((pTruth[i] & 0x0F0F0F0F) << 4);
832  return;
833  case 3:
834  for ( i = 0; i < nWords; i++ )
835  pTruth[i] &= ((pTruth[i] & 0xFF00FF00) >> 8) | ((pTruth[i] & 0x00FF00FF) << 8);
836  return;
837  case 4:
838  for ( i = 0; i < nWords; i++ )
839  pTruth[i] &= ((pTruth[i] & 0xFFFF0000) >> 16) | ((pTruth[i] & 0x0000FFFF) << 16);
840  return;
841  default:
842  Step = (1 << (iVar - 5));
843  for ( k = 0; k < nWords; k += 2*Step )
844  {
845  for ( i = 0; i < Step; i++ )
846  {
847  pTruth[i] &= pTruth[Step+i];
848  pTruth[Step+i] = pTruth[i];
849  }
850  pTruth += 2*Step;
851  }
852  return;
853  }
854 }
855 
856 /**Function*************************************************************
857 
858  Synopsis [Universally quantifies the variable.]
859 
860  Description []
861 
862  SideEffects []
863 
864  SeeAlso []
865 
866 ***********************************************************************/
867 void Kit_TruthForallNew( unsigned * pRes, unsigned * pTruth, int nVars, int iVar )
868 {
869  int nWords = Kit_TruthWordNum( nVars );
870  int i, k, Step;
871 
872  assert( iVar < nVars );
873  switch ( iVar )
874  {
875  case 0:
876  for ( i = 0; i < nWords; i++ )
877  pRes[i] = pTruth[i] & (((pTruth[i] & 0xAAAAAAAA) >> 1) | ((pTruth[i] & 0x55555555) << 1));
878  return;
879  case 1:
880  for ( i = 0; i < nWords; i++ )
881  pRes[i] = pTruth[i] & (((pTruth[i] & 0xCCCCCCCC) >> 2) | ((pTruth[i] & 0x33333333) << 2));
882  return;
883  case 2:
884  for ( i = 0; i < nWords; i++ )
885  pRes[i] = pTruth[i] & (((pTruth[i] & 0xF0F0F0F0) >> 4) | ((pTruth[i] & 0x0F0F0F0F) << 4));
886  return;
887  case 3:
888  for ( i = 0; i < nWords; i++ )
889  pRes[i] = pTruth[i] & (((pTruth[i] & 0xFF00FF00) >> 8) | ((pTruth[i] & 0x00FF00FF) << 8));
890  return;
891  case 4:
892  for ( i = 0; i < nWords; i++ )
893  pRes[i] = pTruth[i] & (((pTruth[i] & 0xFFFF0000) >> 16) | ((pTruth[i] & 0x0000FFFF) << 16));
894  return;
895  default:
896  Step = (1 << (iVar - 5));
897  for ( k = 0; k < nWords; k += 2*Step )
898  {
899  for ( i = 0; i < Step; i++ )
900  {
901  pRes[i] = pTruth[i] & pTruth[Step+i];
902  pRes[Step+i] = pRes[i];
903  }
904  pRes += 2*Step;
905  pTruth += 2*Step;
906  }
907  return;
908  }
909 }
910 
911 /**Function*************************************************************
912 
913  Synopsis [Universally quantifies the variable.]
914 
915  Description []
916 
917  SideEffects []
918 
919  SeeAlso []
920 
921 ***********************************************************************/
922 void Kit_TruthUniqueNew( unsigned * pRes, unsigned * pTruth, int nVars, int iVar )
923 {
924  int nWords = Kit_TruthWordNum( nVars );
925  int i, k, Step;
926 
927  assert( iVar < nVars );
928  switch ( iVar )
929  {
930  case 0:
931  for ( i = 0; i < nWords; i++ )
932  pRes[i] = pTruth[i] ^ (((pTruth[i] & 0xAAAAAAAA) >> 1) | ((pTruth[i] & 0x55555555) << 1));
933  return;
934  case 1:
935  for ( i = 0; i < nWords; i++ )
936  pRes[i] = pTruth[i] ^ (((pTruth[i] & 0xCCCCCCCC) >> 2) | ((pTruth[i] & 0x33333333) << 2));
937  return;
938  case 2:
939  for ( i = 0; i < nWords; i++ )
940  pRes[i] = pTruth[i] ^ (((pTruth[i] & 0xF0F0F0F0) >> 4) | ((pTruth[i] & 0x0F0F0F0F) << 4));
941  return;
942  case 3:
943  for ( i = 0; i < nWords; i++ )
944  pRes[i] = pTruth[i] ^ (((pTruth[i] & 0xFF00FF00) >> 8) | ((pTruth[i] & 0x00FF00FF) << 8));
945  return;
946  case 4:
947  for ( i = 0; i < nWords; i++ )
948  pRes[i] = pTruth[i] ^ (((pTruth[i] & 0xFFFF0000) >> 16) | ((pTruth[i] & 0x0000FFFF) << 16));
949  return;
950  default:
951  Step = (1 << (iVar - 5));
952  for ( k = 0; k < nWords; k += 2*Step )
953  {
954  for ( i = 0; i < Step; i++ )
955  {
956  pRes[i] = pTruth[i] ^ pTruth[Step+i];
957  pRes[Step+i] = pRes[i];
958  }
959  pRes += 2*Step;
960  pTruth += 2*Step;
961  }
962  return;
963  }
964 }
965 
966 /**Function*************************************************************
967 
968  Synopsis [Returns the number of minterms in the Boolean difference.]
969 
970  Description []
971 
972  SideEffects []
973 
974  SeeAlso []
975 
976 ***********************************************************************/
977 int Kit_TruthBooleanDiffCount( unsigned * pTruth, int nVars, int iVar )
978 {
979  int nWords = Kit_TruthWordNum( nVars );
980  int i, k, Step, Counter = 0;
981 
982  assert( iVar < nVars );
983  switch ( iVar )
984  {
985  case 0:
986  for ( i = 0; i < nWords; i++ )
987  Counter += Kit_WordCountOnes( (pTruth[i] ^ (pTruth[i] >> 1)) & 0x55555555 );
988  return Counter;
989  case 1:
990  for ( i = 0; i < nWords; i++ )
991  Counter += Kit_WordCountOnes( (pTruth[i] ^ (pTruth[i] >> 2)) & 0x33333333 );
992  return Counter;
993  case 2:
994  for ( i = 0; i < nWords; i++ )
995  Counter += Kit_WordCountOnes( (pTruth[i] ^ (pTruth[i] >> 4)) & 0x0F0F0F0F );
996  return Counter;
997  case 3:
998  for ( i = 0; i < nWords; i++ )
999  Counter += Kit_WordCountOnes( (pTruth[i] ^ (pTruth[i] >> 8)) & 0x00FF00FF );
1000  return Counter;
1001  case 4:
1002  for ( i = 0; i < nWords; i++ )
1003  Counter += Kit_WordCountOnes( (pTruth[i] ^ (pTruth[i] >>16)) & 0x0000FFFF );
1004  return Counter;
1005  default:
1006  Step = (1 << (iVar - 5));
1007  for ( k = 0; k < nWords; k += 2*Step )
1008  {
1009  for ( i = 0; i < Step; i++ )
1010  Counter += Kit_WordCountOnes( pTruth[i] ^ pTruth[Step+i] );
1011  pTruth += 2*Step;
1012  }
1013  return Counter;
1014  }
1015 }
1016 
1017 /**Function*************************************************************
1018 
1019  Synopsis [Returns the number of minterms in the Boolean difference.]
1020 
1021  Description []
1022 
1023  SideEffects []
1024 
1025  SeeAlso []
1026 
1027 ***********************************************************************/
1028 int Kit_TruthXorCount( unsigned * pTruth0, unsigned * pTruth1, int nVars )
1029 {
1030  int nWords = Kit_TruthWordNum( nVars );
1031  int i, Counter = 0;
1032  for ( i = 0; i < nWords; i++ )
1033  Counter += Kit_WordCountOnes( pTruth0[i] ^ pTruth1[i] );
1034  return Counter;
1035 }
1036 
1037 /**Function*************************************************************
1038 
1039  Synopsis [Universally quantifies the set of variables.]
1040 
1041  Description []
1042 
1043  SideEffects []
1044 
1045  SeeAlso []
1046 
1047 ***********************************************************************/
1048 void Kit_TruthForallSet( unsigned * pRes, unsigned * pTruth, int nVars, unsigned uMask )
1049 {
1050  int v;
1051  Kit_TruthCopy( pRes, pTruth, nVars );
1052  for ( v = 0; v < nVars; v++ )
1053  if ( uMask & (1 << v) )
1054  Kit_TruthForall( pRes, nVars, v );
1055 }
1056 
1057 
1058 /**Function*************************************************************
1059 
1060  Synopsis [Multiplexes two functions with the given variable.]
1061 
1062  Description []
1063 
1064  SideEffects []
1065 
1066  SeeAlso []
1067 
1068 ***********************************************************************/
1069 void Kit_TruthMuxVar( unsigned * pOut, unsigned * pCof0, unsigned * pCof1, int nVars, int iVar )
1070 {
1071  int nWords = Kit_TruthWordNum( nVars );
1072  int i, k, Step;
1073 
1074  assert( iVar < nVars );
1075  switch ( iVar )
1076  {
1077  case 0:
1078  for ( i = 0; i < nWords; i++ )
1079  pOut[i] = (pCof0[i] & 0x55555555) | (pCof1[i] & 0xAAAAAAAA);
1080  return;
1081  case 1:
1082  for ( i = 0; i < nWords; i++ )
1083  pOut[i] = (pCof0[i] & 0x33333333) | (pCof1[i] & 0xCCCCCCCC);
1084  return;
1085  case 2:
1086  for ( i = 0; i < nWords; i++ )
1087  pOut[i] = (pCof0[i] & 0x0F0F0F0F) | (pCof1[i] & 0xF0F0F0F0);
1088  return;
1089  case 3:
1090  for ( i = 0; i < nWords; i++ )
1091  pOut[i] = (pCof0[i] & 0x00FF00FF) | (pCof1[i] & 0xFF00FF00);
1092  return;
1093  case 4:
1094  for ( i = 0; i < nWords; i++ )
1095  pOut[i] = (pCof0[i] & 0x0000FFFF) | (pCof1[i] & 0xFFFF0000);
1096  return;
1097  default:
1098  Step = (1 << (iVar - 5));
1099  for ( k = 0; k < nWords; k += 2*Step )
1100  {
1101  for ( i = 0; i < Step; i++ )
1102  {
1103  pOut[i] = pCof0[i];
1104  pOut[Step+i] = pCof1[Step+i];
1105  }
1106  pOut += 2*Step;
1107  pCof0 += 2*Step;
1108  pCof1 += 2*Step;
1109  }
1110  return;
1111  }
1112 }
1113 
1114 /**Function*************************************************************
1115 
1116  Synopsis [Multiplexes two functions with the given variable.]
1117 
1118  Description []
1119 
1120  SideEffects []
1121 
1122  SeeAlso []
1123 
1124 ***********************************************************************/
1125 void Kit_TruthMuxVarPhase( unsigned * pOut, unsigned * pCof0, unsigned * pCof1, int nVars, int iVar, int fCompl0 )
1126 {
1127  int nWords = Kit_TruthWordNum( nVars );
1128  int i, k, Step;
1129 
1130  if ( fCompl0 == 0 )
1131  {
1132  Kit_TruthMuxVar( pOut, pCof0, pCof1, nVars, iVar );
1133  return;
1134  }
1135 
1136  assert( iVar < nVars );
1137  switch ( iVar )
1138  {
1139  case 0:
1140  for ( i = 0; i < nWords; i++ )
1141  pOut[i] = (~pCof0[i] & 0x55555555) | (pCof1[i] & 0xAAAAAAAA);
1142  return;
1143  case 1:
1144  for ( i = 0; i < nWords; i++ )
1145  pOut[i] = (~pCof0[i] & 0x33333333) | (pCof1[i] & 0xCCCCCCCC);
1146  return;
1147  case 2:
1148  for ( i = 0; i < nWords; i++ )
1149  pOut[i] = (~pCof0[i] & 0x0F0F0F0F) | (pCof1[i] & 0xF0F0F0F0);
1150  return;
1151  case 3:
1152  for ( i = 0; i < nWords; i++ )
1153  pOut[i] = (~pCof0[i] & 0x00FF00FF) | (pCof1[i] & 0xFF00FF00);
1154  return;
1155  case 4:
1156  for ( i = 0; i < nWords; i++ )
1157  pOut[i] = (~pCof0[i] & 0x0000FFFF) | (pCof1[i] & 0xFFFF0000);
1158  return;
1159  default:
1160  Step = (1 << (iVar - 5));
1161  for ( k = 0; k < nWords; k += 2*Step )
1162  {
1163  for ( i = 0; i < Step; i++ )
1164  {
1165  pOut[i] = ~pCof0[i];
1166  pOut[Step+i] = pCof1[Step+i];
1167  }
1168  pOut += 2*Step;
1169  pCof0 += 2*Step;
1170  pCof1 += 2*Step;
1171  }
1172  return;
1173  }
1174 }
1175 
1176 /**Function*************************************************************
1177 
1178  Synopsis [Checks symmetry of two variables.]
1179 
1180  Description []
1181 
1182  SideEffects []
1183 
1184  SeeAlso []
1185 
1186 ***********************************************************************/
1187 int Kit_TruthVarsSymm( unsigned * pTruth, int nVars, int iVar0, int iVar1, unsigned * pCof0, unsigned * pCof1 )
1188 {
1189  static unsigned uTemp0[32], uTemp1[32];
1190  if ( pCof0 == NULL )
1191  {
1192  assert( nVars <= 10 );
1193  pCof0 = uTemp0;
1194  }
1195  if ( pCof1 == NULL )
1196  {
1197  assert( nVars <= 10 );
1198  pCof1 = uTemp1;
1199  }
1200  // compute Cof01
1201  Kit_TruthCopy( pCof0, pTruth, nVars );
1202  Kit_TruthCofactor0( pCof0, nVars, iVar0 );
1203  Kit_TruthCofactor1( pCof0, nVars, iVar1 );
1204  // compute Cof10
1205  Kit_TruthCopy( pCof1, pTruth, nVars );
1206  Kit_TruthCofactor1( pCof1, nVars, iVar0 );
1207  Kit_TruthCofactor0( pCof1, nVars, iVar1 );
1208  // compare
1209  return Kit_TruthIsEqual( pCof0, pCof1, nVars );
1210 }
1211 
1212 /**Function*************************************************************
1213 
1214  Synopsis [Checks antisymmetry of two variables.]
1215 
1216  Description []
1217 
1218  SideEffects []
1219 
1220  SeeAlso []
1221 
1222 ***********************************************************************/
1223 int Kit_TruthVarsAntiSymm( unsigned * pTruth, int nVars, int iVar0, int iVar1, unsigned * pCof0, unsigned * pCof1 )
1224 {
1225  static unsigned uTemp0[32], uTemp1[32];
1226  if ( pCof0 == NULL )
1227  {
1228  assert( nVars <= 10 );
1229  pCof0 = uTemp0;
1230  }
1231  if ( pCof1 == NULL )
1232  {
1233  assert( nVars <= 10 );
1234  pCof1 = uTemp1;
1235  }
1236  // compute Cof00
1237  Kit_TruthCopy( pCof0, pTruth, nVars );
1238  Kit_TruthCofactor0( pCof0, nVars, iVar0 );
1239  Kit_TruthCofactor0( pCof0, nVars, iVar1 );
1240  // compute Cof11
1241  Kit_TruthCopy( pCof1, pTruth, nVars );
1242  Kit_TruthCofactor1( pCof1, nVars, iVar0 );
1243  Kit_TruthCofactor1( pCof1, nVars, iVar1 );
1244  // compare
1245  return Kit_TruthIsEqual( pCof0, pCof1, nVars );
1246 }
1247 
1248 /**Function*************************************************************
1249 
1250  Synopsis [Changes phase of the function w.r.t. one variable.]
1251 
1252  Description []
1253 
1254  SideEffects []
1255 
1256  SeeAlso []
1257 
1258 ***********************************************************************/
1259 void Kit_TruthChangePhase( unsigned * pTruth, int nVars, int iVar )
1260 {
1261  int nWords = Kit_TruthWordNum( nVars );
1262  int i, k, Step;
1263  unsigned Temp;
1264 
1265  assert( iVar < nVars );
1266  switch ( iVar )
1267  {
1268  case 0:
1269  for ( i = 0; i < nWords; i++ )
1270  pTruth[i] = ((pTruth[i] & 0x55555555) << 1) | ((pTruth[i] & 0xAAAAAAAA) >> 1);
1271  return;
1272  case 1:
1273  for ( i = 0; i < nWords; i++ )
1274  pTruth[i] = ((pTruth[i] & 0x33333333) << 2) | ((pTruth[i] & 0xCCCCCCCC) >> 2);
1275  return;
1276  case 2:
1277  for ( i = 0; i < nWords; i++ )
1278  pTruth[i] = ((pTruth[i] & 0x0F0F0F0F) << 4) | ((pTruth[i] & 0xF0F0F0F0) >> 4);
1279  return;
1280  case 3:
1281  for ( i = 0; i < nWords; i++ )
1282  pTruth[i] = ((pTruth[i] & 0x00FF00FF) << 8) | ((pTruth[i] & 0xFF00FF00) >> 8);
1283  return;
1284  case 4:
1285  for ( i = 0; i < nWords; i++ )
1286  pTruth[i] = ((pTruth[i] & 0x0000FFFF) << 16) | ((pTruth[i] & 0xFFFF0000) >> 16);
1287  return;
1288  default:
1289  Step = (1 << (iVar - 5));
1290  for ( k = 0; k < nWords; k += 2*Step )
1291  {
1292  for ( i = 0; i < Step; i++ )
1293  {
1294  Temp = pTruth[i];
1295  pTruth[i] = pTruth[Step+i];
1296  pTruth[Step+i] = Temp;
1297  }
1298  pTruth += 2*Step;
1299  }
1300  return;
1301  }
1302 }
1303 
1304 /**Function*************************************************************
1305 
1306  Synopsis [Computes minimum overlap in supports of cofactors.]
1307 
1308  Description []
1309 
1310  SideEffects []
1311 
1312  SeeAlso []
1313 
1314 ***********************************************************************/
1315 int Kit_TruthMinCofSuppOverlap( unsigned * pTruth, int nVars, int * pVarMin )
1316 {
1317  static unsigned uCofactor[16];
1318  int i, ValueCur, ValueMin, VarMin;
1319  unsigned uSupp0, uSupp1;
1320  int nVars0, nVars1;
1321  assert( nVars <= 9 );
1322  ValueMin = 32;
1323  VarMin = -1;
1324  for ( i = 0; i < nVars; i++ )
1325  {
1326  // get negative cofactor
1327  Kit_TruthCopy( uCofactor, pTruth, nVars );
1328  Kit_TruthCofactor0( uCofactor, nVars, i );
1329  uSupp0 = Kit_TruthSupport( uCofactor, nVars );
1330  nVars0 = Kit_WordCountOnes( uSupp0 );
1331 //Kit_PrintBinary( stdout, &uSupp0, 8 ); printf( "\n" );
1332  // get positive cofactor
1333  Kit_TruthCopy( uCofactor, pTruth, nVars );
1334  Kit_TruthCofactor1( uCofactor, nVars, i );
1335  uSupp1 = Kit_TruthSupport( uCofactor, nVars );
1336  nVars1 = Kit_WordCountOnes( uSupp1 );
1337 //Kit_PrintBinary( stdout, &uSupp1, 8 ); printf( "\n" );
1338  // get the number of common vars
1339  ValueCur = Kit_WordCountOnes( uSupp0 & uSupp1 );
1340  if ( ValueMin > ValueCur && nVars0 <= 5 && nVars1 <= 5 )
1341  {
1342  ValueMin = ValueCur;
1343  VarMin = i;
1344  }
1345  if ( ValueMin == 0 )
1346  break;
1347  }
1348  if ( pVarMin )
1349  *pVarMin = VarMin;
1350  return ValueMin;
1351 }
1352 
1353 
1354 /**Function*************************************************************
1355 
1356  Synopsis [Find the best cofactoring variable.]
1357 
1358  Description []
1359 
1360  SideEffects []
1361 
1362  SeeAlso []
1363 
1364 ***********************************************************************/
1365 int Kit_TruthBestCofVar( unsigned * pTruth, int nVars, unsigned * pCof0, unsigned * pCof1 )
1366 {
1367  int i, iBestVar, nSuppSizeCur0, nSuppSizeCur1, nSuppSizeCur, nSuppSizeMin;
1368  if ( Kit_TruthIsConst0(pTruth, nVars) || Kit_TruthIsConst1(pTruth, nVars) )
1369  return -1;
1370  // iterate through variables
1371  iBestVar = -1;
1372  nSuppSizeMin = KIT_INFINITY;
1373  for ( i = 0; i < nVars; i++ )
1374  {
1375  // cofactor the functiona and get support sizes
1376  Kit_TruthCofactor0New( pCof0, pTruth, nVars, i );
1377  Kit_TruthCofactor1New( pCof1, pTruth, nVars, i );
1378  nSuppSizeCur0 = Kit_TruthSupportSize( pCof0, nVars );
1379  nSuppSizeCur1 = Kit_TruthSupportSize( pCof1, nVars );
1380  nSuppSizeCur = nSuppSizeCur0 + nSuppSizeCur1;
1381  // compare this variable with other variables
1382  if ( nSuppSizeMin > nSuppSizeCur )
1383  {
1384  nSuppSizeMin = nSuppSizeCur;
1385  iBestVar = i;
1386  }
1387  }
1388  assert( iBestVar != -1 );
1389  // cofactor w.r.t. this variable
1390  Kit_TruthCofactor0New( pCof0, pTruth, nVars, iBestVar );
1391  Kit_TruthCofactor1New( pCof1, pTruth, nVars, iBestVar );
1392  return iBestVar;
1393 }
1394 
1395 
1396 /**Function*************************************************************
1397 
1398  Synopsis [Counts the number of 1's in each cofactor.]
1399 
1400  Description [The resulting numbers are stored in the array of ints,
1401  whose length is 2*nVars. The number of 1's is counted in a different
1402  space than the original function. For example, if the function depends
1403  on k variables, the cofactors are assumed to depend on k-1 variables.]
1404 
1405  SideEffects []
1406 
1407  SeeAlso []
1408 
1409 ***********************************************************************/
1410 void Kit_TruthCountOnesInCofs( unsigned * pTruth, int nVars, int * pStore )
1411 {
1412  int nWords = Kit_TruthWordNum( nVars );
1413  int i, k, Counter;
1414  memset( pStore, 0, sizeof(int) * 2 * nVars );
1415  if ( nVars <= 5 )
1416  {
1417  if ( nVars > 0 )
1418  {
1419  pStore[2*0+0] = Kit_WordCountOnes( pTruth[0] & 0x55555555 );
1420  pStore[2*0+1] = Kit_WordCountOnes( pTruth[0] & 0xAAAAAAAA );
1421  }
1422  if ( nVars > 1 )
1423  {
1424  pStore[2*1+0] = Kit_WordCountOnes( pTruth[0] & 0x33333333 );
1425  pStore[2*1+1] = Kit_WordCountOnes( pTruth[0] & 0xCCCCCCCC );
1426  }
1427  if ( nVars > 2 )
1428  {
1429  pStore[2*2+0] = Kit_WordCountOnes( pTruth[0] & 0x0F0F0F0F );
1430  pStore[2*2+1] = Kit_WordCountOnes( pTruth[0] & 0xF0F0F0F0 );
1431  }
1432  if ( nVars > 3 )
1433  {
1434  pStore[2*3+0] = Kit_WordCountOnes( pTruth[0] & 0x00FF00FF );
1435  pStore[2*3+1] = Kit_WordCountOnes( pTruth[0] & 0xFF00FF00 );
1436  }
1437  if ( nVars > 4 )
1438  {
1439  pStore[2*4+0] = Kit_WordCountOnes( pTruth[0] & 0x0000FFFF );
1440  pStore[2*4+1] = Kit_WordCountOnes( pTruth[0] & 0xFFFF0000 );
1441  }
1442  return;
1443  }
1444  // nVars >= 6
1445  // count 1's for all other variables
1446  for ( k = 0; k < nWords; k++ )
1447  {
1448  Counter = Kit_WordCountOnes( pTruth[k] );
1449  for ( i = 5; i < nVars; i++ )
1450  if ( k & (1 << (i-5)) )
1451  pStore[2*i+1] += Counter;
1452  else
1453  pStore[2*i+0] += Counter;
1454  }
1455  // count 1's for the first five variables
1456  for ( k = 0; k < nWords/2; k++ )
1457  {
1458  pStore[2*0+0] += Kit_WordCountOnes( (pTruth[0] & 0x55555555) | ((pTruth[1] & 0x55555555) << 1) );
1459  pStore[2*0+1] += Kit_WordCountOnes( (pTruth[0] & 0xAAAAAAAA) | ((pTruth[1] & 0xAAAAAAAA) >> 1) );
1460  pStore[2*1+0] += Kit_WordCountOnes( (pTruth[0] & 0x33333333) | ((pTruth[1] & 0x33333333) << 2) );
1461  pStore[2*1+1] += Kit_WordCountOnes( (pTruth[0] & 0xCCCCCCCC) | ((pTruth[1] & 0xCCCCCCCC) >> 2) );
1462  pStore[2*2+0] += Kit_WordCountOnes( (pTruth[0] & 0x0F0F0F0F) | ((pTruth[1] & 0x0F0F0F0F) << 4) );
1463  pStore[2*2+1] += Kit_WordCountOnes( (pTruth[0] & 0xF0F0F0F0) | ((pTruth[1] & 0xF0F0F0F0) >> 4) );
1464  pStore[2*3+0] += Kit_WordCountOnes( (pTruth[0] & 0x00FF00FF) | ((pTruth[1] & 0x00FF00FF) << 8) );
1465  pStore[2*3+1] += Kit_WordCountOnes( (pTruth[0] & 0xFF00FF00) | ((pTruth[1] & 0xFF00FF00) >> 8) );
1466  pStore[2*4+0] += Kit_WordCountOnes( (pTruth[0] & 0x0000FFFF) | ((pTruth[1] & 0x0000FFFF) << 16) );
1467  pStore[2*4+1] += Kit_WordCountOnes( (pTruth[0] & 0xFFFF0000) | ((pTruth[1] & 0xFFFF0000) >> 16) );
1468  pTruth += 2;
1469  }
1470 }
1471 
1472 /**Function*************************************************************
1473 
1474  Synopsis [Counts the number of 1's in each negative cofactor.]
1475 
1476  Description [The resulting numbers are stored in the array of ints,
1477  whose length is nVars. The number of 1's is counted in a different
1478  space than the original function. For example, if the function depends
1479  on k variables, the cofactors are assumed to depend on k-1 variables.]
1480 
1481  SideEffects []
1482 
1483  SeeAlso []
1484 
1485 ***********************************************************************/
1486 void Kit_TruthCountOnesInCofs0( unsigned * pTruth, int nVars, int * pStore )
1487 {
1488  int nWords = Kit_TruthWordNum( nVars );
1489  int i, k, Counter;
1490  memset( pStore, 0, sizeof(int) * nVars );
1491  if ( nVars <= 5 )
1492  {
1493  if ( nVars > 0 )
1494  pStore[0] = Kit_WordCountOnes( pTruth[0] & 0x55555555 );
1495  if ( nVars > 1 )
1496  pStore[1] = Kit_WordCountOnes( pTruth[0] & 0x33333333 );
1497  if ( nVars > 2 )
1498  pStore[2] = Kit_WordCountOnes( pTruth[0] & 0x0F0F0F0F );
1499  if ( nVars > 3 )
1500  pStore[3] = Kit_WordCountOnes( pTruth[0] & 0x00FF00FF );
1501  if ( nVars > 4 )
1502  pStore[4] = Kit_WordCountOnes( pTruth[0] & 0x0000FFFF );
1503  return;
1504  }
1505  // nVars >= 6
1506  // count 1's for all other variables
1507  for ( k = 0; k < nWords; k++ )
1508  {
1509  Counter = Kit_WordCountOnes( pTruth[k] );
1510  for ( i = 5; i < nVars; i++ )
1511  if ( (k & (1 << (i-5))) == 0 )
1512  pStore[i] += Counter;
1513  }
1514  // count 1's for the first five variables
1515  for ( k = 0; k < nWords/2; k++ )
1516  {
1517  pStore[0] += Kit_WordCountOnes( (pTruth[0] & 0x55555555) | ((pTruth[1] & 0x55555555) << 1) );
1518  pStore[1] += Kit_WordCountOnes( (pTruth[0] & 0x33333333) | ((pTruth[1] & 0x33333333) << 2) );
1519  pStore[2] += Kit_WordCountOnes( (pTruth[0] & 0x0F0F0F0F) | ((pTruth[1] & 0x0F0F0F0F) << 4) );
1520  pStore[3] += Kit_WordCountOnes( (pTruth[0] & 0x00FF00FF) | ((pTruth[1] & 0x00FF00FF) << 8) );
1521  pStore[4] += Kit_WordCountOnes( (pTruth[0] & 0x0000FFFF) | ((pTruth[1] & 0x0000FFFF) << 16) );
1522  pTruth += 2;
1523  }
1524 }
1525 
1526 /**Function*************************************************************
1527 
1528  Synopsis [Counts the number of 1's in each cofactor.]
1529 
1530  Description [Verifies the above procedure.]
1531 
1532  SideEffects []
1533 
1534  SeeAlso []
1535 
1536 ***********************************************************************/
1537 void Kit_TruthCountOnesInCofsSlow( unsigned * pTruth, int nVars, int * pStore, unsigned * pAux )
1538 {
1539  int i;
1540  for ( i = 0; i < nVars; i++ )
1541  {
1542  Kit_TruthCofactor0New( pAux, pTruth, nVars, i );
1543  pStore[2*i+0] = Kit_TruthCountOnes( pAux, nVars ) / 2;
1544  Kit_TruthCofactor1New( pAux, pTruth, nVars, i );
1545  pStore[2*i+1] = Kit_TruthCountOnes( pAux, nVars ) / 2;
1546  }
1547 }
1548 
1549 /**Function*************************************************************
1550 
1551  Synopsis [Canonicize the truth table.]
1552 
1553  Description []
1554 
1555  SideEffects []
1556 
1557  SeeAlso []
1558 
1559 ***********************************************************************/
1560 unsigned Kit_TruthHash( unsigned * pIn, int nWords )
1561 {
1562  // The 1,024 smallest prime numbers used to compute the hash value
1563  // http://www.math.utah.edu/~alfeld/math/primelist.html
1564  static int HashPrimes[1024] = { 2, 3, 5,
1565  7, 11, 13, 17, 19, 23, 29, 31, 37, 41, 43, 47, 53, 59, 61, 67, 71, 73, 79, 83, 89, 97,
1566  101, 103, 107, 109, 113, 127, 131, 137, 139, 149, 151, 157, 163, 167, 173, 179, 181, 191,
1567  193, 197, 199, 211, 223, 227, 229, 233, 239, 241, 251, 257, 263, 269, 271, 277, 281, 283,
1568  293, 307, 311, 313, 317, 331, 337, 347, 349, 353, 359, 367, 373, 379, 383, 389, 397, 401,
1569  409, 419, 421, 431, 433, 439, 443, 449, 457, 461, 463, 467, 479, 487, 491, 499, 503, 509,
1570  521, 523, 541, 547, 557, 563, 569, 571, 577, 587, 593, 599, 601, 607, 613, 617, 619, 631,
1571  641, 643, 647, 653, 659, 661, 673, 677, 683, 691, 701, 709, 719, 727, 733, 739, 743, 751,
1572  757, 761, 769, 773, 787, 797, 809, 811, 821, 823, 827, 829, 839, 853, 857, 859, 863, 877,
1573  881, 883, 887, 907, 911, 919, 929, 937, 941, 947, 953, 967, 971, 977, 983, 991, 997,
1574  1009, 1013, 1019, 1021, 1031, 1033, 1039, 1049, 1051, 1061, 1063, 1069, 1087, 1091,
1575  1093, 1097, 1103, 1109, 1117, 1123, 1129, 1151, 1153, 1163, 1171, 1181, 1187, 1193,
1576  1201, 1213, 1217, 1223, 1229, 1231, 1237, 1249, 1259, 1277, 1279, 1283, 1289, 1291,
1577  1297, 1301, 1303, 1307, 1319, 1321, 1327, 1361, 1367, 1373, 1381, 1399, 1409, 1423,
1578  1427, 1429, 1433, 1439, 1447, 1451, 1453, 1459, 1471, 1481, 1483, 1487, 1489, 1493,
1579  1499, 1511, 1523, 1531, 1543, 1549, 1553, 1559, 1567, 1571, 1579, 1583, 1597, 1601,
1580  1607, 1609, 1613, 1619, 1621, 1627, 1637, 1657, 1663, 1667, 1669, 1693, 1697, 1699,
1581  1709, 1721, 1723, 1733, 1741, 1747, 1753, 1759, 1777, 1783, 1787, 1789, 1801, 1811,
1582  1823, 1831, 1847, 1861, 1867, 1871, 1873, 1877, 1879, 1889, 1901, 1907, 1913, 1931,
1583  1933, 1949, 1951, 1973, 1979, 1987, 1993, 1997, 1999, 2003, 2011, 2017, 2027, 2029,
1584  2039, 2053, 2063, 2069, 2081, 2083, 2087, 2089, 2099, 2111, 2113, 2129, 2131, 2137,
1585  2141, 2143, 2153, 2161, 2179, 2203, 2207, 2213, 2221, 2237, 2239, 2243, 2251, 2267,
1586  2269, 2273, 2281, 2287, 2293, 2297, 2309, 2311, 2333, 2339, 2341, 2347, 2351, 2357,
1587  2371, 2377, 2381, 2383, 2389, 2393, 2399, 2411, 2417, 2423, 2437, 2441, 2447, 2459,
1588  2467, 2473, 2477, 2503, 2521, 2531, 2539, 2543, 2549, 2551, 2557, 2579, 2591, 2593,
1589  2609, 2617, 2621, 2633, 2647, 2657, 2659, 2663, 2671, 2677, 2683, 2687, 2689, 2693,
1590  2699, 2707, 2711, 2713, 2719, 2729, 2731, 2741, 2749, 2753, 2767, 2777, 2789, 2791,
1591  2797, 2801, 2803, 2819, 2833, 2837, 2843, 2851, 2857, 2861, 2879, 2887, 2897, 2903,
1592  2909, 2917, 2927, 2939, 2953, 2957, 2963, 2969, 2971, 2999, 3001, 3011, 3019, 3023,
1593  3037, 3041, 3049, 3061, 3067, 3079, 3083, 3089, 3109, 3119, 3121, 3137, 3163, 3167,
1594  3169, 3181, 3187, 3191, 3203, 3209, 3217, 3221, 3229, 3251, 3253, 3257, 3259, 3271,
1595  3299, 3301, 3307, 3313, 3319, 3323, 3329, 3331, 3343, 3347, 3359, 3361, 3371, 3373,
1596  3389, 3391, 3407, 3413, 3433, 3449, 3457, 3461, 3463, 3467, 3469, 3491, 3499, 3511,
1597  3517, 3527, 3529, 3533, 3539, 3541, 3547, 3557, 3559, 3571, 3581, 3583, 3593, 3607,
1598  3613, 3617, 3623, 3631, 3637, 3643, 3659, 3671, 3673, 3677, 3691, 3697, 3701, 3709,
1599  3719, 3727, 3733, 3739, 3761, 3767, 3769, 3779, 3793, 3797, 3803, 3821, 3823, 3833,
1600  3847, 3851, 3853, 3863, 3877, 3881, 3889, 3907, 3911, 3917, 3919, 3923, 3929, 3931,
1601  3943, 3947, 3967, 3989, 4001, 4003, 4007, 4013, 4019, 4021, 4027, 4049, 4051, 4057,
1602  4073, 4079, 4091, 4093, 4099, 4111, 4127, 4129, 4133, 4139, 4153, 4157, 4159, 4177,
1603  4201, 4211, 4217, 4219, 4229, 4231, 4241, 4243, 4253, 4259, 4261, 4271, 4273, 4283,
1604  4289, 4297, 4327, 4337, 4339, 4349, 4357, 4363, 4373, 4391, 4397, 4409, 4421, 4423,
1605  4441, 4447, 4451, 4457, 4463, 4481, 4483, 4493, 4507, 4513, 4517, 4519, 4523, 4547,
1606  4549, 4561, 4567, 4583, 4591, 4597, 4603, 4621, 4637, 4639, 4643, 4649, 4651, 4657,
1607  4663, 4673, 4679, 4691, 4703, 4721, 4723, 4729, 4733, 4751, 4759, 4783, 4787, 4789,
1608  4793, 4799, 4801, 4813, 4817, 4831, 4861, 4871, 4877, 4889, 4903, 4909, 4919, 4931,
1609  4933, 4937, 4943, 4951, 4957, 4967, 4969, 4973, 4987, 4993, 4999, 5003, 5009, 5011,
1610  5021, 5023, 5039, 5051, 5059, 5077, 5081, 5087, 5099, 5101, 5107, 5113, 5119, 5147,
1611  5153, 5167, 5171, 5179, 5189, 5197, 5209, 5227, 5231, 5233, 5237, 5261, 5273, 5279,
1612  5281, 5297, 5303, 5309, 5323, 5333, 5347, 5351, 5381, 5387, 5393, 5399, 5407, 5413,
1613  5417, 5419, 5431, 5437, 5441, 5443, 5449, 5471, 5477, 5479, 5483, 5501, 5503, 5507,
1614  5519, 5521, 5527, 5531, 5557, 5563, 5569, 5573, 5581, 5591, 5623, 5639, 5641, 5647,
1615  5651, 5653, 5657, 5659, 5669, 5683, 5689, 5693, 5701, 5711, 5717, 5737, 5741, 5743,
1616  5749, 5779, 5783, 5791, 5801, 5807, 5813, 5821, 5827, 5839, 5843, 5849, 5851, 5857,
1617  5861, 5867, 5869, 5879, 5881, 5897, 5903, 5923, 5927, 5939, 5953, 5981, 5987, 6007,
1618  6011, 6029, 6037, 6043, 6047, 6053, 6067, 6073, 6079, 6089, 6091, 6101, 6113, 6121,
1619  6131, 6133, 6143, 6151, 6163, 6173, 6197, 6199, 6203, 6211, 6217, 6221, 6229, 6247,
1620  6257, 6263, 6269, 6271, 6277, 6287, 6299, 6301, 6311, 6317, 6323, 6329, 6337, 6343,
1621  6353, 6359, 6361, 6367, 6373, 6379, 6389, 6397, 6421, 6427, 6449, 6451, 6469, 6473,
1622  6481, 6491, 6521, 6529, 6547, 6551, 6553, 6563, 6569, 6571, 6577, 6581, 6599, 6607,
1623  6619, 6637, 6653, 6659, 6661, 6673, 6679, 6689, 6691, 6701, 6703, 6709, 6719, 6733,
1624  6737, 6761, 6763, 6779, 6781, 6791, 6793, 6803, 6823, 6827, 6829, 6833, 6841, 6857,
1625  6863, 6869, 6871, 6883, 6899, 6907, 6911, 6917, 6947, 6949, 6959, 6961, 6967, 6971,
1626  6977, 6983, 6991, 6997, 7001, 7013, 7019, 7027, 7039, 7043, 7057, 7069, 7079, 7103,
1627  7109, 7121, 7127, 7129, 7151, 7159, 7177, 7187, 7193, 7207, 7211, 7213, 7219, 7229,
1628  7237, 7243, 7247, 7253, 7283, 7297, 7307, 7309, 7321, 7331, 7333, 7349, 7351, 7369,
1629  7393, 7411, 7417, 7433, 7451, 7457, 7459, 7477, 7481, 7487, 7489, 7499, 7507, 7517,
1630  7523, 7529, 7537, 7541, 7547, 7549, 7559, 7561, 7573, 7577, 7583, 7589, 7591, 7603,
1631  7607, 7621, 7639, 7643, 7649, 7669, 7673, 7681, 7687, 7691, 7699, 7703, 7717, 7723,
1632  7727, 7741, 7753, 7757, 7759, 7789, 7793, 7817, 7823, 7829, 7841, 7853, 7867, 7873,
1633  7877, 7879, 7883, 7901, 7907, 7919, 7927, 7933, 7937, 7949, 7951, 7963, 7993, 8009,
1634  8011, 8017, 8039, 8053, 8059, 8069, 8081, 8087, 8089, 8093, 8101, 8111, 8117, 8123,
1635  8147, 8161 };
1636  int i;
1637  unsigned uHashKey;
1638  assert( nWords <= 1024 );
1639  uHashKey = 0;
1640  for ( i = 0; i < nWords; i++ )
1641  uHashKey ^= HashPrimes[i] * pIn[i];
1642  return uHashKey;
1643 }
1644 
1645 
1646 /**Function*************************************************************
1647 
1648  Synopsis [Canonicize the truth table.]
1649 
1650  Description [Returns the phase. ]
1651 
1652  SideEffects []
1653 
1654  SeeAlso []
1655 
1656 ***********************************************************************/
1657 unsigned Kit_TruthSemiCanonicize( unsigned * pInOut, unsigned * pAux, int nVars, char * pCanonPerm )
1658 {
1659  int pStore[32];
1660  unsigned * pIn = pInOut, * pOut = pAux, * pTemp;
1661  int nWords = Kit_TruthWordNum( nVars );
1662  int i, Temp, fChange, Counter, nOnes;//, k, j, w, Limit;
1663  unsigned uCanonPhase;
1664 
1665  // canonicize output
1666  uCanonPhase = 0;
1667  for ( i = 0; i < nVars; i++ )
1668  pCanonPerm[i] = i;
1669 
1670  nOnes = Kit_TruthCountOnes(pIn, nVars);
1671  //if(pIn[0] & 1)
1672  if ( (nOnes > nWords * 16) )//|| ((nOnes == nWords * 16) && (pIn[0] & 1)) )
1673  {
1674  uCanonPhase |= (1 << nVars);
1675  Kit_TruthNot( pIn, pIn, nVars );
1676  }
1677 
1678  // collect the minterm counts
1679  Kit_TruthCountOnesInCofs( pIn, nVars, pStore );
1680 /*
1681  Kit_TruthCountOnesInCofsSlow( pIn, nVars, pStore2, pAux );
1682  for ( i = 0; i < 2*nVars; i++ )
1683  {
1684  assert( pStore[i] == pStore2[i] );
1685  }
1686 */
1687  // canonicize phase
1688  for ( i = 0; i < nVars; i++ )
1689  {
1690  if ( pStore[2*i+0] >= pStore[2*i+1] )
1691  continue;
1692  uCanonPhase |= (1 << i);
1693  Temp = pStore[2*i+0];
1694  pStore[2*i+0] = pStore[2*i+1];
1695  pStore[2*i+1] = Temp;
1696  Kit_TruthChangePhase( pIn, nVars, i );
1697  }
1698 
1699 // Kit_PrintHexadecimal( stdout, pIn, nVars );
1700 // printf( "\n" );
1701 
1702  // permute
1703  Counter = 0;
1704  do {
1705  fChange = 0;
1706  for ( i = 0; i < nVars-1; i++ )
1707  {
1708  if ( pStore[2*i] >= pStore[2*(i+1)] )
1709  continue;
1710  Counter++;
1711  fChange = 1;
1712 
1713  Temp = pCanonPerm[i];
1714  pCanonPerm[i] = pCanonPerm[i+1];
1715  pCanonPerm[i+1] = Temp;
1716 
1717  Temp = pStore[2*i];
1718  pStore[2*i] = pStore[2*(i+1)];
1719  pStore[2*(i+1)] = Temp;
1720 
1721  Temp = pStore[2*i+1];
1722  pStore[2*i+1] = pStore[2*(i+1)+1];
1723  pStore[2*(i+1)+1] = Temp;
1724 
1725  // if the polarity of variables is different, swap them
1726  if ( ((uCanonPhase & (1 << i)) > 0) != ((uCanonPhase & (1 << (i+1))) > 0) )
1727  {
1728  uCanonPhase ^= (1 << i);
1729  uCanonPhase ^= (1 << (i+1));
1730  }
1731 
1732  Kit_TruthSwapAdjacentVars( pOut, pIn, nVars, i );
1733  pTemp = pIn; pIn = pOut; pOut = pTemp;
1734  }
1735  } while ( fChange );
1736 
1737 
1738 /*
1739  Extra_PrintBinary( stdout, &uCanonPhase, nVars+1 ); printf( " : " );
1740  for ( i = 0; i < nVars; i++ )
1741  printf( "%d=%d/%d ", pCanonPerm[i], pStore[2*i], pStore[2*i+1] );
1742  printf( " C = %d\n", Counter );
1743  Extra_PrintHexadecimal( stdout, pIn, nVars );
1744  printf( "\n" );
1745 */
1746 
1747 /*
1748  // process symmetric variable groups
1749  uSymms = 0;
1750  for ( i = 0; i < nVars-1; i++ )
1751  {
1752  if ( pStore[2*i] != pStore[2*(i+1)] ) // i and i+1 cannot be symmetric
1753  continue;
1754  if ( pStore[2*i] != pStore[2*i+1] )
1755  continue;
1756  if ( Kit_TruthVarsSymm( pIn, nVars, i, i+1 ) )
1757  continue;
1758  if ( Kit_TruthVarsAntiSymm( pIn, nVars, i, i+1 ) )
1759  Kit_TruthChangePhase( pIn, nVars, i+1 );
1760  }
1761 */
1762 
1763 /*
1764  // process symmetric variable groups
1765  uSymms = 0;
1766  for ( i = 0; i < nVars-1; i++ )
1767  {
1768  if ( pStore[2*i] != pStore[2*(i+1)] ) // i and i+1 cannot be symmetric
1769  continue;
1770  // i and i+1 can be symmetric
1771  // find the end of this group
1772  for ( k = i+1; k < nVars; k++ )
1773  if ( pStore[2*i] != pStore[2*k] )
1774  break;
1775  Limit = k;
1776  assert( i < Limit-1 );
1777  // go through the variables in this group
1778  for ( j = i + 1; j < Limit; j++ )
1779  {
1780  // check symmetry
1781  if ( Kit_TruthVarsSymm( pIn, nVars, i, j ) )
1782  {
1783  uSymms |= (1 << j);
1784  continue;
1785  }
1786  // they are phase-unknown
1787  if ( pStore[2*i] == pStore[2*i+1] )
1788  {
1789  if ( Kit_TruthVarsAntiSymm( pIn, nVars, i, j ) )
1790  {
1791  Kit_TruthChangePhase( pIn, nVars, j );
1792  uCanonPhase ^= (1 << j);
1793  uSymms |= (1 << j);
1794  continue;
1795  }
1796  }
1797 
1798  // they are not symmetric - move j as far as it goes in the group
1799  for ( k = j; k < Limit-1; k++ )
1800  {
1801  Counter++;
1802 
1803  Temp = pCanonPerm[k];
1804  pCanonPerm[k] = pCanonPerm[k+1];
1805  pCanonPerm[k+1] = Temp;
1806 
1807  assert( pStore[2*k] == pStore[2*(k+1)] );
1808  Kit_TruthSwapAdjacentVars( pOut, pIn, nVars, k );
1809  pTemp = pIn; pIn = pOut; pOut = pTemp;
1810  }
1811  Limit--;
1812  j--;
1813  }
1814  i = Limit - 1;
1815  }
1816 */
1817 
1818  // swap if it was moved an even number of times
1819  if ( Counter & 1 )
1820  Kit_TruthCopy( pOut, pIn, nVars );
1821  return uCanonPhase;
1822 }
1823 
1824 
1825 /**Function*************************************************************
1826 
1827  Synopsis [Fast counting minterms in the cofactors of a function.]
1828 
1829  Description [Returns the total number of minterms in the function.
1830  The resulting array (pRes) contains the number of minterms in 0-cofactor
1831  w.r.t. each variables. The additional array (pBytes) is used for internal
1832  storage. It should have the size equal to the number of truth table bytes.]
1833 
1834  SideEffects []
1835 
1836  SeeAlso []
1837 
1838 ***********************************************************************/
1839 int Kit_TruthCountMinterms( unsigned * pTruth, int nVars, int * pRes, int * pBytesInit )
1840 {
1841  // the number of 1s if every byte as well as in the 0-cofactors w.r.t. three variables
1842  static unsigned Table[256] = {
1843  0x00000000, 0x01010101, 0x01010001, 0x02020102, 0x01000101, 0x02010202, 0x02010102, 0x03020203,
1844  0x01000001, 0x02010102, 0x02010002, 0x03020103, 0x02000102, 0x03010203, 0x03010103, 0x04020204,
1845  0x00010101, 0x01020202, 0x01020102, 0x02030203, 0x01010202, 0x02020303, 0x02020203, 0x03030304,
1846  0x01010102, 0x02020203, 0x02020103, 0x03030204, 0x02010203, 0x03020304, 0x03020204, 0x04030305,
1847  0x00010001, 0x01020102, 0x01020002, 0x02030103, 0x01010102, 0x02020203, 0x02020103, 0x03030204,
1848  0x01010002, 0x02020103, 0x02020003, 0x03030104, 0x02010103, 0x03020204, 0x03020104, 0x04030205,
1849  0x00020102, 0x01030203, 0x01030103, 0x02040204, 0x01020203, 0x02030304, 0x02030204, 0x03040305,
1850  0x01020103, 0x02030204, 0x02030104, 0x03040205, 0x02020204, 0x03030305, 0x03030205, 0x04040306,
1851  0x00000101, 0x01010202, 0x01010102, 0x02020203, 0x01000202, 0x02010303, 0x02010203, 0x03020304,
1852  0x01000102, 0x02010203, 0x02010103, 0x03020204, 0x02000203, 0x03010304, 0x03010204, 0x04020305,
1853  0x00010202, 0x01020303, 0x01020203, 0x02030304, 0x01010303, 0x02020404, 0x02020304, 0x03030405,
1854  0x01010203, 0x02020304, 0x02020204, 0x03030305, 0x02010304, 0x03020405, 0x03020305, 0x04030406,
1855  0x00010102, 0x01020203, 0x01020103, 0x02030204, 0x01010203, 0x02020304, 0x02020204, 0x03030305,
1856  0x01010103, 0x02020204, 0x02020104, 0x03030205, 0x02010204, 0x03020305, 0x03020205, 0x04030306,
1857  0x00020203, 0x01030304, 0x01030204, 0x02040305, 0x01020304, 0x02030405, 0x02030305, 0x03040406,
1858  0x01020204, 0x02030305, 0x02030205, 0x03040306, 0x02020305, 0x03030406, 0x03030306, 0x04040407,
1859  0x00000001, 0x01010102, 0x01010002, 0x02020103, 0x01000102, 0x02010203, 0x02010103, 0x03020204,
1860  0x01000002, 0x02010103, 0x02010003, 0x03020104, 0x02000103, 0x03010204, 0x03010104, 0x04020205,
1861  0x00010102, 0x01020203, 0x01020103, 0x02030204, 0x01010203, 0x02020304, 0x02020204, 0x03030305,
1862  0x01010103, 0x02020204, 0x02020104, 0x03030205, 0x02010204, 0x03020305, 0x03020205, 0x04030306,
1863  0x00010002, 0x01020103, 0x01020003, 0x02030104, 0x01010103, 0x02020204, 0x02020104, 0x03030205,
1864  0x01010003, 0x02020104, 0x02020004, 0x03030105, 0x02010104, 0x03020205, 0x03020105, 0x04030206,
1865  0x00020103, 0x01030204, 0x01030104, 0x02040205, 0x01020204, 0x02030305, 0x02030205, 0x03040306,
1866  0x01020104, 0x02030205, 0x02030105, 0x03040206, 0x02020205, 0x03030306, 0x03030206, 0x04040307,
1867  0x00000102, 0x01010203, 0x01010103, 0x02020204, 0x01000203, 0x02010304, 0x02010204, 0x03020305,
1868  0x01000103, 0x02010204, 0x02010104, 0x03020205, 0x02000204, 0x03010305, 0x03010205, 0x04020306,
1869  0x00010203, 0x01020304, 0x01020204, 0x02030305, 0x01010304, 0x02020405, 0x02020305, 0x03030406,
1870  0x01010204, 0x02020305, 0x02020205, 0x03030306, 0x02010305, 0x03020406, 0x03020306, 0x04030407,
1871  0x00010103, 0x01020204, 0x01020104, 0x02030205, 0x01010204, 0x02020305, 0x02020205, 0x03030306,
1872  0x01010104, 0x02020205, 0x02020105, 0x03030206, 0x02010205, 0x03020306, 0x03020206, 0x04030307,
1873  0x00020204, 0x01030305, 0x01030205, 0x02040306, 0x01020305, 0x02030406, 0x02030306, 0x03040407,
1874  0x01020205, 0x02030306, 0x02030206, 0x03040307, 0x02020306, 0x03030407, 0x03030307, 0x04040408
1875  };
1876  unsigned uSum;
1877  unsigned char * pTruthC, * pLimit;
1878  int * pBytes = pBytesInit;
1879  int i, iVar, Step, nWords, nBytes, nTotal;
1880 
1881  assert( nVars <= 20 );
1882 
1883  // clear storage
1884  memset( pRes, 0, sizeof(int) * nVars );
1885 
1886  // count the number of one's in 0-cofactors of the first three variables
1887  nTotal = uSum = 0;
1888  nWords = Kit_TruthWordNum( nVars );
1889  nBytes = nWords * 4;
1890  pTruthC = (unsigned char *)pTruth;
1891  pLimit = pTruthC + nBytes;
1892  for ( ; pTruthC < pLimit; pTruthC++ )
1893  {
1894  uSum += Table[*pTruthC];
1895  *pBytes++ = (Table[*pTruthC] & 0xff);
1896  if ( (uSum & 0xff) > 246 )
1897  {
1898  nTotal += (uSum & 0xff);
1899  pRes[0] += ((uSum >> 8) & 0xff);
1900  pRes[2] += ((uSum >> 16) & 0xff);
1901  pRes[3] += ((uSum >> 24) & 0xff);
1902  uSum = 0;
1903  }
1904  }
1905  if ( uSum )
1906  {
1907  nTotal += (uSum & 0xff);
1908  pRes[0] += ((uSum >> 8) & 0xff);
1909  pRes[1] += ((uSum >> 16) & 0xff);
1910  pRes[2] += ((uSum >> 24) & 0xff);
1911  }
1912 
1913  // count all other variables
1914  for ( iVar = 3, Step = 1; Step < nBytes; Step *= 2, iVar++ )
1915  for ( i = 0; i < nBytes; i += Step + Step )
1916  {
1917  pRes[iVar] += pBytesInit[i];
1918  pBytesInit[i] += pBytesInit[i+Step];
1919  }
1920  assert( pBytesInit[0] == nTotal );
1921  assert( iVar == nVars );
1922 
1923  for ( i = 0; i < nVars; i++ )
1924  assert( pRes[i] == Kit_TruthCofactor0Count(pTruth, nVars, i) );
1925  return nTotal;
1926 }
1927 
1928 /**Function*************************************************************
1929 
1930  Synopsis [Prints the hex unsigned into a file.]
1931 
1932  Description []
1933 
1934  SideEffects []
1935 
1936  SeeAlso []
1937 
1938 ***********************************************************************/
1939 void Kit_PrintHexadecimal( FILE * pFile, unsigned Sign[], int nVars )
1940 {
1941  int nDigits, Digit, k;
1942  // write the number into the file
1943  nDigits = (1 << nVars) / 4;
1944  for ( k = nDigits - 1; k >= 0; k-- )
1945  {
1946  Digit = ((Sign[k/8] >> ((k%8) * 4)) & 15);
1947  if ( Digit < 10 )
1948  fprintf( pFile, "%d", Digit );
1949  else
1950  fprintf( pFile, "%c", 'a' + Digit-10 );
1951  }
1952 // fprintf( pFile, "\n" );
1953 }
1954 
1955 /**Function*************************************************************
1956 
1957  Synopsis [Fast counting minterms for the functions.]
1958 
1959  Description [Returns 0 if the function is a constant.]
1960 
1961  SideEffects []
1962 
1963  SeeAlso []
1964 
1965 ***********************************************************************/
1966 void Kit_TruthCountMintermsPrecomp()
1967 {
1968  int bit_count[256] = {
1969  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,
1970  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,
1971  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,
1972  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,
1973  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,
1974  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,
1975  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,
1976  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
1977  };
1978  unsigned i, uWord;
1979  for ( i = 0; i < 256; i++ )
1980  {
1981  if ( i % 8 == 0 )
1982  printf( "\n" );
1983  uWord = bit_count[i];
1984  uWord |= (bit_count[i & 0x55] << 8);
1985  uWord |= (bit_count[i & 0x33] << 16);
1986  uWord |= (bit_count[i & 0x0f] << 24);
1987  printf( "0x" );
1988  Kit_PrintHexadecimal( stdout, &uWord, 5 );
1989  printf( ", " );
1990  }
1991 }
1992 
1993 /**Function*************************************************************
1994 
1995  Synopsis [Dumps truth table into a file.]
1996 
1997  Description [Generates script file for reading into ABC.]
1998 
1999  SideEffects []
2000 
2001  SeeAlso []
2002 
2003 ***********************************************************************/
2004 char * Kit_TruthDumpToFile( unsigned * pTruth, int nVars, int nFile )
2005 {
2006  static char pFileName[100];
2007  FILE * pFile;
2008  sprintf( pFileName, "tt\\s%04d", nFile );
2009  pFile = fopen( pFileName, "w" );
2010  fprintf( pFile, "rt " );
2011  Kit_PrintHexadecimal( pFile, pTruth, nVars );
2012  fprintf( pFile, "; bdd; sop; ps\n" );
2013  fclose( pFile );
2014  return pFileName;
2015 }
2016 
2017 
2018 /**Function*************************************************************
2019 
2020  Synopsis [Dumps truth table into a file.]
2021 
2022  Description [Generates script file for reading into ABC.]
2023 
2024  SideEffects []
2025 
2026  SeeAlso []
2027 
2028 ***********************************************************************/
2029 void Kit_TruthPrintProfile_int( unsigned * pTruth, int nVars )
2030 {
2031  int Mints[20];
2032  int Mints0[20];
2033  int Mints1[20];
2034  int Unique1[20];
2035  int Total2[20][20];
2036  int Unique2[20][20];
2037  int Common2[20][20];
2038  int nWords = Kit_TruthWordNum( nVars );
2039  int * pBytes = ABC_ALLOC( int, nWords * 4 );
2040  unsigned * pIn = ABC_ALLOC( unsigned, nWords );
2041  unsigned * pOut = ABC_ALLOC( unsigned, nWords );
2042  unsigned * pCof00 = ABC_ALLOC( unsigned, nWords );
2043  unsigned * pCof01 = ABC_ALLOC( unsigned, nWords );
2044  unsigned * pCof10 = ABC_ALLOC( unsigned, nWords );
2045  unsigned * pCof11 = ABC_ALLOC( unsigned, nWords );
2046  unsigned * pTemp;
2047  int nTotalMints, nTotalMints0, nTotalMints1;
2048  int v, u, i, iVar, nMints1;
2049  int Cof00, Cof01, Cof10, Cof11;
2050  int Coz00, Coz01, Coz10, Coz11;
2051  assert( nVars <= 20 );
2052  assert( nVars >= 6 );
2053 
2054  nTotalMints = Kit_TruthCountMinterms( pTruth, nVars, Mints, pBytes );
2055  for ( v = 0; v < nVars; v++ )
2056  Unique1[v] = Kit_TruthBooleanDiffCount( pTruth, nVars, v );
2057 
2058  for ( v = 0; v < nVars; v++ )
2059  for ( u = 0; u < nVars; u++ )
2060  Total2[v][u] = Unique2[v][u] = Common2[v][u] = -1;
2061 
2062  nMints1 = (1<<(nVars-2));
2063  for ( v = 0; v < nVars; v++ )
2064  {
2065  // move this var to be the first
2066  Kit_TruthCopy( pIn, pTruth, nVars );
2067 // Extra_PrintBinary( stdout, pIn, (1<<nVars) ); printf( "\n" );
2068  for ( i = v; i < nVars - 1; i++ )
2069  {
2070  Kit_TruthSwapAdjacentVars( pOut, pIn, nVars, i );
2071  pTemp = pIn; pIn = pOut; pOut = pTemp;
2072  }
2073 // Extra_PrintBinary( stdout, pIn, (1<<nVars) ); printf( "\n" );
2074 // printf( "\n" );
2075 
2076 
2077  // count minterms in both cofactor
2078  nTotalMints0 = Kit_TruthCountMinterms( pIn, nVars-1, Mints0, pBytes );
2079  nTotalMints1 = Kit_TruthCountMinterms( pIn+nWords/2, nVars-1, Mints1, pBytes );
2080  assert( nTotalMints == nTotalMints0 + nTotalMints1 );
2081 /*
2082  for ( u = 0; u < nVars-1; u++ )
2083  printf( "%2d ", Mints0[u] );
2084  printf( "\n" );
2085 
2086  for ( u = 0; u < nVars-1; u++ )
2087  printf( "%2d ", Mints1[u] );
2088  printf( "\n" );
2089 */
2090  for ( u = 0; u < nVars-1; u++ )
2091  {
2092  if ( u < v )
2093  iVar = u;
2094  else
2095  iVar = u + 1;
2096  assert( v != iVar );
2097  // get minter counts in the cofactors
2098  Cof00 = Mints0[u]; Coz00 = nMints1 - Cof00;
2099  Cof01 = nTotalMints0-Mints0[u]; Coz01 = nMints1 - Cof01;
2100  Cof10 = Mints1[u]; Coz10 = nMints1 - Cof10;
2101  Cof11 = nTotalMints1-Mints1[u]; Coz11 = nMints1 - Cof11;
2102 
2103  assert( Cof00 >= 0 && Cof00 <= nMints1 );
2104  assert( Cof01 >= 0 && Cof01 <= nMints1 );
2105  assert( Cof10 >= 0 && Cof10 <= nMints1 );
2106  assert( Cof11 >= 0 && Cof11 <= nMints1 );
2107 
2108  assert( Coz00 >= 0 && Coz00 <= nMints1 );
2109  assert( Coz01 >= 0 && Coz01 <= nMints1 );
2110  assert( Coz10 >= 0 && Coz10 <= nMints1 );
2111  assert( Coz11 >= 0 && Coz11 <= nMints1 );
2112 
2113  Common2[v][iVar] = Common2[iVar][v] = Cof00 * Coz11 + Coz00 * Cof11 + Cof01 * Coz10 + Coz01 * Cof10;
2114 
2115  Total2[v][iVar] = Total2[iVar][v] =
2116  Cof00 * Coz01 + Coz00 * Cof01 +
2117  Cof00 * Coz10 + Coz00 * Cof10 +
2118  Cof00 * Coz11 + Coz00 * Cof11 +
2119  Cof01 * Coz10 + Coz01 * Cof10 +
2120  Cof01 * Coz11 + Coz01 * Cof11 +
2121  Cof10 * Coz11 + Coz10 * Cof11 ;
2122 
2123 
2124  Kit_TruthCofactor0New( pCof00, pIn, nVars-1, u );
2125  Kit_TruthCofactor1New( pCof01, pIn, nVars-1, u );
2126  Kit_TruthCofactor0New( pCof10, pIn+nWords/2, nVars-1, u );
2127  Kit_TruthCofactor1New( pCof11, pIn+nWords/2, nVars-1, u );
2128 
2129  Unique2[v][iVar] = Unique2[iVar][v] =
2130  Kit_TruthXorCount( pCof00, pCof01, nVars-1 ) +
2131  Kit_TruthXorCount( pCof00, pCof10, nVars-1 ) +
2132  Kit_TruthXorCount( pCof00, pCof11, nVars-1 ) +
2133  Kit_TruthXorCount( pCof01, pCof10, nVars-1 ) +
2134  Kit_TruthXorCount( pCof01, pCof11, nVars-1 ) +
2135  Kit_TruthXorCount( pCof10, pCof11, nVars-1 );
2136  }
2137  }
2138 
2139  printf( "\n" );
2140  printf( " V: " );
2141  for ( v = 0; v < nVars; v++ )
2142  printf( "%8c ", v+'a' );
2143  printf( "\n" );
2144 
2145  printf( " M: " );
2146  for ( v = 0; v < nVars; v++ )
2147  printf( "%8d ", Mints[v] );
2148  printf( "\n" );
2149 
2150  printf( " U: " );
2151  for ( v = 0; v < nVars; v++ )
2152  printf( "%8d ", Unique1[v] );
2153  printf( "\n" );
2154  printf( "\n" );
2155 
2156  printf( "Unique:\n" );
2157  for ( i = 0; i < nVars; i++ )
2158  {
2159  printf( " %2d ", i );
2160  for ( v = 0; v < nVars; v++ )
2161  printf( "%8d ", Unique2[i][v] );
2162  printf( "\n" );
2163  }
2164 
2165  printf( "Common:\n" );
2166  for ( i = 0; i < nVars; i++ )
2167  {
2168  printf( " %2d ", i );
2169  for ( v = 0; v < nVars; v++ )
2170  printf( "%8d ", Common2[i][v] );
2171  printf( "\n" );
2172  }
2173 
2174  printf( "Total:\n" );
2175  for ( i = 0; i < nVars; i++ )
2176  {
2177  printf( " %2d ", i );
2178  for ( v = 0; v < nVars; v++ )
2179  printf( "%8d ", Total2[i][v] );
2180  printf( "\n" );
2181  }
2182 
2183  ABC_FREE( pIn );
2184  ABC_FREE( pOut );
2185  ABC_FREE( pCof00 );
2186  ABC_FREE( pCof01 );
2187  ABC_FREE( pCof10 );
2188  ABC_FREE( pCof11 );
2189  ABC_FREE( pBytes );
2190 }
2191 
2192 /**Function*************************************************************
2193 
2194  Synopsis [Dumps truth table into a file.]
2195 
2196  Description [Generates script file for reading into ABC.]
2197 
2198  SideEffects []
2199 
2200  SeeAlso []
2201 
2202 ***********************************************************************/
2203 void Kit_TruthPrintProfile( unsigned * pTruth, int nVars )
2204 {
2205  unsigned uTruth[2];
2206  if ( nVars >= 6 )
2207  {
2208  Kit_TruthPrintProfile_int( pTruth, nVars );
2209  return;
2210  }
2211  assert( nVars >= 2 );
2212  uTruth[0] = pTruth[0];
2213  uTruth[1] = pTruth[0];
2214  Kit_TruthPrintProfile( uTruth, 6 );
2215 }
2216 
2217 
2218 ////////////////////////////////////////////////////////////////////////
2219 /// END OF FILE ///
2220 ////////////////////////////////////////////////////////////////////////
2221 
2222 
2223 ABC_NAMESPACE_IMPL_END
2224 
memset
char * memset()
Kit_TruthDumpToFile
char * Kit_TruthDumpToFile(unsigned *pTruth, int nVars, int nFile)
Definition: kitTruth.c:2004
Kit_TruthVarsAntiSymm
int Kit_TruthVarsAntiSymm(unsigned *pTruth, int nVars, int iVar0, int iVar1, unsigned *pCof0, unsigned *pCof1)
Definition: kitTruth.c:1223
KIT_INFINITY
#define KIT_INFINITY
Definition: kit.h:173
Kit_PrintHexadecimal
void Kit_PrintHexadecimal(FILE *pFile, unsigned Sign[], int nVars)
Definition: kitTruth.c:1939
Kit_TruthWordNum
static int Kit_TruthWordNum(int nVars)
Definition: kit.h:224
Kit_TruthExistSet
void Kit_TruthExistSet(unsigned *pRes, unsigned *pTruth, int nVars, unsigned uMask)
Definition: kitTruth.c:793
Kit_TruthSemiCanonicize
unsigned Kit_TruthSemiCanonicize(unsigned *pInOut, unsigned *pAux, int nVars, char *pCanonPerm)
Definition: kitTruth.c:1657
Kit_TruthBooleanDiffCount
int Kit_TruthBooleanDiffCount(unsigned *pTruth, int nVars, int iVar)
Definition: kitTruth.c:977
Kit_TruthVarInSupport
int Kit_TruthVarInSupport(unsigned *pTruth, int nVars, int iVar)
Definition: kitTruth.c:270
ABC_ALLOC
#define ABC_ALLOC(type, num)
Definition: abc_global.h:229
Kit_TruthSwapAdjacentVars
ABC_NAMESPACE_IMPL_START void Kit_TruthSwapAdjacentVars(unsigned *pOut, unsigned *pIn, int nVars, int iVar)
DECLARATIONS ///.
Definition: kitTruth.c:46
Kit_TruthCofactor1
void Kit_TruthCofactor1(unsigned *pTruth, int nVars, int iVar)
Definition: kitTruth.c:470
Kit_TruthIsEqual
static int Kit_TruthIsEqual(unsigned *pIn0, unsigned *pIn1, int nVars)
Definition: kit.h:274
Kit_TruthIsConst0
static int Kit_TruthIsConst0(unsigned *pIn, int nVars)
Definition: kit.h:315
Kit_TruthStretch
void Kit_TruthStretch(unsigned *pOut, unsigned *pIn, int nVars, int nVarsAll, unsigned Phase, int fReturnIn)
Definition: kitTruth.c:166
Kit_TruthCofactor1New
void Kit_TruthCofactor1New(unsigned *pOut, unsigned *pIn, int nVars, int iVar)
Definition: kitTruth.c:573
bit_count
static int bit_count[256]
Definition: fpgaCut.c:50
nWords
int nWords
Definition: abcNpn.c:127
Kit_TruthSwapAdjacentVars2
void Kit_TruthSwapAdjacentVars2(unsigned *pIn, unsigned *pOut, int nVars, int Start)
Definition: kitTruth.c:103
Kit_TruthCountMintermsPrecomp
void Kit_TruthCountMintermsPrecomp()
Definition: kitTruth.c:1966
Kit_TruthSupportSize
int Kit_TruthSupportSize(unsigned *pTruth, int nVars)
Definition: kitTruth.c:327
Kit_TruthPrintProfile_int
void Kit_TruthPrintProfile_int(unsigned *pTruth, int nVars)
Definition: kitTruth.c:2029
Kit_TruthCountOnesInCofsSlow
void Kit_TruthCountOnesInCofsSlow(unsigned *pTruth, int nVars, int *pStore, unsigned *pAux)
Definition: kitTruth.c:1537
Kit_TruthExistNew
void Kit_TruthExistNew(unsigned *pRes, unsigned *pTruth, int nVars, int iVar)
Definition: kitTruth.c:738
Kit_TruthMuxVar
void Kit_TruthMuxVar(unsigned *pOut, unsigned *pCof0, unsigned *pCof1, int nVars, int iVar)
Definition: kitTruth.c:1069
Kit_TruthIsConst1
static int Kit_TruthIsConst1(unsigned *pIn, int nVars)
Definition: kit.h:323
Kit_TruthPermute
void Kit_TruthPermute(unsigned *pOut, unsigned *pIn, int nVars, char *pPerm, int fReturnIn)
Definition: kitTruth.c:233
Kit_TruthXorCount
int Kit_TruthXorCount(unsigned *pTruth0, unsigned *pTruth1, int nVars)
Definition: kitTruth.c:1028
Kit_TruthMuxVarPhase
void Kit_TruthMuxVarPhase(unsigned *pOut, unsigned *pCof0, unsigned *pCof1, int nVars, int iVar, int fCompl0)
Definition: kitTruth.c:1125
Kit_TruthBestCofVar
int Kit_TruthBestCofVar(unsigned *pTruth, int nVars, unsigned *pCof0, unsigned *pCof1)
Definition: kitTruth.c:1365
Kit_TruthUniqueNew
void Kit_TruthUniqueNew(unsigned *pRes, unsigned *pTruth, int nVars, int iVar)
Definition: kitTruth.c:922
Kit_TruthExist
void Kit_TruthExist(unsigned *pTruth, int nVars, int iVar)
Definition: kitTruth.c:684
ABC_NAMESPACE_IMPL_END
#define ABC_NAMESPACE_IMPL_END
Definition: abc_global.h:108
Kit_TruthCountOnes
static int Kit_TruthCountOnes(unsigned *pIn, int nVars)
Definition: kit.h:251
sprintf
char * sprintf()
Counter
static int Counter
Definition: extraBddMisc.c:1877
Kit_TruthVarIsVacuous
int Kit_TruthVarIsVacuous(unsigned *pOnset, unsigned *pOffset, int nVars, int iVar)
Definition: kitTruth.c:625
Kit_TruthMinCofSuppOverlap
int Kit_TruthMinCofSuppOverlap(unsigned *pTruth, int nVars, int *pVarMin)
Definition: kitTruth.c:1315
Kit_TruthNot
static void Kit_TruthNot(unsigned *pOut, unsigned *pIn, int nVars)
Definition: kit.h:373
Kit_TruthForallSet
void Kit_TruthForallSet(unsigned *pRes, unsigned *pTruth, int nVars, unsigned uMask)
Definition: kitTruth.c:1048
Kit_TruthShrink
void Kit_TruthShrink(unsigned *pOut, unsigned *pIn, int nVars, int nVarsAll, unsigned Phase, int fReturnIn)
Definition: kitTruth.c:200
pPerm
static int pPerm[13719]
Definition: rwrTemp.c:32
PMasks
static word PMasks[5][3]
Definition: ifDec07.c:44
Kit_TruthCofactor0New
void Kit_TruthCofactor0New(unsigned *pOut, unsigned *pIn, int nVars, int iVar)
Definition: kitTruth.c:521
Kit_TruthForall
void Kit_TruthForall(unsigned *pTruth, int nVars, int iVar)
Definition: kitTruth.c:813
Kit_TruthChangePhase
void Kit_TruthChangePhase(unsigned *pTruth, int nVars, int iVar)
Definition: kitTruth.c:1259
Kit_TruthCofactor0
void Kit_TruthCofactor0(unsigned *pTruth, int nVars, int iVar)
Definition: kitTruth.c:368
ABC_NAMESPACE_IMPL_START
#define ABC_NAMESPACE_IMPL_START
Definition: abc_global.h:107
Kit_TruthPrintProfile
void Kit_TruthPrintProfile(unsigned *pTruth, int nVars)
Definition: kitTruth.c:2203
Kit_TruthVarsSymm
int Kit_TruthVarsSymm(unsigned *pTruth, int nVars, int iVar0, int iVar1, unsigned *pCof0, unsigned *pCof1)
Definition: kitTruth.c:1187
ABC_FREE
#define ABC_FREE(obj)
Definition: abc_global.h:232
Kit_TruthCopy
static void Kit_TruthCopy(unsigned *pOut, unsigned *pIn, int nVars)
Definition: kit.h:355
Minisat::Var
int Var
Definition: SolverTypes.h:42
assert
#define assert(ex)
Definition: util_old.h:213
Kit_WordCountOnes
static int Kit_WordCountOnes(unsigned uWord)
Definition: kit.h:243
Kit_TruthCountOnesInCofs0
void Kit_TruthCountOnesInCofs0(unsigned *pTruth, int nVars, int *pStore)
Definition: kitTruth.c:1486
Kit_TruthHash
unsigned Kit_TruthHash(unsigned *pIn, int nWords)
Definition: kitTruth.c:1560
Kit_TruthSupport
unsigned Kit_TruthSupport(unsigned *pTruth, int nVars)
Definition: kitTruth.c:346
Kit_TruthCountOnesInCofs
void Kit_TruthCountOnesInCofs(unsigned *pTruth, int nVars, int *pStore)
Definition: kitTruth.c:1410
Kit_TruthForallNew
void Kit_TruthForallNew(unsigned *pRes, unsigned *pTruth, int nVars, int iVar)
Definition: kitTruth.c:867
Kit_TruthCountMinterms
int Kit_TruthCountMinterms(unsigned *pTruth, int nVars, int *pRes, int *pBytesInit)
Definition: kitTruth.c:1839
nTotal
int nTotal
DECLARATIONS ///.
Definition: cutTruth.c:37
Kit_TruthCofactor0Count
int Kit_TruthCofactor0Count(unsigned *pTruth, int nVars, int iVar)
Definition: kitTruth.c:419