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