abc-master
 All Data Structures Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros
extraUtilTruth.c
Go to the documentation of this file.
1 /**CFile****************************************************************
2 
3  FileName [extraUtilMisc.c]
4 
5  SystemName [ABC: Logic synthesis and verification system.]
6 
7  PackageName [extra]
8 
9  Synopsis [Various procedures for truth table manipulation.]
10 
11  Author [Alan Mishchenko]
12 
13  Affiliation [UC Berkeley]
14 
15  Date [Ver. 1.0. Started - June 20, 2005.]
16 
17  Revision [$Id: extraUtilMisc.c,v 1.0 2003/09/01 00:00:00 alanmi Exp $]
18 
19 ***********************************************************************/
20 
21 #include "extra.h"
22 
23 ABC_NAMESPACE_IMPL_START
24 
25 
26 /*---------------------------------------------------------------------------*/
27 /* Constant declarations */
28 /*---------------------------------------------------------------------------*/
29 
30 /*---------------------------------------------------------------------------*/
31 /* Stucture declarations */
32 /*---------------------------------------------------------------------------*/
33 
34 /*---------------------------------------------------------------------------*/
35 /* Type declarations */
36 /*---------------------------------------------------------------------------*/
37 
38 /*---------------------------------------------------------------------------*/
39 /* Variable declarations */
40 /*---------------------------------------------------------------------------*/
41 
42 static unsigned s_VarMasks[5][2] = {
43  { 0x33333333, 0xAAAAAAAA },
44  { 0x55555555, 0xCCCCCCCC },
45  { 0x0F0F0F0F, 0xF0F0F0F0 },
46  { 0x00FF00FF, 0xFF00FF00 },
47  { 0x0000FFFF, 0xFFFF0000 }
48 };
49 
50 /*---------------------------------------------------------------------------*/
51 /* Macro declarations */
52 /*---------------------------------------------------------------------------*/
53 
54 /**AutomaticStart*************************************************************/
55 
56 /*---------------------------------------------------------------------------*/
57 /* Static function prototypes */
58 /*---------------------------------------------------------------------------*/
59 
60 /**AutomaticEnd***************************************************************/
61 
62 /*---------------------------------------------------------------------------*/
63 /* Definition of exported functions */
64 /*---------------------------------------------------------------------------*/
65 
66 /**Function*************************************************************
67 
68  Synopsis [Derive elementary truth tables.]
69 
70  Description []
71 
72  SideEffects []
73 
74  SeeAlso []
75 
76 ***********************************************************************/
77 unsigned ** Extra_TruthElementary( int nVars )
78 {
79  unsigned ** pRes;
80  int i, k, nWords;
81  nWords = Extra_TruthWordNum(nVars);
82  pRes = (unsigned **)Extra_ArrayAlloc( nVars, nWords, 4 );
83  for ( i = 0; i < nVars; i++ )
84  {
85  if ( i < 5 )
86  {
87  for ( k = 0; k < nWords; k++ )
88  pRes[i][k] = s_VarMasks[i][1];
89  }
90  else
91  {
92  for ( k = 0; k < nWords; k++ )
93  if ( k & (1 << (i-5)) )
94  pRes[i][k] = ~(unsigned)0;
95  else
96  pRes[i][k] = 0;
97  }
98  }
99  return pRes;
100 }
101 
102 /**Function*************************************************************
103 
104  Synopsis [Swaps two adjacent variables in the truth table.]
105 
106  Description [Swaps var number Start and var number Start+1 (0-based numbers).
107  The input truth table is pIn. The output truth table is pOut.]
108 
109  SideEffects []
110 
111  SeeAlso []
112 
113 ***********************************************************************/
114 void Extra_TruthSwapAdjacentVars( unsigned * pOut, unsigned * pIn, int nVars, int iVar )
115 {
116  static unsigned PMasks[4][3] = {
117  { 0x99999999, 0x22222222, 0x44444444 },
118  { 0xC3C3C3C3, 0x0C0C0C0C, 0x30303030 },
119  { 0xF00FF00F, 0x00F000F0, 0x0F000F00 },
120  { 0xFF0000FF, 0x0000FF00, 0x00FF0000 }
121  };
122  int nWords = Extra_TruthWordNum( nVars );
123  int i, k, Step, Shift;
124 
125  assert( iVar < nVars - 1 );
126  if ( iVar < 4 )
127  {
128  Shift = (1 << iVar);
129  for ( i = 0; i < nWords; i++ )
130  pOut[i] = (pIn[i] & PMasks[iVar][0]) | ((pIn[i] & PMasks[iVar][1]) << Shift) | ((pIn[i] & PMasks[iVar][2]) >> Shift);
131  }
132  else if ( iVar > 4 )
133  {
134  Step = (1 << (iVar - 5));
135  for ( k = 0; k < nWords; k += 4*Step )
136  {
137  for ( i = 0; i < Step; i++ )
138  pOut[i] = pIn[i];
139  for ( i = 0; i < Step; i++ )
140  pOut[Step+i] = pIn[2*Step+i];
141  for ( i = 0; i < Step; i++ )
142  pOut[2*Step+i] = pIn[Step+i];
143  for ( i = 0; i < Step; i++ )
144  pOut[3*Step+i] = pIn[3*Step+i];
145  pIn += 4*Step;
146  pOut += 4*Step;
147  }
148  }
149  else // if ( iVar == 4 )
150  {
151  for ( i = 0; i < nWords; i += 2 )
152  {
153  pOut[i] = (pIn[i] & 0x0000FFFF) | ((pIn[i+1] & 0x0000FFFF) << 16);
154  pOut[i+1] = (pIn[i+1] & 0xFFFF0000) | ((pIn[i] & 0xFFFF0000) >> 16);
155  }
156  }
157 }
158 
159 /**Function*************************************************************
160 
161  Synopsis [Swaps two adjacent variables in the truth table.]
162 
163  Description [Swaps var number Start and var number Start+1 (0-based numbers).
164  The input truth table is pIn. The output truth table is pOut.]
165 
166  SideEffects []
167 
168  SeeAlso []
169 
170 ***********************************************************************/
171 void Extra_TruthSwapAdjacentVars2( unsigned * pIn, unsigned * pOut, int nVars, int Start )
172 {
173  int nWords = (nVars <= 5)? 1 : (1 << (nVars-5));
174  int i, k, Step;
175 
176  assert( Start < nVars - 1 );
177  switch ( Start )
178  {
179  case 0:
180  for ( i = 0; i < nWords; i++ )
181  pOut[i] = (pIn[i] & 0x99999999) | ((pIn[i] & 0x22222222) << 1) | ((pIn[i] & 0x44444444) >> 1);
182  return;
183  case 1:
184  for ( i = 0; i < nWords; i++ )
185  pOut[i] = (pIn[i] & 0xC3C3C3C3) | ((pIn[i] & 0x0C0C0C0C) << 2) | ((pIn[i] & 0x30303030) >> 2);
186  return;
187  case 2:
188  for ( i = 0; i < nWords; i++ )
189  pOut[i] = (pIn[i] & 0xF00FF00F) | ((pIn[i] & 0x00F000F0) << 4) | ((pIn[i] & 0x0F000F00) >> 4);
190  return;
191  case 3:
192  for ( i = 0; i < nWords; i++ )
193  pOut[i] = (pIn[i] & 0xFF0000FF) | ((pIn[i] & 0x0000FF00) << 8) | ((pIn[i] & 0x00FF0000) >> 8);
194  return;
195  case 4:
196  for ( i = 0; i < nWords; i += 2 )
197  {
198  pOut[i] = (pIn[i] & 0x0000FFFF) | ((pIn[i+1] & 0x0000FFFF) << 16);
199  pOut[i+1] = (pIn[i+1] & 0xFFFF0000) | ((pIn[i] & 0xFFFF0000) >> 16);
200  }
201  return;
202  default:
203  Step = (1 << (Start - 5));
204  for ( k = 0; k < nWords; k += 4*Step )
205  {
206  for ( i = 0; i < Step; i++ )
207  pOut[i] = pIn[i];
208  for ( i = 0; i < Step; i++ )
209  pOut[Step+i] = pIn[2*Step+i];
210  for ( i = 0; i < Step; i++ )
211  pOut[2*Step+i] = pIn[Step+i];
212  for ( i = 0; i < Step; i++ )
213  pOut[3*Step+i] = pIn[3*Step+i];
214  pIn += 4*Step;
215  pOut += 4*Step;
216  }
217  return;
218  }
219 }
220 
221 /**Function*************************************************************
222 
223  Synopsis [Expands the truth table according to the phase.]
224 
225  Description [The input and output truth tables are in pIn/pOut. The current number
226  of variables is nVars. The total number of variables in nVarsAll. The last argument
227  (Phase) contains shows where the variables should go.]
228 
229  SideEffects []
230 
231  SeeAlso []
232 
233 ***********************************************************************/
234 void Extra_TruthStretch( unsigned * pOut, unsigned * pIn, int nVars, int nVarsAll, unsigned Phase )
235 {
236  unsigned * pTemp;
237  int i, k, Var = nVars - 1, Counter = 0;
238  for ( i = nVarsAll - 1; i >= 0; i-- )
239  if ( Phase & (1 << i) )
240  {
241  for ( k = Var; k < i; k++ )
242  {
243  Extra_TruthSwapAdjacentVars( pOut, pIn, nVarsAll, k );
244  pTemp = pIn; pIn = pOut; pOut = pTemp;
245  Counter++;
246  }
247  Var--;
248  }
249  assert( Var == -1 );
250  // swap if it was moved an even number of times
251  if ( !(Counter & 1) )
252  Extra_TruthCopy( pOut, pIn, nVarsAll );
253 }
254 
255 /**Function*************************************************************
256 
257  Synopsis [Shrinks the truth table according to the phase.]
258 
259  Description [The input and output truth tables are in pIn/pOut. The current number
260  of variables is nVars. The total number of variables in nVarsAll. The last argument
261  (Phase) contains shows what variables should remain.]
262 
263  SideEffects []
264 
265  SeeAlso []
266 
267 ***********************************************************************/
268 void Extra_TruthShrink( unsigned * pOut, unsigned * pIn, int nVars, int nVarsAll, unsigned Phase )
269 {
270  unsigned * pTemp;
271  int i, k, Var = 0, Counter = 0;
272  for ( i = 0; i < nVarsAll; i++ )
273  if ( Phase & (1 << i) )
274  {
275  for ( k = i-1; k >= Var; k-- )
276  {
277  Extra_TruthSwapAdjacentVars( pOut, pIn, nVarsAll, k );
278  pTemp = pIn; pIn = pOut; pOut = pTemp;
279  Counter++;
280  }
281  Var++;
282  }
283  assert( Var == nVars );
284  // swap if it was moved an even number of times
285  if ( !(Counter & 1) )
286  Extra_TruthCopy( pOut, pIn, nVarsAll );
287 }
288 
289 
290 /**Function*************************************************************
291 
292  Synopsis [Returns 1 if TT depends on the given variable.]
293 
294  Description []
295 
296  SideEffects []
297 
298  SeeAlso []
299 
300 ***********************************************************************/
301 int Extra_TruthVarInSupport( unsigned * pTruth, int nVars, int iVar )
302 {
303  int nWords = Extra_TruthWordNum( nVars );
304  int i, k, Step;
305 
306  assert( iVar < nVars );
307  switch ( iVar )
308  {
309  case 0:
310  for ( i = 0; i < nWords; i++ )
311  if ( (pTruth[i] & 0x55555555) != ((pTruth[i] & 0xAAAAAAAA) >> 1) )
312  return 1;
313  return 0;
314  case 1:
315  for ( i = 0; i < nWords; i++ )
316  if ( (pTruth[i] & 0x33333333) != ((pTruth[i] & 0xCCCCCCCC) >> 2) )
317  return 1;
318  return 0;
319  case 2:
320  for ( i = 0; i < nWords; i++ )
321  if ( (pTruth[i] & 0x0F0F0F0F) != ((pTruth[i] & 0xF0F0F0F0) >> 4) )
322  return 1;
323  return 0;
324  case 3:
325  for ( i = 0; i < nWords; i++ )
326  if ( (pTruth[i] & 0x00FF00FF) != ((pTruth[i] & 0xFF00FF00) >> 8) )
327  return 1;
328  return 0;
329  case 4:
330  for ( i = 0; i < nWords; i++ )
331  if ( (pTruth[i] & 0x0000FFFF) != ((pTruth[i] & 0xFFFF0000) >> 16) )
332  return 1;
333  return 0;
334  default:
335  Step = (1 << (iVar - 5));
336  for ( k = 0; k < nWords; k += 2*Step )
337  {
338  for ( i = 0; i < Step; i++ )
339  if ( pTruth[i] != pTruth[Step+i] )
340  return 1;
341  pTruth += 2*Step;
342  }
343  return 0;
344  }
345 }
346 
347 /**Function*************************************************************
348 
349  Synopsis [Returns the number of support vars.]
350 
351  Description []
352 
353  SideEffects []
354 
355  SeeAlso []
356 
357 ***********************************************************************/
358 int Extra_TruthSupportSize( unsigned * pTruth, int nVars )
359 {
360  int i, Counter = 0;
361  for ( i = 0; i < nVars; i++ )
362  Counter += Extra_TruthVarInSupport( pTruth, nVars, i );
363  return Counter;
364 }
365 
366 /**Function*************************************************************
367 
368  Synopsis [Returns support of the function.]
369 
370  Description []
371 
372  SideEffects []
373 
374  SeeAlso []
375 
376 ***********************************************************************/
377 int Extra_TruthSupport( unsigned * pTruth, int nVars )
378 {
379  int i, Support = 0;
380  for ( i = 0; i < nVars; i++ )
381  if ( Extra_TruthVarInSupport( pTruth, nVars, i ) )
382  Support |= (1 << i);
383  return Support;
384 }
385 
386 
387 
388 /**Function*************************************************************
389 
390  Synopsis [Computes positive cofactor of the function.]
391 
392  Description []
393 
394  SideEffects []
395 
396  SeeAlso []
397 
398 ***********************************************************************/
399 void Extra_TruthCofactor1( unsigned * pTruth, int nVars, int iVar )
400 {
401  int nWords = Extra_TruthWordNum( nVars );
402  int i, k, Step;
403 
404  assert( iVar < nVars );
405  switch ( iVar )
406  {
407  case 0:
408  for ( i = 0; i < nWords; i++ )
409  pTruth[i] = (pTruth[i] & 0xAAAAAAAA) | ((pTruth[i] & 0xAAAAAAAA) >> 1);
410  return;
411  case 1:
412  for ( i = 0; i < nWords; i++ )
413  pTruth[i] = (pTruth[i] & 0xCCCCCCCC) | ((pTruth[i] & 0xCCCCCCCC) >> 2);
414  return;
415  case 2:
416  for ( i = 0; i < nWords; i++ )
417  pTruth[i] = (pTruth[i] & 0xF0F0F0F0) | ((pTruth[i] & 0xF0F0F0F0) >> 4);
418  return;
419  case 3:
420  for ( i = 0; i < nWords; i++ )
421  pTruth[i] = (pTruth[i] & 0xFF00FF00) | ((pTruth[i] & 0xFF00FF00) >> 8);
422  return;
423  case 4:
424  for ( i = 0; i < nWords; i++ )
425  pTruth[i] = (pTruth[i] & 0xFFFF0000) | ((pTruth[i] & 0xFFFF0000) >> 16);
426  return;
427  default:
428  Step = (1 << (iVar - 5));
429  for ( k = 0; k < nWords; k += 2*Step )
430  {
431  for ( i = 0; i < Step; i++ )
432  pTruth[i] = pTruth[Step+i];
433  pTruth += 2*Step;
434  }
435  return;
436  }
437 }
438 
439 /**Function*************************************************************
440 
441  Synopsis [Computes negative cofactor of the function.]
442 
443  Description []
444 
445  SideEffects []
446 
447  SeeAlso []
448 
449 ***********************************************************************/
450 void Extra_TruthCofactor0( unsigned * pTruth, int nVars, int iVar )
451 {
452  int nWords = Extra_TruthWordNum( nVars );
453  int i, k, Step;
454 
455  assert( iVar < nVars );
456  switch ( iVar )
457  {
458  case 0:
459  for ( i = 0; i < nWords; i++ )
460  pTruth[i] = (pTruth[i] & 0x55555555) | ((pTruth[i] & 0x55555555) << 1);
461  return;
462  case 1:
463  for ( i = 0; i < nWords; i++ )
464  pTruth[i] = (pTruth[i] & 0x33333333) | ((pTruth[i] & 0x33333333) << 2);
465  return;
466  case 2:
467  for ( i = 0; i < nWords; i++ )
468  pTruth[i] = (pTruth[i] & 0x0F0F0F0F) | ((pTruth[i] & 0x0F0F0F0F) << 4);
469  return;
470  case 3:
471  for ( i = 0; i < nWords; i++ )
472  pTruth[i] = (pTruth[i] & 0x00FF00FF) | ((pTruth[i] & 0x00FF00FF) << 8);
473  return;
474  case 4:
475  for ( i = 0; i < nWords; i++ )
476  pTruth[i] = (pTruth[i] & 0x0000FFFF) | ((pTruth[i] & 0x0000FFFF) << 16);
477  return;
478  default:
479  Step = (1 << (iVar - 5));
480  for ( k = 0; k < nWords; k += 2*Step )
481  {
482  for ( i = 0; i < Step; i++ )
483  pTruth[Step+i] = pTruth[i];
484  pTruth += 2*Step;
485  }
486  return;
487  }
488 }
489 
490 
491 /**Function*************************************************************
492 
493  Synopsis [Existentially quantifies the variable.]
494 
495  Description []
496 
497  SideEffects []
498 
499  SeeAlso []
500 
501 ***********************************************************************/
502 void Extra_TruthExist( unsigned * pTruth, int nVars, int iVar )
503 {
504  int nWords = Extra_TruthWordNum( nVars );
505  int i, k, Step;
506 
507  assert( iVar < nVars );
508  switch ( iVar )
509  {
510  case 0:
511  for ( i = 0; i < nWords; i++ )
512  pTruth[i] |= ((pTruth[i] & 0xAAAAAAAA) >> 1) | ((pTruth[i] & 0x55555555) << 1);
513  return;
514  case 1:
515  for ( i = 0; i < nWords; i++ )
516  pTruth[i] |= ((pTruth[i] & 0xCCCCCCCC) >> 2) | ((pTruth[i] & 0x33333333) << 2);
517  return;
518  case 2:
519  for ( i = 0; i < nWords; i++ )
520  pTruth[i] |= ((pTruth[i] & 0xF0F0F0F0) >> 4) | ((pTruth[i] & 0x0F0F0F0F) << 4);
521  return;
522  case 3:
523  for ( i = 0; i < nWords; i++ )
524  pTruth[i] |= ((pTruth[i] & 0xFF00FF00) >> 8) | ((pTruth[i] & 0x00FF00FF) << 8);
525  return;
526  case 4:
527  for ( i = 0; i < nWords; i++ )
528  pTruth[i] |= ((pTruth[i] & 0xFFFF0000) >> 16) | ((pTruth[i] & 0x0000FFFF) << 16);
529  return;
530  default:
531  Step = (1 << (iVar - 5));
532  for ( k = 0; k < nWords; k += 2*Step )
533  {
534  for ( i = 0; i < Step; i++ )
535  {
536  pTruth[i] |= pTruth[Step+i];
537  pTruth[Step+i] = pTruth[i];
538  }
539  pTruth += 2*Step;
540  }
541  return;
542  }
543 }
544 
545 /**Function*************************************************************
546 
547  Synopsis [Existentially quantifies the variable.]
548 
549  Description []
550 
551  SideEffects []
552 
553  SeeAlso []
554 
555 ***********************************************************************/
556 void Extra_TruthForall( unsigned * pTruth, int nVars, int iVar )
557 {
558  int nWords = Extra_TruthWordNum( nVars );
559  int i, k, Step;
560 
561  assert( iVar < nVars );
562  switch ( iVar )
563  {
564  case 0:
565  for ( i = 0; i < nWords; i++ )
566  pTruth[i] &= ((pTruth[i] & 0xAAAAAAAA) >> 1) | ((pTruth[i] & 0x55555555) << 1);
567  return;
568  case 1:
569  for ( i = 0; i < nWords; i++ )
570  pTruth[i] &= ((pTruth[i] & 0xCCCCCCCC) >> 2) | ((pTruth[i] & 0x33333333) << 2);
571  return;
572  case 2:
573  for ( i = 0; i < nWords; i++ )
574  pTruth[i] &= ((pTruth[i] & 0xF0F0F0F0) >> 4) | ((pTruth[i] & 0x0F0F0F0F) << 4);
575  return;
576  case 3:
577  for ( i = 0; i < nWords; i++ )
578  pTruth[i] &= ((pTruth[i] & 0xFF00FF00) >> 8) | ((pTruth[i] & 0x00FF00FF) << 8);
579  return;
580  case 4:
581  for ( i = 0; i < nWords; i++ )
582  pTruth[i] &= ((pTruth[i] & 0xFFFF0000) >> 16) | ((pTruth[i] & 0x0000FFFF) << 16);
583  return;
584  default:
585  Step = (1 << (iVar - 5));
586  for ( k = 0; k < nWords; k += 2*Step )
587  {
588  for ( i = 0; i < Step; i++ )
589  {
590  pTruth[i] &= pTruth[Step+i];
591  pTruth[Step+i] = pTruth[i];
592  }
593  pTruth += 2*Step;
594  }
595  return;
596  }
597 }
598 
599 
600 /**Function*************************************************************
601 
602  Synopsis [Computes negative cofactor of the function.]
603 
604  Description []
605 
606  SideEffects []
607 
608  SeeAlso []
609 
610 ***********************************************************************/
611 void Extra_TruthMux( unsigned * pOut, unsigned * pCof0, unsigned * pCof1, int nVars, int iVar )
612 {
613  int nWords = Extra_TruthWordNum( nVars );
614  int i, k, Step;
615 
616  assert( iVar < nVars );
617  switch ( iVar )
618  {
619  case 0:
620  for ( i = 0; i < nWords; i++ )
621  pOut[i] = (pCof0[i] & 0x55555555) | (pCof1[i] & 0xAAAAAAAA);
622  return;
623  case 1:
624  for ( i = 0; i < nWords; i++ )
625  pOut[i] = (pCof0[i] & 0x33333333) | (pCof1[i] & 0xCCCCCCCC);
626  return;
627  case 2:
628  for ( i = 0; i < nWords; i++ )
629  pOut[i] = (pCof0[i] & 0x0F0F0F0F) | (pCof1[i] & 0xF0F0F0F0);
630  return;
631  case 3:
632  for ( i = 0; i < nWords; i++ )
633  pOut[i] = (pCof0[i] & 0x00FF00FF) | (pCof1[i] & 0xFF00FF00);
634  return;
635  case 4:
636  for ( i = 0; i < nWords; i++ )
637  pOut[i] = (pCof0[i] & 0x0000FFFF) | (pCof1[i] & 0xFFFF0000);
638  return;
639  default:
640  Step = (1 << (iVar - 5));
641  for ( k = 0; k < nWords; k += 2*Step )
642  {
643  for ( i = 0; i < Step; i++ )
644  {
645  pOut[i] = pCof0[i];
646  pOut[Step+i] = pCof1[Step+i];
647  }
648  pOut += 2*Step;
649  }
650  return;
651  }
652 }
653 
654 /**Function*************************************************************
655 
656  Synopsis [Checks symmetry of two variables.]
657 
658  Description []
659 
660  SideEffects []
661 
662  SeeAlso []
663 
664 ***********************************************************************/
665 int Extra_TruthVarsSymm( unsigned * pTruth, int nVars, int iVar0, int iVar1 )
666 {
667  static unsigned uTemp0[16], uTemp1[16];
668  assert( nVars <= 9 );
669  // compute Cof01
670  Extra_TruthCopy( uTemp0, pTruth, nVars );
671  Extra_TruthCofactor0( uTemp0, nVars, iVar0 );
672  Extra_TruthCofactor1( uTemp0, nVars, iVar1 );
673  // compute Cof10
674  Extra_TruthCopy( uTemp1, pTruth, nVars );
675  Extra_TruthCofactor1( uTemp1, nVars, iVar0 );
676  Extra_TruthCofactor0( uTemp1, nVars, iVar1 );
677  // compare
678  return Extra_TruthIsEqual( uTemp0, uTemp1, nVars );
679 }
680 
681 /**Function*************************************************************
682 
683  Synopsis [Checks antisymmetry of two variables.]
684 
685  Description []
686 
687  SideEffects []
688 
689  SeeAlso []
690 
691 ***********************************************************************/
692 int Extra_TruthVarsAntiSymm( unsigned * pTruth, int nVars, int iVar0, int iVar1 )
693 {
694  static unsigned uTemp0[16], uTemp1[16];
695  assert( nVars <= 9 );
696  // compute Cof00
697  Extra_TruthCopy( uTemp0, pTruth, nVars );
698  Extra_TruthCofactor0( uTemp0, nVars, iVar0 );
699  Extra_TruthCofactor0( uTemp0, nVars, iVar1 );
700  // compute Cof11
701  Extra_TruthCopy( uTemp1, pTruth, nVars );
702  Extra_TruthCofactor1( uTemp1, nVars, iVar0 );
703  Extra_TruthCofactor1( uTemp1, nVars, iVar1 );
704  // compare
705  return Extra_TruthIsEqual( uTemp0, uTemp1, nVars );
706 }
707 
708 /**Function*************************************************************
709 
710  Synopsis [Changes phase of the function w.r.t. one variable.]
711 
712  Description []
713 
714  SideEffects []
715 
716  SeeAlso []
717 
718 ***********************************************************************/
719 void Extra_TruthChangePhase( unsigned * pTruth, int nVars, int iVar )
720 {
721  int nWords = Extra_TruthWordNum( nVars );
722  int i, k, Step;
723  unsigned Temp;
724 
725  assert( iVar < nVars );
726  switch ( iVar )
727  {
728  case 0:
729  for ( i = 0; i < nWords; i++ )
730  pTruth[i] = ((pTruth[i] & 0x55555555) << 1) | ((pTruth[i] & 0xAAAAAAAA) >> 1);
731  return;
732  case 1:
733  for ( i = 0; i < nWords; i++ )
734  pTruth[i] = ((pTruth[i] & 0x33333333) << 2) | ((pTruth[i] & 0xCCCCCCCC) >> 2);
735  return;
736  case 2:
737  for ( i = 0; i < nWords; i++ )
738  pTruth[i] = ((pTruth[i] & 0x0F0F0F0F) << 4) | ((pTruth[i] & 0xF0F0F0F0) >> 4);
739  return;
740  case 3:
741  for ( i = 0; i < nWords; i++ )
742  pTruth[i] = ((pTruth[i] & 0x00FF00FF) << 8) | ((pTruth[i] & 0xFF00FF00) >> 8);
743  return;
744  case 4:
745  for ( i = 0; i < nWords; i++ )
746  pTruth[i] = ((pTruth[i] & 0x0000FFFF) << 16) | ((pTruth[i] & 0xFFFF0000) >> 16);
747  return;
748  default:
749  Step = (1 << (iVar - 5));
750  for ( k = 0; k < nWords; k += 2*Step )
751  {
752  for ( i = 0; i < Step; i++ )
753  {
754  Temp = pTruth[i];
755  pTruth[i] = pTruth[Step+i];
756  pTruth[Step+i] = Temp;
757  }
758  pTruth += 2*Step;
759  }
760  return;
761  }
762 }
763 
764 /**Function*************************************************************
765 
766  Synopsis [Computes minimum overlap in supports of cofactors.]
767 
768  Description []
769 
770  SideEffects []
771 
772  SeeAlso []
773 
774 ***********************************************************************/
775 int Extra_TruthMinCofSuppOverlap( unsigned * pTruth, int nVars, int * pVarMin )
776 {
777  static unsigned uCofactor[16];
778  int i, ValueCur, ValueMin, VarMin;
779  unsigned uSupp0, uSupp1;
780  int nVars0, nVars1;
781  assert( nVars <= 9 );
782  ValueMin = 32;
783  VarMin = -1;
784  for ( i = 0; i < nVars; i++ )
785  {
786  // get negative cofactor
787  Extra_TruthCopy( uCofactor, pTruth, nVars );
788  Extra_TruthCofactor0( uCofactor, nVars, i );
789  uSupp0 = Extra_TruthSupport( uCofactor, nVars );
790  nVars0 = Extra_WordCountOnes( uSupp0 );
791 //Extra_PrintBinary( stdout, &uSupp0, 8 ); printf( "\n" );
792  // get positive cofactor
793  Extra_TruthCopy( uCofactor, pTruth, nVars );
794  Extra_TruthCofactor1( uCofactor, nVars, i );
795  uSupp1 = Extra_TruthSupport( uCofactor, nVars );
796  nVars1 = Extra_WordCountOnes( uSupp1 );
797 //Extra_PrintBinary( stdout, &uSupp1, 8 ); printf( "\n" );
798  // get the number of common vars
799  ValueCur = Extra_WordCountOnes( uSupp0 & uSupp1 );
800  if ( ValueMin > ValueCur && nVars0 <= 5 && nVars1 <= 5 )
801  {
802  ValueMin = ValueCur;
803  VarMin = i;
804  }
805  if ( ValueMin == 0 )
806  break;
807  }
808  if ( pVarMin )
809  *pVarMin = VarMin;
810  return ValueMin;
811 }
812 
813 
814 /**Function*************************************************************
815 
816  Synopsis [Counts the number of 1's in each cofactor.]
817 
818  Description [The resulting numbers are stored in the array of shorts,
819  whose length is 2*nVars. The number of 1's is counted in a different
820  space than the original function. For example, if the function depends
821  on k variables, the cofactors are assumed to depend on k-1 variables.]
822 
823  SideEffects []
824 
825  SeeAlso []
826 
827 ***********************************************************************/
828 void Extra_TruthCountOnesInCofs( unsigned * pTruth, int nVars, short * pStore )
829 {
830  int nWords = Extra_TruthWordNum( nVars );
831  int i, k, Counter;
832  memset( pStore, 0, sizeof(short) * 2 * nVars );
833  if ( nVars <= 5 )
834  {
835  if ( nVars > 0 )
836  {
837  pStore[2*0+0] = Extra_WordCountOnes( pTruth[0] & 0x55555555 );
838  pStore[2*0+1] = Extra_WordCountOnes( pTruth[0] & 0xAAAAAAAA );
839  }
840  if ( nVars > 1 )
841  {
842  pStore[2*1+0] = Extra_WordCountOnes( pTruth[0] & 0x33333333 );
843  pStore[2*1+1] = Extra_WordCountOnes( pTruth[0] & 0xCCCCCCCC );
844  }
845  if ( nVars > 2 )
846  {
847  pStore[2*2+0] = Extra_WordCountOnes( pTruth[0] & 0x0F0F0F0F );
848  pStore[2*2+1] = Extra_WordCountOnes( pTruth[0] & 0xF0F0F0F0 );
849  }
850  if ( nVars > 3 )
851  {
852  pStore[2*3+0] = Extra_WordCountOnes( pTruth[0] & 0x00FF00FF );
853  pStore[2*3+1] = Extra_WordCountOnes( pTruth[0] & 0xFF00FF00 );
854  }
855  if ( nVars > 4 )
856  {
857  pStore[2*4+0] = Extra_WordCountOnes( pTruth[0] & 0x0000FFFF );
858  pStore[2*4+1] = Extra_WordCountOnes( pTruth[0] & 0xFFFF0000 );
859  }
860  return;
861  }
862  // nVars >= 6
863  // count 1's for all other variables
864  for ( k = 0; k < nWords; k++ )
865  {
866  Counter = Extra_WordCountOnes( pTruth[k] );
867  for ( i = 5; i < nVars; i++ )
868  if ( k & (1 << (i-5)) )
869  pStore[2*i+1] += Counter;
870  else
871  pStore[2*i+0] += Counter;
872  }
873  // count 1's for the first five variables
874  for ( k = 0; k < nWords/2; k++ )
875  {
876  pStore[2*0+0] += Extra_WordCountOnes( (pTruth[0] & 0x55555555) | ((pTruth[1] & 0x55555555) << 1) );
877  pStore[2*0+1] += Extra_WordCountOnes( (pTruth[0] & 0xAAAAAAAA) | ((pTruth[1] & 0xAAAAAAAA) >> 1) );
878  pStore[2*1+0] += Extra_WordCountOnes( (pTruth[0] & 0x33333333) | ((pTruth[1] & 0x33333333) << 2) );
879  pStore[2*1+1] += Extra_WordCountOnes( (pTruth[0] & 0xCCCCCCCC) | ((pTruth[1] & 0xCCCCCCCC) >> 2) );
880  pStore[2*2+0] += Extra_WordCountOnes( (pTruth[0] & 0x0F0F0F0F) | ((pTruth[1] & 0x0F0F0F0F) << 4) );
881  pStore[2*2+1] += Extra_WordCountOnes( (pTruth[0] & 0xF0F0F0F0) | ((pTruth[1] & 0xF0F0F0F0) >> 4) );
882  pStore[2*3+0] += Extra_WordCountOnes( (pTruth[0] & 0x00FF00FF) | ((pTruth[1] & 0x00FF00FF) << 8) );
883  pStore[2*3+1] += Extra_WordCountOnes( (pTruth[0] & 0xFF00FF00) | ((pTruth[1] & 0xFF00FF00) >> 8) );
884  pStore[2*4+0] += Extra_WordCountOnes( (pTruth[0] & 0x0000FFFF) | ((pTruth[1] & 0x0000FFFF) << 16) );
885  pStore[2*4+1] += Extra_WordCountOnes( (pTruth[0] & 0xFFFF0000) | ((pTruth[1] & 0xFFFF0000) >> 16) );
886  pTruth += 2;
887  }
888 }
889 
890 
891 /**Function*************************************************************
892 
893  Synopsis [Canonicize the truth table.]
894 
895  Description []
896 
897  SideEffects []
898 
899  SeeAlso []
900 
901 ***********************************************************************/
902 unsigned Extra_TruthHash( unsigned * pIn, int nWords )
903 {
904  // The 1,024 smallest prime numbers used to compute the hash value
905  // http://www.math.utah.edu/~alfeld/math/primelist.html
906  static int HashPrimes[1024] = { 2, 3, 5,
907  7, 11, 13, 17, 19, 23, 29, 31, 37, 41, 43, 47, 53, 59, 61, 67, 71, 73, 79, 83, 89, 97,
908  101, 103, 107, 109, 113, 127, 131, 137, 139, 149, 151, 157, 163, 167, 173, 179, 181, 191,
909  193, 197, 199, 211, 223, 227, 229, 233, 239, 241, 251, 257, 263, 269, 271, 277, 281, 283,
910  293, 307, 311, 313, 317, 331, 337, 347, 349, 353, 359, 367, 373, 379, 383, 389, 397, 401,
911  409, 419, 421, 431, 433, 439, 443, 449, 457, 461, 463, 467, 479, 487, 491, 499, 503, 509,
912  521, 523, 541, 547, 557, 563, 569, 571, 577, 587, 593, 599, 601, 607, 613, 617, 619, 631,
913  641, 643, 647, 653, 659, 661, 673, 677, 683, 691, 701, 709, 719, 727, 733, 739, 743, 751,
914  757, 761, 769, 773, 787, 797, 809, 811, 821, 823, 827, 829, 839, 853, 857, 859, 863, 877,
915  881, 883, 887, 907, 911, 919, 929, 937, 941, 947, 953, 967, 971, 977, 983, 991, 997,
916  1009, 1013, 1019, 1021, 1031, 1033, 1039, 1049, 1051, 1061, 1063, 1069, 1087, 1091,
917  1093, 1097, 1103, 1109, 1117, 1123, 1129, 1151, 1153, 1163, 1171, 1181, 1187, 1193,
918  1201, 1213, 1217, 1223, 1229, 1231, 1237, 1249, 1259, 1277, 1279, 1283, 1289, 1291,
919  1297, 1301, 1303, 1307, 1319, 1321, 1327, 1361, 1367, 1373, 1381, 1399, 1409, 1423,
920  1427, 1429, 1433, 1439, 1447, 1451, 1453, 1459, 1471, 1481, 1483, 1487, 1489, 1493,
921  1499, 1511, 1523, 1531, 1543, 1549, 1553, 1559, 1567, 1571, 1579, 1583, 1597, 1601,
922  1607, 1609, 1613, 1619, 1621, 1627, 1637, 1657, 1663, 1667, 1669, 1693, 1697, 1699,
923  1709, 1721, 1723, 1733, 1741, 1747, 1753, 1759, 1777, 1783, 1787, 1789, 1801, 1811,
924  1823, 1831, 1847, 1861, 1867, 1871, 1873, 1877, 1879, 1889, 1901, 1907, 1913, 1931,
925  1933, 1949, 1951, 1973, 1979, 1987, 1993, 1997, 1999, 2003, 2011, 2017, 2027, 2029,
926  2039, 2053, 2063, 2069, 2081, 2083, 2087, 2089, 2099, 2111, 2113, 2129, 2131, 2137,
927  2141, 2143, 2153, 2161, 2179, 2203, 2207, 2213, 2221, 2237, 2239, 2243, 2251, 2267,
928  2269, 2273, 2281, 2287, 2293, 2297, 2309, 2311, 2333, 2339, 2341, 2347, 2351, 2357,
929  2371, 2377, 2381, 2383, 2389, 2393, 2399, 2411, 2417, 2423, 2437, 2441, 2447, 2459,
930  2467, 2473, 2477, 2503, 2521, 2531, 2539, 2543, 2549, 2551, 2557, 2579, 2591, 2593,
931  2609, 2617, 2621, 2633, 2647, 2657, 2659, 2663, 2671, 2677, 2683, 2687, 2689, 2693,
932  2699, 2707, 2711, 2713, 2719, 2729, 2731, 2741, 2749, 2753, 2767, 2777, 2789, 2791,
933  2797, 2801, 2803, 2819, 2833, 2837, 2843, 2851, 2857, 2861, 2879, 2887, 2897, 2903,
934  2909, 2917, 2927, 2939, 2953, 2957, 2963, 2969, 2971, 2999, 3001, 3011, 3019, 3023,
935  3037, 3041, 3049, 3061, 3067, 3079, 3083, 3089, 3109, 3119, 3121, 3137, 3163, 3167,
936  3169, 3181, 3187, 3191, 3203, 3209, 3217, 3221, 3229, 3251, 3253, 3257, 3259, 3271,
937  3299, 3301, 3307, 3313, 3319, 3323, 3329, 3331, 3343, 3347, 3359, 3361, 3371, 3373,
938  3389, 3391, 3407, 3413, 3433, 3449, 3457, 3461, 3463, 3467, 3469, 3491, 3499, 3511,
939  3517, 3527, 3529, 3533, 3539, 3541, 3547, 3557, 3559, 3571, 3581, 3583, 3593, 3607,
940  3613, 3617, 3623, 3631, 3637, 3643, 3659, 3671, 3673, 3677, 3691, 3697, 3701, 3709,
941  3719, 3727, 3733, 3739, 3761, 3767, 3769, 3779, 3793, 3797, 3803, 3821, 3823, 3833,
942  3847, 3851, 3853, 3863, 3877, 3881, 3889, 3907, 3911, 3917, 3919, 3923, 3929, 3931,
943  3943, 3947, 3967, 3989, 4001, 4003, 4007, 4013, 4019, 4021, 4027, 4049, 4051, 4057,
944  4073, 4079, 4091, 4093, 4099, 4111, 4127, 4129, 4133, 4139, 4153, 4157, 4159, 4177,
945  4201, 4211, 4217, 4219, 4229, 4231, 4241, 4243, 4253, 4259, 4261, 4271, 4273, 4283,
946  4289, 4297, 4327, 4337, 4339, 4349, 4357, 4363, 4373, 4391, 4397, 4409, 4421, 4423,
947  4441, 4447, 4451, 4457, 4463, 4481, 4483, 4493, 4507, 4513, 4517, 4519, 4523, 4547,
948  4549, 4561, 4567, 4583, 4591, 4597, 4603, 4621, 4637, 4639, 4643, 4649, 4651, 4657,
949  4663, 4673, 4679, 4691, 4703, 4721, 4723, 4729, 4733, 4751, 4759, 4783, 4787, 4789,
950  4793, 4799, 4801, 4813, 4817, 4831, 4861, 4871, 4877, 4889, 4903, 4909, 4919, 4931,
951  4933, 4937, 4943, 4951, 4957, 4967, 4969, 4973, 4987, 4993, 4999, 5003, 5009, 5011,
952  5021, 5023, 5039, 5051, 5059, 5077, 5081, 5087, 5099, 5101, 5107, 5113, 5119, 5147,
953  5153, 5167, 5171, 5179, 5189, 5197, 5209, 5227, 5231, 5233, 5237, 5261, 5273, 5279,
954  5281, 5297, 5303, 5309, 5323, 5333, 5347, 5351, 5381, 5387, 5393, 5399, 5407, 5413,
955  5417, 5419, 5431, 5437, 5441, 5443, 5449, 5471, 5477, 5479, 5483, 5501, 5503, 5507,
956  5519, 5521, 5527, 5531, 5557, 5563, 5569, 5573, 5581, 5591, 5623, 5639, 5641, 5647,
957  5651, 5653, 5657, 5659, 5669, 5683, 5689, 5693, 5701, 5711, 5717, 5737, 5741, 5743,
958  5749, 5779, 5783, 5791, 5801, 5807, 5813, 5821, 5827, 5839, 5843, 5849, 5851, 5857,
959  5861, 5867, 5869, 5879, 5881, 5897, 5903, 5923, 5927, 5939, 5953, 5981, 5987, 6007,
960  6011, 6029, 6037, 6043, 6047, 6053, 6067, 6073, 6079, 6089, 6091, 6101, 6113, 6121,
961  6131, 6133, 6143, 6151, 6163, 6173, 6197, 6199, 6203, 6211, 6217, 6221, 6229, 6247,
962  6257, 6263, 6269, 6271, 6277, 6287, 6299, 6301, 6311, 6317, 6323, 6329, 6337, 6343,
963  6353, 6359, 6361, 6367, 6373, 6379, 6389, 6397, 6421, 6427, 6449, 6451, 6469, 6473,
964  6481, 6491, 6521, 6529, 6547, 6551, 6553, 6563, 6569, 6571, 6577, 6581, 6599, 6607,
965  6619, 6637, 6653, 6659, 6661, 6673, 6679, 6689, 6691, 6701, 6703, 6709, 6719, 6733,
966  6737, 6761, 6763, 6779, 6781, 6791, 6793, 6803, 6823, 6827, 6829, 6833, 6841, 6857,
967  6863, 6869, 6871, 6883, 6899, 6907, 6911, 6917, 6947, 6949, 6959, 6961, 6967, 6971,
968  6977, 6983, 6991, 6997, 7001, 7013, 7019, 7027, 7039, 7043, 7057, 7069, 7079, 7103,
969  7109, 7121, 7127, 7129, 7151, 7159, 7177, 7187, 7193, 7207, 7211, 7213, 7219, 7229,
970  7237, 7243, 7247, 7253, 7283, 7297, 7307, 7309, 7321, 7331, 7333, 7349, 7351, 7369,
971  7393, 7411, 7417, 7433, 7451, 7457, 7459, 7477, 7481, 7487, 7489, 7499, 7507, 7517,
972  7523, 7529, 7537, 7541, 7547, 7549, 7559, 7561, 7573, 7577, 7583, 7589, 7591, 7603,
973  7607, 7621, 7639, 7643, 7649, 7669, 7673, 7681, 7687, 7691, 7699, 7703, 7717, 7723,
974  7727, 7741, 7753, 7757, 7759, 7789, 7793, 7817, 7823, 7829, 7841, 7853, 7867, 7873,
975  7877, 7879, 7883, 7901, 7907, 7919, 7927, 7933, 7937, 7949, 7951, 7963, 7993, 8009,
976  8011, 8017, 8039, 8053, 8059, 8069, 8081, 8087, 8089, 8093, 8101, 8111, 8117, 8123,
977  8147, 8161 };
978  int i;
979  unsigned uHashKey;
980  assert( nWords <= 1024 );
981  uHashKey = 0;
982  for ( i = 0; i < nWords; i++ )
983  uHashKey ^= HashPrimes[i] * pIn[i];
984  return uHashKey;
985 }
986 
987 
988 /**Function*************************************************************
989 
990  Synopsis [Canonicize the truth table.]
991 
992  Description [Returns the phase. ]
993 
994  SideEffects []
995 
996  SeeAlso []
997 
998 ***********************************************************************/
999 unsigned Extra_TruthSemiCanonicize( unsigned * pInOut, unsigned * pAux, int nVars, char * pCanonPerm, short * pStore )
1000 {
1001  unsigned * pIn = pInOut, * pOut = pAux, * pTemp;
1002  int nWords = Extra_TruthWordNum( nVars );
1003  int i, Temp, fChange, Counter, nOnes;//, k, j, w, Limit;
1004  unsigned uCanonPhase;
1005 
1006  // canonicize output
1007  uCanonPhase = 0;
1008  nOnes = Extra_TruthCountOnes(pIn, nVars);
1009  if ( (nOnes > nWords * 16) || ((nOnes == nWords * 16) && (pIn[0] & 1)) )
1010  {
1011  uCanonPhase |= (1 << nVars);
1012  Extra_TruthNot( pIn, pIn, nVars );
1013  }
1014 
1015  // collect the minterm counts
1016  Extra_TruthCountOnesInCofs( pIn, nVars, pStore );
1017 
1018  // canonicize phase
1019  for ( i = 0; i < nVars; i++ )
1020  {
1021  if ( pStore[2*i+0] <= pStore[2*i+1] )
1022  continue;
1023  uCanonPhase |= (1 << i);
1024  Temp = pStore[2*i+0];
1025  pStore[2*i+0] = pStore[2*i+1];
1026  pStore[2*i+1] = Temp;
1027  Extra_TruthChangePhase( pIn, nVars, i );
1028  }
1029 
1030 // Extra_PrintHexadecimal( stdout, pIn, nVars );
1031 // printf( "\n" );
1032 
1033  // permute
1034  Counter = 0;
1035  do {
1036  fChange = 0;
1037  for ( i = 0; i < nVars-1; i++ )
1038  {
1039  if ( pStore[2*i] <= pStore[2*(i+1)] )
1040  continue;
1041  Counter++;
1042  fChange = 1;
1043 
1044  Temp = pCanonPerm[i];
1045  pCanonPerm[i] = pCanonPerm[i+1];
1046  pCanonPerm[i+1] = Temp;
1047 
1048  Temp = pStore[2*i];
1049  pStore[2*i] = pStore[2*(i+1)];
1050  pStore[2*(i+1)] = Temp;
1051 
1052  Temp = pStore[2*i+1];
1053  pStore[2*i+1] = pStore[2*(i+1)+1];
1054  pStore[2*(i+1)+1] = Temp;
1055 
1056  Extra_TruthSwapAdjacentVars( pOut, pIn, nVars, i );
1057  pTemp = pIn; pIn = pOut; pOut = pTemp;
1058  }
1059  } while ( fChange );
1060 
1061 /*
1062  Extra_PrintBinary( stdout, &uCanonPhase, nVars+1 ); printf( " : " );
1063  for ( i = 0; i < nVars; i++ )
1064  printf( "%d=%d/%d ", pCanonPerm[i], pStore[2*i], pStore[2*i+1] );
1065  printf( " C = %d\n", Counter );
1066  Extra_PrintHexadecimal( stdout, pIn, nVars );
1067  printf( "\n" );
1068 */
1069 
1070 /*
1071  // process symmetric variable groups
1072  uSymms = 0;
1073  for ( i = 0; i < nVars-1; i++ )
1074  {
1075  if ( pStore[2*i] != pStore[2*(i+1)] ) // i and i+1 cannot be symmetric
1076  continue;
1077  if ( pStore[2*i] != pStore[2*i+1] )
1078  continue;
1079  if ( Extra_TruthVarsSymm( pIn, nVars, i, i+1 ) )
1080  continue;
1081  if ( Extra_TruthVarsAntiSymm( pIn, nVars, i, i+1 ) )
1082  Extra_TruthChangePhase( pIn, nVars, i+1 );
1083  }
1084 */
1085 
1086 /*
1087  // process symmetric variable groups
1088  uSymms = 0;
1089  for ( i = 0; i < nVars-1; i++ )
1090  {
1091  if ( pStore[2*i] != pStore[2*(i+1)] ) // i and i+1 cannot be symmetric
1092  continue;
1093  // i and i+1 can be symmetric
1094  // find the end of this group
1095  for ( k = i+1; k < nVars; k++ )
1096  if ( pStore[2*i] != pStore[2*k] )
1097  break;
1098  Limit = k;
1099  assert( i < Limit-1 );
1100  // go through the variables in this group
1101  for ( j = i + 1; j < Limit; j++ )
1102  {
1103  // check symmetry
1104  if ( Extra_TruthVarsSymm( pIn, nVars, i, j ) )
1105  {
1106  uSymms |= (1 << j);
1107  continue;
1108  }
1109  // they are phase-unknown
1110  if ( pStore[2*i] == pStore[2*i+1] )
1111  {
1112  if ( Extra_TruthVarsAntiSymm( pIn, nVars, i, j ) )
1113  {
1114  Extra_TruthChangePhase( pIn, nVars, j );
1115  uCanonPhase ^= (1 << j);
1116  uSymms |= (1 << j);
1117  continue;
1118  }
1119  }
1120 
1121  // they are not symmetric - move j as far as it goes in the group
1122  for ( k = j; k < Limit-1; k++ )
1123  {
1124  Counter++;
1125 
1126  Temp = pCanonPerm[k];
1127  pCanonPerm[k] = pCanonPerm[k+1];
1128  pCanonPerm[k+1] = Temp;
1129 
1130  assert( pStore[2*k] == pStore[2*(k+1)] );
1131  Extra_TruthSwapAdjacentVars( pOut, pIn, nVars, k );
1132  pTemp = pIn; pIn = pOut; pOut = pTemp;
1133  }
1134  Limit--;
1135  j--;
1136  }
1137  i = Limit - 1;
1138  }
1139 */
1140 
1141  // swap if it was moved an even number of times
1142  if ( Counter & 1 )
1143  Extra_TruthCopy( pOut, pIn, nVars );
1144  return uCanonPhase;
1145 }
1146 
1147 ////////////////////////////////////////////////////////////////////////
1148 /// END OF FILE ///
1149 ////////////////////////////////////////////////////////////////////////
1150 
1151 
1152 ABC_NAMESPACE_IMPL_END
1153 
memset
char * memset()
Extra_TruthMinCofSuppOverlap
int Extra_TruthMinCofSuppOverlap(unsigned *pTruth, int nVars, int *pVarMin)
Definition: extraUtilTruth.c:775
Extra_ArrayAlloc
void ** Extra_ArrayAlloc(int nCols, int nRows, int Size)
Definition: extraUtilMisc.c:880
Extra_TruthStretch
void Extra_TruthStretch(unsigned *pOut, unsigned *pIn, int nVars, int nVarsAll, unsigned Phase)
Definition: extraUtilTruth.c:234
Extra_TruthShrink
void Extra_TruthShrink(unsigned *pOut, unsigned *pIn, int nVars, int nVarsAll, unsigned Phase)
Definition: extraUtilTruth.c:268
Extra_TruthSwapAdjacentVars
void Extra_TruthSwapAdjacentVars(unsigned *pOut, unsigned *pIn, int nVars, int iVar)
Definition: extraUtilTruth.c:114
nWords
int nWords
Definition: abcNpn.c:127
Extra_TruthVarsSymm
int Extra_TruthVarsSymm(unsigned *pTruth, int nVars, int iVar0, int iVar1)
Definition: extraUtilTruth.c:665
Extra_TruthCofactor1
void Extra_TruthCofactor1(unsigned *pTruth, int nVars, int iVar)
Definition: extraUtilTruth.c:399
Extra_TruthSupport
int Extra_TruthSupport(unsigned *pTruth, int nVars)
Definition: extraUtilTruth.c:377
ABC_NAMESPACE_IMPL_END
#define ABC_NAMESPACE_IMPL_END
Definition: abc_global.h:108
Extra_TruthSupportSize
int Extra_TruthSupportSize(unsigned *pTruth, int nVars)
Definition: extraUtilTruth.c:358
Extra_TruthCountOnes
static int Extra_TruthCountOnes(unsigned *pIn, int nVars)
Definition: extra.h:263
Extra_TruthHash
unsigned Extra_TruthHash(unsigned *pIn, int nWords)
Definition: extraUtilTruth.c:902
Counter
static int Counter
Definition: extraBddMisc.c:1877
Extra_TruthVarsAntiSymm
int Extra_TruthVarsAntiSymm(unsigned *pTruth, int nVars, int iVar0, int iVar1)
Definition: extraUtilTruth.c:692
PMasks
static word PMasks[5][3]
Definition: ifDec07.c:44
Extra_TruthWordNum
static int Extra_TruthWordNum(int nVars)
Definition: extra.h:249
Extra_TruthIsEqual
static int Extra_TruthIsEqual(unsigned *pIn0, unsigned *pIn1, int nVars)
Definition: extra.h:270
Extra_TruthSemiCanonicize
unsigned Extra_TruthSemiCanonicize(unsigned *pInOut, unsigned *pAux, int nVars, char *pCanonPerm, short *pStore)
Definition: extraUtilTruth.c:999
ABC_NAMESPACE_IMPL_START
#define ABC_NAMESPACE_IMPL_START
Definition: abc_global.h:107
Extra_TruthCountOnesInCofs
void Extra_TruthCountOnesInCofs(unsigned *pTruth, int nVars, short *pStore)
Definition: extraUtilTruth.c:828
Extra_TruthCofactor0
void Extra_TruthCofactor0(unsigned *pTruth, int nVars, int iVar)
Definition: extraUtilTruth.c:450
Extra_TruthExist
void Extra_TruthExist(unsigned *pTruth, int nVars, int iVar)
Definition: extraUtilTruth.c:502
Extra_TruthForall
void Extra_TruthForall(unsigned *pTruth, int nVars, int iVar)
Definition: extraUtilTruth.c:556
s_VarMasks
static ABC_NAMESPACE_IMPL_START unsigned s_VarMasks[5][2]
Definition: extraUtilTruth.c:42
Minisat::Var
int Var
Definition: SolverTypes.h:42
Extra_WordCountOnes
static int Extra_WordCountOnes(unsigned uWord)
Definition: extra.h:255
assert
#define assert(ex)
Definition: util_old.h:213
Extra_TruthMux
void Extra_TruthMux(unsigned *pOut, unsigned *pCof0, unsigned *pCof1, int nVars, int iVar)
Definition: extraUtilTruth.c:611
Extra_TruthNot
static void Extra_TruthNot(unsigned *pOut, unsigned *pIn, int nVars)
Definition: extra.h:320
Extra_TruthVarInSupport
int Extra_TruthVarInSupport(unsigned *pTruth, int nVars, int iVar)
Definition: extraUtilTruth.c:301
Extra_TruthChangePhase
void Extra_TruthChangePhase(unsigned *pTruth, int nVars, int iVar)
Definition: extraUtilTruth.c:719
Extra_TruthCopy
static void Extra_TruthCopy(unsigned *pOut, unsigned *pIn, int nVars)
Definition: extra.h:302
Extra_TruthSwapAdjacentVars2
void Extra_TruthSwapAdjacentVars2(unsigned *pIn, unsigned *pOut, int nVars, int Start)
Definition: extraUtilTruth.c:171
Extra_TruthElementary
unsigned ** Extra_TruthElementary(int nVars)
Definition: extraUtilTruth.c:77