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 ***********************************************************************/
Extra_TruthElementary(int nVars)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 ***********************************************************************/
Extra_TruthSwapAdjacentVars(unsigned * pOut,unsigned * pIn,int nVars,int iVar)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 ***********************************************************************/
Extra_TruthSwapAdjacentVars2(unsigned * pIn,unsigned * pOut,int nVars,int Start)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 ***********************************************************************/
Extra_TruthStretch(unsigned * pOut,unsigned * pIn,int nVars,int nVarsAll,unsigned Phase)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 ***********************************************************************/
Extra_TruthShrink(unsigned * pOut,unsigned * pIn,int nVars,int nVarsAll,unsigned Phase)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 ***********************************************************************/
Extra_TruthVarInSupport(unsigned * pTruth,int nVars,int iVar)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 ***********************************************************************/
Extra_TruthSupportSize(unsigned * pTruth,int nVars)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 ***********************************************************************/
Extra_TruthSupport(unsigned * pTruth,int nVars)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 ***********************************************************************/
Extra_TruthCofactor1(unsigned * pTruth,int nVars,int iVar)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 ***********************************************************************/
Extra_TruthCofactor0(unsigned * pTruth,int nVars,int iVar)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 ***********************************************************************/
Extra_TruthExist(unsigned * pTruth,int nVars,int iVar)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 ***********************************************************************/
Extra_TruthForall(unsigned * pTruth,int nVars,int iVar)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 ***********************************************************************/
Extra_TruthMux(unsigned * pOut,unsigned * pCof0,unsigned * pCof1,int nVars,int iVar)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 ***********************************************************************/
Extra_TruthVarsSymm(unsigned * pTruth,int nVars,int iVar0,int iVar1)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 ***********************************************************************/
Extra_TruthVarsAntiSymm(unsigned * pTruth,int nVars,int iVar0,int iVar1)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 ***********************************************************************/
Extra_TruthChangePhase(unsigned * pTruth,int nVars,int iVar)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 ***********************************************************************/
Extra_TruthMinCofSuppOverlap(unsigned * pTruth,int nVars,int * pVarMin)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 ***********************************************************************/
Extra_TruthCountOnesInCofs(unsigned * pTruth,int nVars,short * pStore)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 ***********************************************************************/
Extra_TruthHash(unsigned * pIn,int nWords)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 ***********************************************************************/
Extra_TruthSemiCanonicize(unsigned * pInOut,unsigned * pAux,int nVars,char * pCanonPerm,short * pStore)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 
1154