1 /**CFile****************************************************************
2
3 FileName [dauCanon.c]
4
5 SystemName [ABC: Logic synthesis and verification system.]
6
7 PackageName [DAG-aware unmapping.]
8
9 Synopsis [Canonical form computation.]
10
11 Author [Alan Mishchenko]
12
13 Affiliation [UC Berkeley]
14
15 Date [Ver. 1.0. Started - June 20, 2005.]
16
17 Revision [$Id: dauCanon.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
18
19 ***********************************************************************/
20
21 #include "dauInt.h"
22 #include "misc/util/utilTruth.h"
23 #include "misc/vec/vecMem.h"
24 #include "bool/lucky/lucky.h"
25 #include <math.h>
26
27 ABC_NAMESPACE_IMPL_START
28
29 ////////////////////////////////////////////////////////////////////////
30 /// DECLARATIONS ///
31 ////////////////////////////////////////////////////////////////////////
32
33 static word s_CMasks6[5] = {
34 ABC_CONST(0x1111111111111111),
35 ABC_CONST(0x0303030303030303),
36 ABC_CONST(0x000F000F000F000F),
37 ABC_CONST(0x000000FF000000FF),
38 ABC_CONST(0x000000000000FFFF)
39 };
40
41 ////////////////////////////////////////////////////////////////////////
42 /// FUNCTION DEFINITIONS ///
43 ////////////////////////////////////////////////////////////////////////
44
45 /**Function*************************************************************
46
47 Synopsis [Compares Cof0 and Cof1.]
48
49 Description []
50
51 SideEffects []
52
53 SeeAlso []
54
55 ***********************************************************************/
56 /*
57 static inline int Abc_TtCompare1VarCofs( word * pTruth, int nWords, int iVar )
58 {
59 if ( nWords == 1 )
60 {
61 word Cof0 = pTruth[0] & s_Truths6Neg[iVar];
62 word Cof1 = (pTruth[0] >> (1 << iVar)) & s_Truths6Neg[iVar];
63 if ( Cof0 != Cof1 )
64 return Cof0 < Cof1 ? -1 : 1;
65 return 0;
66 }
67 if ( iVar <= 5 )
68 {
69 word Cof0, Cof1;
70 int w, shift = (1 << iVar);
71 for ( w = 0; w < nWords; w++ )
72 {
73 Cof0 = pTruth[w] & s_Truths6Neg[iVar];
74 Cof1 = (pTruth[w] >> shift) & s_Truths6Neg[iVar];
75 if ( Cof0 != Cof1 )
76 return Cof0 < Cof1 ? -1 : 1;
77 }
78 return 0;
79 }
80 // if ( iVar > 5 )
81 {
82 word * pLimit = pTruth + nWords;
83 int i, iStep = Abc_TtWordNum(iVar);
84 assert( nWords >= 2 );
85 for ( ; pTruth < pLimit; pTruth += 2*iStep )
86 for ( i = 0; i < iStep; i++ )
87 if ( pTruth[i] != pTruth[i + iStep] )
88 return pTruth[i] < pTruth[i + iStep] ? -1 : 1;
89 return 0;
90 }
91 }
92 static inline int Abc_TtCompare1VarCofsRev( word * pTruth, int nWords, int iVar )
93 {
94 if ( nWords == 1 )
95 {
96 word Cof0 = pTruth[0] & s_Truths6Neg[iVar];
97 word Cof1 = (pTruth[0] >> (1 << iVar)) & s_Truths6Neg[iVar];
98 if ( Cof0 != Cof1 )
99 return Cof0 < Cof1 ? -1 : 1;
100 return 0;
101 }
102 if ( iVar <= 5 )
103 {
104 word Cof0, Cof1;
105 int w, shift = (1 << iVar);
106 for ( w = nWords - 1; w >= 0; w-- )
107 {
108 Cof0 = pTruth[w] & s_Truths6Neg[iVar];
109 Cof1 = (pTruth[w] >> shift) & s_Truths6Neg[iVar];
110 if ( Cof0 != Cof1 )
111 return Cof0 < Cof1 ? -1 : 1;
112 }
113 return 0;
114 }
115 // if ( iVar > 5 )
116 {
117 word * pLimit = pTruth + nWords;
118 int i, iStep = Abc_TtWordNum(iVar);
119 assert( nWords >= 2 );
120 for ( pLimit -= 2*iStep; pLimit >= pTruth; pLimit -= 2*iStep )
121 for ( i = iStep - 1; i >= 0; i-- )
122 if ( pLimit[i] != pLimit[i + iStep] )
123 return pLimit[i] < pLimit[i + iStep] ? -1 : 1;
124 return 0;
125 }
126 }
127 */
128
129 /**Function*************************************************************
130
131 Synopsis [Checks equality of pairs of cofactors w.r.t. adjacent variables.]
132
133 Description []
134
135 SideEffects []
136
137 SeeAlso []
138
139 ***********************************************************************/
Abc_TtCheckEqual2VarCofs(word * pTruth,int nWords,int iVar,int Num1,int Num2)140 static inline int Abc_TtCheckEqual2VarCofs( word * pTruth, int nWords, int iVar, int Num1, int Num2 )
141 {
142 assert( Num1 < Num2 && Num2 < 4 );
143 if ( nWords == 1 )
144 return ((pTruth[0] >> (Num2 * (1 << iVar))) & s_CMasks6[iVar]) == ((pTruth[0] >> (Num1 * (1 << iVar))) & s_CMasks6[iVar]);
145 if ( iVar <= 4 )
146 {
147 int w, shift = (1 << iVar);
148 for ( w = 0; w < nWords; w++ )
149 if ( ((pTruth[w] >> Num2 * shift) & s_CMasks6[iVar]) != ((pTruth[w] >> Num1 * shift) & s_CMasks6[iVar]) )
150 return 0;
151 return 1;
152 }
153 if ( iVar == 5 )
154 {
155 unsigned * pTruthU = (unsigned *)pTruth;
156 unsigned * pLimitU = (unsigned *)(pTruth + nWords);
157 assert( nWords >= 2 );
158 for ( ; pTruthU < pLimitU; pTruthU += 4 )
159 if ( pTruthU[Num2] != pTruthU[Num1] )
160 return 0;
161 return 1;
162 }
163 // if ( iVar > 5 )
164 {
165 word * pLimit = pTruth + nWords;
166 int i, iStep = Abc_TtWordNum(iVar);
167 assert( nWords >= 4 );
168 for ( ; pTruth < pLimit; pTruth += 4*iStep )
169 for ( i = 0; i < iStep; i++ )
170 if ( pTruth[i+Num2*iStep] != pTruth[i+Num1*iStep] )
171 return 0;
172 return 1;
173 }
174 }
175
176 /**Function*************************************************************
177
178 Synopsis [Compares pairs of cofactors w.r.t. adjacent variables.]
179
180 Description []
181
182 SideEffects []
183
184 SeeAlso []
185
186 ***********************************************************************/
Abc_TtCompare2VarCofs(word * pTruth,int nWords,int iVar,int Num1,int Num2)187 static inline int Abc_TtCompare2VarCofs( word * pTruth, int nWords, int iVar, int Num1, int Num2 )
188 {
189 assert( Num1 < Num2 && Num2 < 4 );
190 if ( nWords == 1 )
191 {
192 word Cof1 = (pTruth[0] >> (Num1 * (1 << iVar))) & s_CMasks6[iVar];
193 word Cof2 = (pTruth[0] >> (Num2 * (1 << iVar))) & s_CMasks6[iVar];
194 if ( Cof1 != Cof2 )
195 return Cof1 < Cof2 ? -1 : 1;
196 return 0;
197 }
198 if ( iVar <= 4 )
199 {
200 word Cof1, Cof2;
201 int w, shift = (1 << iVar);
202 for ( w = 0; w < nWords; w++ )
203 {
204 Cof1 = (pTruth[w] >> Num1 * shift) & s_CMasks6[iVar];
205 Cof2 = (pTruth[w] >> Num2 * shift) & s_CMasks6[iVar];
206 if ( Cof1 != Cof2 )
207 return Cof1 < Cof2 ? -1 : 1;
208 }
209 return 0;
210 }
211 if ( iVar == 5 )
212 {
213 unsigned * pTruthU = (unsigned *)pTruth;
214 unsigned * pLimitU = (unsigned *)(pTruth + nWords);
215 assert( nWords >= 2 );
216 for ( ; pTruthU < pLimitU; pTruthU += 4 )
217 if ( pTruthU[Num1] != pTruthU[Num2] )
218 return pTruthU[Num1] < pTruthU[Num2] ? -1 : 1;
219 return 0;
220 }
221 // if ( iVar > 5 )
222 {
223 word * pLimit = pTruth + nWords;
224 int i, iStep = Abc_TtWordNum(iVar);
225 int Offset1 = Num1*iStep;
226 int Offset2 = Num2*iStep;
227 assert( nWords >= 4 );
228 for ( ; pTruth < pLimit; pTruth += 4*iStep )
229 for ( i = 0; i < iStep; i++ )
230 if ( pTruth[i + Offset1] != pTruth[i + Offset2] )
231 return pTruth[i + Offset1] < pTruth[i + Offset2] ? -1 : 1;
232 return 0;
233 }
234 }
Abc_TtCompare2VarCofsRev(word * pTruth,int nWords,int iVar,int Num1,int Num2)235 static inline int Abc_TtCompare2VarCofsRev( word * pTruth, int nWords, int iVar, int Num1, int Num2 )
236 {
237 assert( Num1 < Num2 && Num2 < 4 );
238 if ( nWords == 1 )
239 {
240 word Cof1 = (pTruth[0] >> (Num1 * (1 << iVar))) & s_CMasks6[iVar];
241 word Cof2 = (pTruth[0] >> (Num2 * (1 << iVar))) & s_CMasks6[iVar];
242 if ( Cof1 != Cof2 )
243 return Cof1 < Cof2 ? -1 : 1;
244 return 0;
245 }
246 if ( iVar <= 4 )
247 {
248 word Cof1, Cof2;
249 int w, shift = (1 << iVar);
250 for ( w = nWords - 1; w >= 0; w-- )
251 {
252 Cof1 = (pTruth[w] >> Num1 * shift) & s_CMasks6[iVar];
253 Cof2 = (pTruth[w] >> Num2 * shift) & s_CMasks6[iVar];
254 if ( Cof1 != Cof2 )
255 return Cof1 < Cof2 ? -1 : 1;
256 }
257 return 0;
258 }
259 if ( iVar == 5 )
260 {
261 unsigned * pTruthU = (unsigned *)pTruth;
262 unsigned * pLimitU = (unsigned *)(pTruth + nWords);
263 assert( nWords >= 2 );
264 for ( pLimitU -= 4; pLimitU >= pTruthU; pLimitU -= 4 )
265 if ( pLimitU[Num1] != pLimitU[Num2] )
266 return pLimitU[Num1] < pLimitU[Num2] ? -1 : 1;
267 return 0;
268 }
269 // if ( iVar > 5 )
270 {
271 word * pLimit = pTruth + nWords;
272 int i, iStep = Abc_TtWordNum(iVar);
273 int Offset1 = Num1*iStep;
274 int Offset2 = Num2*iStep;
275 assert( nWords >= 4 );
276 for ( pLimit -= 4*iStep; pLimit >= pTruth; pLimit -= 4*iStep )
277 for ( i = iStep - 1; i >= 0; i-- )
278 if ( pLimit[i + Offset1] != pLimit[i + Offset2] )
279 return pLimit[i + Offset1] < pLimit[i + Offset2] ? -1 : 1;
280 return 0;
281 }
282 }
283
284 /**Function*************************************************************
285
286 Synopsis [Minterm counting in all cofactors.]
287
288 Description []
289
290 SideEffects []
291
292 SeeAlso []
293
294 ***********************************************************************/
Abc_TtNormalizeSmallTruth(word * pTruth,int nVars)295 void Abc_TtNormalizeSmallTruth(word * pTruth, int nVars)
296 {
297 if (nVars < 6) {
298 int shift, bits = (1 << nVars);
299 word base = *pTruth = *pTruth & ((((word)1) << bits) - 1);
300 for (shift = bits; shift < 64; shift += bits)
301 *pTruth |= base << shift;
302 }
303 }
304
Abc_TtVerifySmallTruth(word * pTruth,int nVars)305 static inline void Abc_TtVerifySmallTruth(word * pTruth, int nVars)
306 {
307 #ifndef NDEBUG
308 if (nVars < 6) {
309 word nTruth = *pTruth;
310 Abc_TtNormalizeSmallTruth(&nTruth, nVars);
311 assert(*pTruth == nTruth);
312 }
313 #endif
314 }
315
Abc_TtCountOnesInTruth(word * pTruth,int nVars)316 static inline int Abc_TtCountOnesInTruth( word * pTruth, int nVars )
317 {
318 int nWords = Abc_TtWordNum( nVars );
319 int k, Counter = 0;
320 Abc_TtVerifySmallTruth(pTruth, nVars);
321 for ( k = 0; k < nWords; k++ )
322 if ( pTruth[k] )
323 Counter += Abc_TtCountOnes( pTruth[k] );
324 return Counter;
325 }
Abc_TtCountOnesInCofs(word * pTruth,int nVars,int * pStore)326 static inline void Abc_TtCountOnesInCofs( word * pTruth, int nVars, int * pStore )
327 {
328 word Temp;
329 int i, k, Counter, nWords;
330 if ( nVars <= 6 )
331 {
332 Abc_TtVerifySmallTruth(pTruth, nVars);
333 for ( i = 0; i < nVars; i++ )
334 pStore[i] = Abc_TtCountOnes( pTruth[0] & s_Truths6Neg[i] );
335 return;
336 }
337 assert( nVars > 6 );
338 nWords = Abc_TtWordNum( nVars );
339 memset( pStore, 0, sizeof(int) * nVars );
340 for ( k = 0; k < nWords; k++ )
341 {
342 // count 1's for the first six variables
343 for ( i = 0; i < 6; i++ )
344 if ( (Temp = (pTruth[k] & s_Truths6Neg[i]) | ((pTruth[k+1] & s_Truths6Neg[i]) << (1 << i))) )
345 pStore[i] += Abc_TtCountOnes( Temp );
346 // count 1's for all other variables
347 if ( pTruth[k] )
348 {
349 Counter = Abc_TtCountOnes( pTruth[k] );
350 for ( i = 6; i < nVars; i++ )
351 if ( (k & (1 << (i-6))) == 0 )
352 pStore[i] += Counter;
353 }
354 k++;
355 // count 1's for all other variables
356 if ( pTruth[k] )
357 {
358 Counter = Abc_TtCountOnes( pTruth[k] );
359 for ( i = 6; i < nVars; i++ )
360 if ( (k & (1 << (i-6))) == 0 )
361 pStore[i] += Counter;
362 }
363 }
364 }
Abc_TtCountOnesInCofsSimple(word * pTruth,int nVars,int * pStore)365 int Abc_TtCountOnesInCofsSimple( word * pTruth, int nVars, int * pStore )
366 {
367 Abc_TtCountOnesInCofs( pTruth, nVars, pStore );
368 return Abc_TtCountOnesInTruth( pTruth, nVars );
369 }
370
371 // Shifted Cofactor Coefficient
shiftFunc(int ci)372 static inline int shiftFunc(int ci)
373 //{ return ci * ci; }
374 { return 1 << ci; }
375
Abc_TtScc6(word wTruth,int ck)376 static int Abc_TtScc6(word wTruth, int ck)
377 {
378 int i;
379 int sum = 0;
380 if (!wTruth) return 0;
381 for (i = 0; i < 64; i++)
382 if (wTruth & (word)1 << i) {
383 int ci = Abc_TtBitCount8[i] + ck;
384 sum += shiftFunc(ci);
385 }
386 return sum;
387 }
Abc_TtScc(word * pTruth,int nVars)388 int Abc_TtScc(word * pTruth, int nVars)
389 {
390 int k, nWords = Abc_TtWordNum(nVars);
391 int sum = 0;
392 Abc_TtNormalizeSmallTruth(pTruth, nVars);
393 for (k = 0; k < nWords; k++)
394 sum += Abc_TtScc6(pTruth[k], Abc_TtBitCount16(k));
395 return sum;
396 }
Abc_TtSccInCofs6(word wTruth,int nVars,int ck,int * pStore)397 static inline void Abc_TtSccInCofs6(word wTruth, int nVars, int ck, int * pStore)
398 {
399 int i, j, v;
400 assert(nVars <= 6);
401 for (v = 0; v < nVars; v++)
402 {
403 int sum = 0;
404 for (i = j = 0; j < 64; j++)
405 if (s_Truths6Neg[v] & (word)1 << j)
406 {
407 if (wTruth & (word)1 << j)
408 {
409 int ci = Abc_TtBitCount8[i] + ck;
410 sum += shiftFunc(ci);
411 }
412 i++;
413 }
414 pStore[v] += sum;
415 }
416 }
Abc_TtSccInCofs(word * pTruth,int nVars,int * pStore)417 static inline void Abc_TtSccInCofs(word * pTruth, int nVars, int * pStore)
418 {
419 int k, v, nWords;
420 int kv[10] = { 0 };
421 memset(pStore, 0, sizeof(int) * nVars);
422 if (nVars <= 6)
423 {
424 Abc_TtNormalizeSmallTruth(pTruth, nVars);
425 Abc_TtSccInCofs6(pTruth[0], nVars, 0, pStore);
426 return;
427 }
428 assert(nVars > 6);
429 nWords = Abc_TtWordNum(nVars);
430 for (k = 0; k < nWords; k++)
431 {
432 // count 1's for the first six variables
433 Abc_TtSccInCofs6(pTruth[k], 6, Abc_TtBitCount16(k), pStore);
434
435 // count 1's for all other variables
436 for (v = 6; v < nVars; v++)
437 if ((k & (1 << (v - 6))) == 0)
438 {
439 pStore[v] += Abc_TtScc6(pTruth[k], Abc_TtBitCount16(kv[v - 6]));
440 kv[v - 6]++;
441 }
442 }
443 }
444
445 /**Function*************************************************************
446
447 Synopsis [Minterm counting in all cofactors.]
448
449 Description []
450
451 SideEffects []
452
453 SeeAlso []
454
455 ***********************************************************************/
Abc_TtCountOnesInCofsSlow(word * pTruth,int nVars,int * pStore)456 static inline void Abc_TtCountOnesInCofsSlow( word * pTruth, int nVars, int * pStore )
457 {
458 static int bit_count[256] = {
459 0,1,1,2,1,2,2,3,1,2,2,3,2,3,3,4,1,2,2,3,2,3,3,4,2,3,3,4,3,4,4,5,
460 1,2,2,3,2,3,3,4,2,3,3,4,3,4,4,5,2,3,3,4,3,4,4,5,3,4,4,5,4,5,5,6,
461 1,2,2,3,2,3,3,4,2,3,3,4,3,4,4,5,2,3,3,4,3,4,4,5,3,4,4,5,4,5,5,6,
462 2,3,3,4,3,4,4,5,3,4,4,5,4,5,5,6,3,4,4,5,4,5,5,6,4,5,5,6,5,6,6,7,
463 1,2,2,3,2,3,3,4,2,3,3,4,3,4,4,5,2,3,3,4,3,4,4,5,3,4,4,5,4,5,5,6,
464 2,3,3,4,3,4,4,5,3,4,4,5,4,5,5,6,3,4,4,5,4,5,5,6,4,5,5,6,5,6,6,7,
465 2,3,3,4,3,4,4,5,3,4,4,5,4,5,5,6,3,4,4,5,4,5,5,6,4,5,5,6,5,6,6,7,
466 3,4,4,5,4,5,5,6,4,5,5,6,5,6,6,7,4,5,5,6,5,6,6,7,5,6,6,7,6,7,7,8
467 };
468 int i, k, nBytes;
469 unsigned char * pTruthC = (unsigned char *)pTruth;
470 nBytes = 8 * Abc_TtWordNum( nVars );
471 memset( pStore, 0, sizeof(int) * nVars );
472 for ( k = 0; k < nBytes; k++ )
473 {
474 pStore[0] += bit_count[ pTruthC[k] & 0x55 ];
475 pStore[1] += bit_count[ pTruthC[k] & 0x33 ];
476 pStore[2] += bit_count[ pTruthC[k] & 0x0F ];
477 for ( i = 3; i < nVars; i++ )
478 if ( (k & (1 << (i-3))) == 0 )
479 pStore[i] += bit_count[pTruthC[k]];
480 }
481 }
482
483 /**Function*************************************************************
484
485 Synopsis [Minterm counting in all cofactors.]
486
487 Description []
488
489 SideEffects []
490
491 SeeAlso []
492
493 ***********************************************************************/
Abc_TtCountOnesInCofsFast6_rec(word Truth,int iVar,int nBytes,int * pStore)494 int Abc_TtCountOnesInCofsFast6_rec( word Truth, int iVar, int nBytes, int * pStore )
495 {
496 static int bit_count[256] = {
497 0,1,1,2,1,2,2,3,1,2,2,3,2,3,3,4,1,2,2,3,2,3,3,4,2,3,3,4,3,4,4,5,
498 1,2,2,3,2,3,3,4,2,3,3,4,3,4,4,5,2,3,3,4,3,4,4,5,3,4,4,5,4,5,5,6,
499 1,2,2,3,2,3,3,4,2,3,3,4,3,4,4,5,2,3,3,4,3,4,4,5,3,4,4,5,4,5,5,6,
500 2,3,3,4,3,4,4,5,3,4,4,5,4,5,5,6,3,4,4,5,4,5,5,6,4,5,5,6,5,6,6,7,
501 1,2,2,3,2,3,3,4,2,3,3,4,3,4,4,5,2,3,3,4,3,4,4,5,3,4,4,5,4,5,5,6,
502 2,3,3,4,3,4,4,5,3,4,4,5,4,5,5,6,3,4,4,5,4,5,5,6,4,5,5,6,5,6,6,7,
503 2,3,3,4,3,4,4,5,3,4,4,5,4,5,5,6,3,4,4,5,4,5,5,6,4,5,5,6,5,6,6,7,
504 3,4,4,5,4,5,5,6,4,5,5,6,5,6,6,7,4,5,5,6,5,6,6,7,5,6,6,7,6,7,7,8
505 };
506 int nMints0, nMints1;
507 if ( Truth == 0 )
508 return 0;
509 if ( ~Truth == 0 )
510 {
511 int i;
512 for ( i = 0; i <= iVar; i++ )
513 pStore[i] += nBytes * 4;
514 return nBytes * 8;
515 }
516 if ( nBytes == 1 )
517 {
518 assert( iVar == 2 );
519 pStore[0] += bit_count[ Truth & 0x55 ];
520 pStore[1] += bit_count[ Truth & 0x33 ];
521 pStore[2] += bit_count[ Truth & 0x0F ];
522 return bit_count[ Truth & 0xFF ];
523 }
524 nMints0 = Abc_TtCountOnesInCofsFast6_rec( Abc_Tt6Cofactor0(Truth, iVar), iVar - 1, nBytes/2, pStore );
525 nMints1 = Abc_TtCountOnesInCofsFast6_rec( Abc_Tt6Cofactor1(Truth, iVar), iVar - 1, nBytes/2, pStore );
526 pStore[iVar] += nMints0;
527 return nMints0 + nMints1;
528 }
529
Abc_TtCountOnesInCofsFast_rec(word * pTruth,int iVar,int nWords,int * pStore)530 int Abc_TtCountOnesInCofsFast_rec( word * pTruth, int iVar, int nWords, int * pStore )
531 {
532 int nMints0, nMints1;
533 if ( nWords == 1 )
534 {
535 assert( iVar == 5 );
536 return Abc_TtCountOnesInCofsFast6_rec( pTruth[0], iVar, 8, pStore );
537 }
538 assert( nWords > 1 );
539 assert( iVar > 5 );
540 if ( pTruth[0] & 1 )
541 {
542 if ( Abc_TtIsConst1( pTruth, nWords ) )
543 {
544 int i;
545 for ( i = 0; i <= iVar; i++ )
546 pStore[i] += nWords * 32;
547 return nWords * 64;
548 }
549 }
550 else
551 {
552 if ( Abc_TtIsConst0( pTruth, nWords ) )
553 return 0;
554 }
555 nMints0 = Abc_TtCountOnesInCofsFast_rec( pTruth, iVar - 1, nWords/2, pStore );
556 nMints1 = Abc_TtCountOnesInCofsFast_rec( pTruth + nWords/2, iVar - 1, nWords/2, pStore );
557 pStore[iVar] += nMints0;
558 return nMints0 + nMints1;
559 }
Abc_TtCountOnesInCofsFast(word * pTruth,int nVars,int * pStore)560 int Abc_TtCountOnesInCofsFast( word * pTruth, int nVars, int * pStore )
561 {
562 memset( pStore, 0, sizeof(int) * nVars );
563 assert( nVars >= 3 );
564 if ( nVars <= 6 )
565 return Abc_TtCountOnesInCofsFast6_rec( pTruth[0], nVars - 1, Abc_TtByteNum( nVars ), pStore );
566 else
567 return Abc_TtCountOnesInCofsFast_rec( pTruth, nVars - 1, Abc_TtWordNum( nVars ), pStore );
568 }
569
570
571 /**Function*************************************************************
572
573 Synopsis []
574
575 Description []
576
577 SideEffects []
578
579 SeeAlso []
580
581 ***********************************************************************/
Abc_TtSemiCanonicize(word * pTruth,int nVars,char * pCanonPerm,int * pStoreOut,int fOnlySwap)582 static inline unsigned Abc_TtSemiCanonicize( word * pTruth, int nVars, char * pCanonPerm, int * pStoreOut, int fOnlySwap )
583 {
584 int fUseOld = 1;
585 int fOldSwap = 0;
586 int pStoreIn[17];
587 int * pStore = pStoreOut ? pStoreOut : pStoreIn;
588 int i, nOnes, nWords = Abc_TtWordNum( nVars );
589 unsigned uCanonPhase = 0;
590 assert( nVars <= 16 );
591 for ( i = 0; i < nVars; i++ )
592 pCanonPerm[i] = i;
593
594 if ( fUseOld )
595 {
596 // normalize polarity
597 nOnes = Abc_TtCountOnesInTruth( pTruth, nVars );
598 if ( nOnes > nWords * 32 && !fOnlySwap )
599 {
600 Abc_TtNot( pTruth, nWords );
601 nOnes = nWords*64 - nOnes;
602 uCanonPhase |= (1 << nVars);
603 }
604 // normalize phase
605 Abc_TtCountOnesInCofs( pTruth, nVars, pStore );
606 pStore[nVars] = nOnes;
607 for ( i = 0; i < nVars; i++ )
608 {
609 if ( pStore[i] >= nOnes - pStore[i] || fOnlySwap )
610 continue;
611 Abc_TtFlip( pTruth, nWords, i );
612 uCanonPhase |= (1 << i);
613 pStore[i] = nOnes - pStore[i];
614 }
615 }
616 else
617 {
618 nOnes = Abc_TtCountOnesInCofsQuick( pTruth, nVars, pStore );
619 // normalize polarity
620 if ( nOnes > nWords * 32 && !fOnlySwap )
621 {
622 for ( i = 0; i < nVars; i++ )
623 pStore[i] = nWords * 32 - pStore[i];
624 Abc_TtNot( pTruth, nWords );
625 nOnes = nWords*64 - nOnes;
626 uCanonPhase |= (1 << nVars);
627 }
628 // normalize phase
629 pStore[nVars] = nOnes;
630 for ( i = 0; i < nVars; i++ )
631 {
632 if ( pStore[i] >= nOnes - pStore[i] || fOnlySwap )
633 continue;
634 Abc_TtFlip( pTruth, nWords, i );
635 uCanonPhase |= (1 << i);
636 pStore[i] = nOnes - pStore[i];
637 }
638 }
639
640 // normalize permutation
641 if ( fOldSwap )
642 {
643 int fChange;
644 do {
645 fChange = 0;
646 for ( i = 0; i < nVars-1; i++ )
647 {
648 if ( pStore[i] <= pStore[i+1] )
649 // if ( pStore[i] >= pStore[i+1] )
650 continue;
651 ABC_SWAP( int, pCanonPerm[i], pCanonPerm[i+1] );
652 ABC_SWAP( int, pStore[i], pStore[i+1] );
653 if ( ((uCanonPhase >> i) & 1) != ((uCanonPhase >> (i+1)) & 1) )
654 {
655 uCanonPhase ^= (1 << i);
656 uCanonPhase ^= (1 << (i+1));
657 }
658 Abc_TtSwapAdjacent( pTruth, nWords, i );
659 fChange = 1;
660 // nSwaps++;
661 }
662 }
663 while ( fChange );
664 }
665 else
666 {
667 int k, BestK;
668 for ( i = 0; i < nVars - 1; i++ )
669 {
670 BestK = i + 1;
671 for ( k = i + 2; k < nVars; k++ )
672 if ( pStore[BestK] > pStore[k] )
673 // if ( pStore[BestK] < pStore[k] )
674 BestK = k;
675 if ( pStore[i] <= pStore[BestK] )
676 // if ( pStore[i] >= pStore[BestK] )
677 continue;
678 ABC_SWAP( int, pCanonPerm[i], pCanonPerm[BestK] );
679 ABC_SWAP( int, pStore[i], pStore[BestK] );
680 if ( ((uCanonPhase >> i) & 1) != ((uCanonPhase >> BestK) & 1) )
681 {
682 uCanonPhase ^= (1 << i);
683 uCanonPhase ^= (1 << BestK);
684 }
685 Abc_TtSwapVars( pTruth, nVars, i, BestK );
686 // nSwaps++;
687 }
688 }
689 return uCanonPhase;
690 }
691
692
693
694 /**Function*************************************************************
695
696 Synopsis []
697
698 Description []
699
700 SideEffects []
701
702 SeeAlso []
703
704 ***********************************************************************/
Abc_TtCofactorTest10(word * pTruth,int nVars,int N)705 void Abc_TtCofactorTest10( word * pTruth, int nVars, int N )
706 {
707 static word pCopy1[1024];
708 static word pCopy2[1024];
709 int nWords = Abc_TtWordNum( nVars );
710 int i;
711 for ( i = 0; i < nVars - 1; i++ )
712 {
713 // Kit_DsdPrintFromTruth( pTruth, nVars ); printf( "\n" );
714 Abc_TtCopy( pCopy1, pTruth, nWords, 0 );
715 Abc_TtSwapAdjacent( pCopy1, nWords, i );
716 // Kit_DsdPrintFromTruth( pCopy1, nVars ); printf( "\n" );
717 Abc_TtCopy( pCopy2, pTruth, nWords, 0 );
718 Abc_TtSwapVars( pCopy2, nVars, i, i+1 );
719 // Kit_DsdPrintFromTruth( pCopy2, nVars ); printf( "\n" );
720 assert( Abc_TtEqual( pCopy1, pCopy2, nWords ) );
721 }
722 }
723
724 /**Function*************************************************************
725
726 Synopsis [Naive evaluation.]
727
728 Description []
729
730 SideEffects []
731
732 SeeAlso []
733
734 ***********************************************************************/
Abc_Tt6CofactorPermNaive(word * pTruth,int i,int fSwapOnly)735 int Abc_Tt6CofactorPermNaive( word * pTruth, int i, int fSwapOnly )
736 {
737 if ( fSwapOnly )
738 {
739 word Copy = Abc_Tt6SwapAdjacent( pTruth[0], i );
740 if ( pTruth[0] > Copy )
741 {
742 pTruth[0] = Copy;
743 return 4;
744 }
745 return 0;
746 }
747 {
748 word Copy = pTruth[0];
749 word Best = pTruth[0];
750 int Config = 0;
751 // PXY
752 // 001
753 Copy = Abc_Tt6Flip( Copy, i );
754 if ( Best > Copy )
755 Best = Copy, Config = 1;
756 // PXY
757 // 011
758 Copy = Abc_Tt6Flip( Copy, i+1 );
759 if ( Best > Copy )
760 Best = Copy, Config = 3;
761 // PXY
762 // 010
763 Copy = Abc_Tt6Flip( Copy, i );
764 if ( Best > Copy )
765 Best = Copy, Config = 2;
766 // PXY
767 // 110
768 Copy = Abc_Tt6SwapAdjacent( Copy, i );
769 if ( Best > Copy )
770 Best = Copy, Config = 6;
771 // PXY
772 // 111
773 Copy = Abc_Tt6Flip( Copy, i+1 );
774 if ( Best > Copy )
775 Best = Copy, Config = 7;
776 // PXY
777 // 101
778 Copy = Abc_Tt6Flip( Copy, i );
779 if ( Best > Copy )
780 Best = Copy, Config = 5;
781 // PXY
782 // 100
783 Copy = Abc_Tt6Flip( Copy, i+1 );
784 if ( Best > Copy )
785 Best = Copy, Config = 4;
786 // PXY
787 // 000
788 Copy = Abc_Tt6SwapAdjacent( Copy, i );
789 assert( Copy == pTruth[0] );
790 assert( Best <= pTruth[0] );
791 pTruth[0] = Best;
792 return Config;
793 }
794 }
Abc_TtCofactorPermNaive(word * pTruth,int i,int nWords,int fSwapOnly)795 int Abc_TtCofactorPermNaive( word * pTruth, int i, int nWords, int fSwapOnly )
796 {
797 if ( fSwapOnly )
798 {
799 static word pCopy[1024];
800 Abc_TtCopy( pCopy, pTruth, nWords, 0 );
801 Abc_TtSwapAdjacent( pCopy, nWords, i );
802 if ( Abc_TtCompareRev(pTruth, pCopy, nWords) == 1 )
803 {
804 Abc_TtCopy( pTruth, pCopy, nWords, 0 );
805 return 4;
806 }
807 return 0;
808 }
809 {
810 static word pCopy[1024];
811 static word pBest[1024];
812 int Config = 0;
813 // save two copies
814 Abc_TtCopy( pCopy, pTruth, nWords, 0 );
815 Abc_TtCopy( pBest, pTruth, nWords, 0 );
816 // PXY
817 // 001
818 Abc_TtFlip( pCopy, nWords, i );
819 if ( Abc_TtCompareRev(pBest, pCopy, nWords) == 1 )
820 Abc_TtCopy( pBest, pCopy, nWords, 0 ), Config = 1;
821 // PXY
822 // 011
823 Abc_TtFlip( pCopy, nWords, i+1 );
824 if ( Abc_TtCompareRev(pBest, pCopy, nWords) == 1 )
825 Abc_TtCopy( pBest, pCopy, nWords, 0 ), Config = 3;
826 // PXY
827 // 010
828 Abc_TtFlip( pCopy, nWords, i );
829 if ( Abc_TtCompareRev(pBest, pCopy, nWords) == 1 )
830 Abc_TtCopy( pBest, pCopy, nWords, 0 ), Config = 2;
831 // PXY
832 // 110
833 Abc_TtSwapAdjacent( pCopy, nWords, i );
834 if ( Abc_TtCompareRev(pBest, pCopy, nWords) == 1 )
835 Abc_TtCopy( pBest, pCopy, nWords, 0 ), Config = 6;
836 // PXY
837 // 111
838 Abc_TtFlip( pCopy, nWords, i+1 );
839 if ( Abc_TtCompareRev(pBest, pCopy, nWords) == 1 )
840 Abc_TtCopy( pBest, pCopy, nWords, 0 ), Config = 7;
841 // PXY
842 // 101
843 Abc_TtFlip( pCopy, nWords, i );
844 if ( Abc_TtCompareRev(pBest, pCopy, nWords) == 1 )
845 Abc_TtCopy( pBest, pCopy, nWords, 0 ), Config = 5;
846 // PXY
847 // 100
848 Abc_TtFlip( pCopy, nWords, i+1 );
849 if ( Abc_TtCompareRev(pBest, pCopy, nWords) == 1 )
850 Abc_TtCopy( pBest, pCopy, nWords, 0 ), Config = 4;
851 // PXY
852 // 000
853 Abc_TtSwapAdjacent( pCopy, nWords, i );
854 assert( Abc_TtEqual( pTruth, pCopy, nWords ) );
855 if ( Config == 0 )
856 return 0;
857 assert( Abc_TtCompareRev(pTruth, pBest, nWords) == 1 );
858 Abc_TtCopy( pTruth, pBest, nWords, 0 );
859 return Config;
860 }
861 }
862
863
864 /**Function*************************************************************
865
866 Synopsis [Smart evaluation.]
867
868 Description []
869
870 SideEffects []
871
872 SeeAlso []
873
874 ***********************************************************************/
Abc_TtCofactorPermConfig(word * pTruth,int i,int nWords,int fSwapOnly,int fNaive)875 int Abc_TtCofactorPermConfig( word * pTruth, int i, int nWords, int fSwapOnly, int fNaive )
876 {
877 if ( nWords == 1 )
878 return Abc_Tt6CofactorPermNaive( pTruth, i, fSwapOnly );
879 if ( fNaive )
880 return Abc_TtCofactorPermNaive( pTruth, i, nWords, fSwapOnly );
881 if ( fSwapOnly )
882 {
883 if ( Abc_TtCompare2VarCofsRev( pTruth, nWords, i, 1, 2 ) < 0 ) // Cof1 < Cof2
884 {
885 Abc_TtSwapAdjacent( pTruth, nWords, i );
886 return 4;
887 }
888 return 0;
889 }
890 {
891 int fComp01, fComp02, fComp03, fComp12, fComp13, fComp23, Config = 0;
892 fComp01 = Abc_TtCompare2VarCofsRev( pTruth, nWords, i, 0, 1 );
893 fComp23 = Abc_TtCompare2VarCofsRev( pTruth, nWords, i, 2, 3 );
894 if ( fComp23 >= 0 ) // Cof2 >= Cof3
895 {
896 if ( fComp01 >= 0 ) // Cof0 >= Cof1
897 {
898 fComp13 = Abc_TtCompare2VarCofsRev( pTruth, nWords, i, 1, 3 );
899 if ( fComp13 < 0 ) // Cof1 < Cof3
900 Abc_TtFlip( pTruth, nWords, i + 1 ), Config = 2;
901 else if ( fComp13 == 0 ) // Cof1 == Cof3
902 {
903 fComp02 = Abc_TtCompare2VarCofsRev( pTruth, nWords, i, 0, 2 );
904 if ( fComp02 < 0 )
905 Abc_TtFlip( pTruth, nWords, i + 1 ), Config = 2;
906 }
907 // else Cof1 > Cof3 -- do nothing
908 }
909 else // Cof0 < Cof1
910 {
911 fComp03 = Abc_TtCompare2VarCofsRev( pTruth, nWords, i, 0, 3 );
912 if ( fComp03 < 0 ) // Cof0 < Cof3
913 {
914 Abc_TtFlip( pTruth, nWords, i );
915 Abc_TtFlip( pTruth, nWords, i + 1 ), Config = 3;
916 }
917 else // Cof0 >= Cof3
918 {
919 if ( fComp23 == 0 ) // can flip Cof0 and Cof1
920 Abc_TtFlip( pTruth, nWords, i ), Config = 1;
921 }
922 }
923 }
924 else // Cof2 < Cof3
925 {
926 if ( fComp01 >= 0 ) // Cof0 >= Cof1
927 {
928 fComp12 = Abc_TtCompare2VarCofsRev( pTruth, nWords, i, 1, 2 );
929 if ( fComp12 > 0 ) // Cof1 > Cof2
930 Abc_TtFlip( pTruth, nWords, i ), Config = 1;
931 else if ( fComp12 == 0 ) // Cof1 == Cof2
932 {
933 Abc_TtFlip( pTruth, nWords, i );
934 Abc_TtFlip( pTruth, nWords, i + 1 ), Config = 3;
935 }
936 else // Cof1 < Cof2
937 {
938 Abc_TtFlip( pTruth, nWords, i + 1 ), Config = 2;
939 if ( fComp01 == 0 )
940 Abc_TtFlip( pTruth, nWords, i ), Config ^= 1;
941 }
942 }
943 else // Cof0 < Cof1
944 {
945 fComp02 = Abc_TtCompare2VarCofsRev( pTruth, nWords, i, 0, 2 );
946 if ( fComp02 == -1 ) // Cof0 < Cof2
947 {
948 Abc_TtFlip( pTruth, nWords, i );
949 Abc_TtFlip( pTruth, nWords, i + 1 ), Config = 3;
950 }
951 else if ( fComp02 == 0 ) // Cof0 == Cof2
952 {
953 fComp13 = Abc_TtCompare2VarCofsRev( pTruth, nWords, i, 1, 3 );
954 if ( fComp13 >= 0 ) // Cof1 >= Cof3
955 Abc_TtFlip( pTruth, nWords, i ), Config = 1;
956 else // Cof1 < Cof3
957 {
958 Abc_TtFlip( pTruth, nWords, i );
959 Abc_TtFlip( pTruth, nWords, i + 1 ), Config = 3;
960 }
961 }
962 else // Cof0 > Cof2
963 Abc_TtFlip( pTruth, nWords, i ), Config = 1;
964 }
965 }
966 // perform final swap if needed
967 fComp12 = Abc_TtCompare2VarCofsRev( pTruth, nWords, i, 1, 2 );
968 if ( fComp12 < 0 ) // Cof1 < Cof2
969 Abc_TtSwapAdjacent( pTruth, nWords, i ), Config ^= 4;
970 return Config;
971 }
972 }
Abc_TtCofactorPerm(word * pTruth,int i,int nWords,int fSwapOnly,char * pCanonPerm,unsigned * puCanonPhase,int fNaive)973 int Abc_TtCofactorPerm( word * pTruth, int i, int nWords, int fSwapOnly, char * pCanonPerm, unsigned * puCanonPhase, int fNaive )
974 {
975 if ( fSwapOnly )
976 {
977 int Config = Abc_TtCofactorPermConfig( pTruth, i, nWords, 1, 0 );
978 if ( Config )
979 {
980 if ( ((*puCanonPhase >> i) & 1) != ((*puCanonPhase >> (i+1)) & 1) )
981 {
982 *puCanonPhase ^= (1 << i);
983 *puCanonPhase ^= (1 << (i+1));
984 }
985 ABC_SWAP( int, pCanonPerm[i], pCanonPerm[i+1] );
986 }
987 return Config;
988 }
989 {
990 static word pCopy1[1024];
991 int Config;
992 Abc_TtCopy( pCopy1, pTruth, nWords, 0 );
993 Config = Abc_TtCofactorPermConfig( pTruth, i, nWords, 0, fNaive );
994 if ( Config == 0 )
995 return 0;
996 if ( Abc_TtCompareRev(pTruth, pCopy1, nWords) == 1 ) // made it worse
997 {
998 Abc_TtCopy( pTruth, pCopy1, nWords, 0 );
999 return 0;
1000 }
1001 // improved
1002 if ( Config & 1 )
1003 *puCanonPhase ^= (1 << i);
1004 if ( Config & 2 )
1005 *puCanonPhase ^= (1 << (i+1));
1006 if ( Config & 4 )
1007 {
1008 if ( ((*puCanonPhase >> i) & 1) != ((*puCanonPhase >> (i+1)) & 1) )
1009 {
1010 *puCanonPhase ^= (1 << i);
1011 *puCanonPhase ^= (1 << (i+1));
1012 }
1013 ABC_SWAP( int, pCanonPerm[i], pCanonPerm[i+1] );
1014 }
1015 return Config;
1016 }
1017 }
1018
1019 /**Function*************************************************************
1020
1021 Synopsis [Semi-canonical form computation.]
1022
1023 Description []
1024
1025 SideEffects []
1026
1027 SeeAlso []
1028
1029 ***********************************************************************/
1030 #define CANON_VERIFY
Abc_TtCanonicize(word * pTruth,int nVars,char * pCanonPerm)1031 unsigned Abc_TtCanonicize( word * pTruth, int nVars, char * pCanonPerm )
1032 {
1033 int pStoreIn[17];
1034 unsigned uCanonPhase;
1035 int i, k, nWords = Abc_TtWordNum( nVars );
1036 int fNaive = 1;
1037
1038 #ifdef CANON_VERIFY
1039 char pCanonPermCopy[16];
1040 static word pCopy1[1024];
1041 static word pCopy2[1024];
1042 Abc_TtCopy( pCopy1, pTruth, nWords, 0 );
1043 #endif
1044
1045 uCanonPhase = Abc_TtSemiCanonicize( pTruth, nVars, pCanonPerm, pStoreIn, 0 );
1046 for ( k = 0; k < 5; k++ )
1047 {
1048 int fChanges = 0;
1049 for ( i = nVars - 2; i >= 0; i-- )
1050 if ( pStoreIn[i] == pStoreIn[i+1] )
1051 fChanges |= Abc_TtCofactorPerm( pTruth, i, nWords, pStoreIn[i] != pStoreIn[nVars]/2, pCanonPerm, &uCanonPhase, fNaive );
1052 if ( !fChanges )
1053 break;
1054 fChanges = 0;
1055 for ( i = 1; i < nVars - 1; i++ )
1056 if ( pStoreIn[i] == pStoreIn[i+1] )
1057 fChanges |= Abc_TtCofactorPerm( pTruth, i, nWords, pStoreIn[i] != pStoreIn[nVars]/2, pCanonPerm, &uCanonPhase, fNaive );
1058 if ( !fChanges )
1059 break;
1060 }
1061
1062 #ifdef CANON_VERIFY
1063 Abc_TtCopy( pCopy2, pTruth, nWords, 0 );
1064 memcpy( pCanonPermCopy, pCanonPerm, sizeof(char) * nVars );
1065 Abc_TtImplementNpnConfig( pCopy2, nVars, pCanonPermCopy, uCanonPhase );
1066 if ( !Abc_TtEqual( pCopy1, pCopy2, nWords ) )
1067 printf( "Canonical form verification failed!\n" );
1068 #endif
1069 /*
1070 if ( !Abc_TtEqual( pCopy1, pCopy2, nWords ) )
1071 {
1072 Kit_DsdPrintFromTruth( pCopy1, nVars ); printf( "\n" );
1073 Kit_DsdPrintFromTruth( pCopy2, nVars ); printf( "\n" );
1074 i = 0;
1075 }
1076 */
1077 return uCanonPhase;
1078 }
1079
Abc_TtCanonicizePerm(word * pTruth,int nVars,char * pCanonPerm)1080 unsigned Abc_TtCanonicizePerm( word * pTruth, int nVars, char * pCanonPerm )
1081 {
1082 int pStoreIn[17];
1083 unsigned uCanonPhase;
1084 int i, k, nWords = Abc_TtWordNum( nVars );
1085 int fNaive = 1;
1086
1087 #ifdef CANON_VERIFY
1088 char pCanonPermCopy[16];
1089 static word pCopy1[1024];
1090 static word pCopy2[1024];
1091 Abc_TtCopy( pCopy1, pTruth, nWords, 0 );
1092 #endif
1093
1094 assert( nVars <= 16 );
1095 for ( i = 0; i < nVars; i++ )
1096 pCanonPerm[i] = i;
1097
1098 uCanonPhase = Abc_TtSemiCanonicize( pTruth, nVars, pCanonPerm, pStoreIn, 1 );
1099 for ( k = 0; k < 5; k++ )
1100 {
1101 int fChanges = 0;
1102 for ( i = nVars - 2; i >= 0; i-- )
1103 if ( pStoreIn[i] == pStoreIn[i+1] )
1104 fChanges |= Abc_TtCofactorPerm( pTruth, i, nWords, 1, pCanonPerm, &uCanonPhase, fNaive );
1105 if ( !fChanges )
1106 break;
1107 fChanges = 0;
1108 for ( i = 1; i < nVars - 1; i++ )
1109 if ( pStoreIn[i] == pStoreIn[i+1] )
1110 fChanges |= Abc_TtCofactorPerm( pTruth, i, nWords, 1, pCanonPerm, &uCanonPhase, fNaive );
1111 if ( !fChanges )
1112 break;
1113 }
1114
1115 #ifdef CANON_VERIFY
1116 Abc_TtCopy( pCopy2, pTruth, nWords, 0 );
1117 memcpy( pCanonPermCopy, pCanonPerm, sizeof(char) * nVars );
1118 Abc_TtImplementNpnConfig( pCopy2, nVars, pCanonPermCopy, uCanonPhase );
1119 if ( !Abc_TtEqual( pCopy1, pCopy2, nWords ) )
1120 printf( "Canonical form verification failed!\n" );
1121 #endif
1122
1123 assert( uCanonPhase == 0 );
1124 return uCanonPhase;
1125 }
1126
1127 /**Function*************************************************************
1128
1129 Synopsis [Semi-canonical form computation.]
1130
1131 Description []
1132
1133 SideEffects []
1134
1135 SeeAlso []
1136
1137 ***********************************************************************/
Abc_TtCanonicizePhaseVar6(word * pTruth,int nVars,int v)1138 static inline int Abc_TtCanonicizePhaseVar6( word * pTruth, int nVars, int v )
1139 {
1140 int w, nWords = Abc_TtWordNum( nVars );
1141 int s, nStep = 1 << (v-6);
1142 assert( v >= 6 );
1143 for ( w = nWords - 1, s = nWords - nStep; w > 0; w-- )
1144 {
1145 if ( pTruth[w-nStep] == pTruth[w] )
1146 {
1147 if ( w == s ) { w = s - nStep; s = w - nStep; }
1148 continue;
1149 }
1150 if ( pTruth[w-nStep] > pTruth[w] )
1151 return -1;
1152 for ( ; w > 0; w-- )
1153 {
1154 ABC_SWAP( word, pTruth[w-nStep], pTruth[w] );
1155 if ( w == s ) { w = s - nStep; s = w - nStep; }
1156 }
1157 assert( w == -1 );
1158 return 1;
1159 }
1160 return 0;
1161 }
Abc_TtCanonicizePhaseVar5(word * pTruth,int nVars,int v)1162 static inline int Abc_TtCanonicizePhaseVar5( word * pTruth, int nVars, int v )
1163 {
1164 int w, nWords = Abc_TtWordNum( nVars );
1165 int Shift = 1 << v;
1166 word Mask = s_Truths6[v];
1167 assert( v < 6 );
1168 for ( w = nWords - 1; w >= 0; w-- )
1169 {
1170 if ( ((pTruth[w] << Shift) & Mask) == (pTruth[w] & Mask) )
1171 continue;
1172 if ( ((pTruth[w] << Shift) & Mask) > (pTruth[w] & Mask) )
1173 return -1;
1174 // Extra_PrintHex( stdout, (unsigned *)pTruth, nVars ); printf("\n" );
1175 for ( ; w >= 0; w-- )
1176 pTruth[w] = ((pTruth[w] << Shift) & Mask) | ((pTruth[w] & Mask) >> Shift);
1177 // Extra_PrintHex( stdout, (unsigned *)pTruth, nVars ); printf( " changed %d", v ), printf("\n" );
1178 return 1;
1179 }
1180 return 0;
1181 }
Abc_TtCanonicizePhase(word * pTruth,int nVars)1182 unsigned Abc_TtCanonicizePhase( word * pTruth, int nVars )
1183 {
1184 unsigned uCanonPhase = 0;
1185 int v, nWords = Abc_TtWordNum( nVars );
1186 // static int Counter = 0;
1187 // Counter++;
1188
1189 #ifdef CANON_VERIFY
1190 static word pCopy1[1024];
1191 static word pCopy2[1024];
1192 Abc_TtCopy( pCopy1, pTruth, nWords, 0 );
1193 #endif
1194
1195 if ( (pTruth[nWords-1] >> 63) & 1 )
1196 {
1197 Abc_TtNot( pTruth, nWords );
1198 uCanonPhase ^= (1 << nVars);
1199 }
1200
1201 // while ( 1 )
1202 // {
1203 // unsigned uCanonPhase2 = uCanonPhase;
1204 for ( v = nVars - 1; v >= 6; v-- )
1205 if ( Abc_TtCanonicizePhaseVar6( pTruth, nVars, v ) == 1 )
1206 uCanonPhase ^= 1 << v;
1207 for ( ; v >= 0; v-- )
1208 if ( Abc_TtCanonicizePhaseVar5( pTruth, nVars, v ) == 1 )
1209 uCanonPhase ^= 1 << v;
1210 // if ( uCanonPhase2 == uCanonPhase )
1211 // break;
1212 // }
1213
1214 // for ( v = 5; v >= 0; v-- )
1215 // assert( Abc_TtCanonicizePhaseVar5( pTruth, nVars, v ) != 1 );
1216
1217 #ifdef CANON_VERIFY
1218 Abc_TtCopy( pCopy2, pTruth, nWords, 0 );
1219 Abc_TtImplementNpnConfig( pCopy2, nVars, NULL, uCanonPhase );
1220 if ( !Abc_TtEqual( pCopy1, pCopy2, nWords ) )
1221 printf( "Canonical form verification failed!\n" );
1222 #endif
1223 return uCanonPhase;
1224 }
1225
1226
1227 /**Function*************************************************************
1228
1229 Synopsis [Hierarchical semi-canonical form computation.]
1230
1231 Description []
1232
1233 SideEffects []
1234
1235 SeeAlso []
1236
1237 ***********************************************************************/
1238 #define TT_MAX_LEVELS 5
1239
1240 struct Abc_TtHieMan_t_
1241 {
1242 int nLastLevel, nWords;
1243 Vec_Mem_t * vTtMem[TT_MAX_LEVELS]; // truth table memory and hash tables
1244 Vec_Int_t * vRepres[TT_MAX_LEVELS]; // pointers to the representatives from the last hierarchical level
1245 int vTruthId[TT_MAX_LEVELS];
1246
1247 Vec_Int_t * vPhase;
1248 };
1249
Abc_TtHieManStart(int nVars,int nLevels)1250 Abc_TtHieMan_t * Abc_TtHieManStart(int nVars, int nLevels)
1251 {
1252 Abc_TtHieMan_t * p = NULL;
1253 int i;
1254 if (nLevels > TT_MAX_LEVELS) return p;
1255 p = ABC_CALLOC(Abc_TtHieMan_t, 1);
1256 p->nLastLevel = nLevels - 1;
1257 p->nWords = Abc_TtWordNum(nVars);
1258 for (i = 0; i < nLevels; i++)
1259 {
1260 p->vTtMem[i] = Vec_MemAlloc(p->nWords, 12);
1261 Vec_MemHashAlloc(p->vTtMem[i], 10000);
1262 p->vRepres[i] = Vec_IntAlloc(1);
1263 }
1264 p->vPhase = Vec_IntAlloc(2500);
1265 return p;
1266 }
1267
Abc_TtHieManStop(Abc_TtHieMan_t * p)1268 void Abc_TtHieManStop(Abc_TtHieMan_t * p)
1269 {
1270 int i;
1271 for (i = 0; i <= p->nLastLevel; i++)
1272 {
1273 Vec_MemHashFree(p->vTtMem[i]);
1274 Vec_MemFreeP(&p->vTtMem[i]);
1275 Vec_IntFree(p->vRepres[i]);
1276 }
1277 Vec_IntFree( p->vPhase );
1278 ABC_FREE(p);
1279 }
1280
Abc_TtHieRetrieveOrInsert(Abc_TtHieMan_t * p,int level,word * pTruth,word * pResult)1281 int Abc_TtHieRetrieveOrInsert(Abc_TtHieMan_t * p, int level, word * pTruth, word * pResult)
1282 {
1283 int i, iSpot, truthId;
1284 word * pRepTruth;
1285 if (!p) return -1;
1286 if (level < 0) level += p->nLastLevel + 1;
1287 if (level < 0 || level > p->nLastLevel) return -1;
1288 iSpot = *Vec_MemHashLookup(p->vTtMem[level], pTruth);
1289 if (iSpot == -1) {
1290 p->vTruthId[level] = Vec_MemHashInsert(p->vTtMem[level], pTruth);
1291 if (level < p->nLastLevel) return 0;
1292 iSpot = p->vTruthId[level];
1293 }
1294 // return the class representative
1295 if (level < p->nLastLevel)
1296 truthId = Vec_IntEntry(p->vRepres[level], iSpot);
1297 else
1298 truthId = iSpot;
1299 for (i = 0; i < level; i++)
1300 Vec_IntSetEntry(p->vRepres[i], p->vTruthId[i], truthId);
1301
1302 pRepTruth = Vec_MemReadEntry(p->vTtMem[p->nLastLevel], truthId);
1303 if (level < p->nLastLevel) {
1304 Abc_TtCopy(pResult, pRepTruth, p->nWords, 0);
1305 return 1;
1306 }
1307 assert(Abc_TtEqual(pTruth, pRepTruth, p->nWords));
1308 if (pTruth != pResult)
1309 Abc_TtCopy(pResult, pRepTruth, p->nWords, 0);
1310 return 0;
1311 }
1312
Abc_TtCanonicizeHie(Abc_TtHieMan_t * p,word * pTruthInit,int nVars,char * pCanonPerm,int fExact)1313 unsigned Abc_TtCanonicizeHie( Abc_TtHieMan_t * p, word * pTruthInit, int nVars, char * pCanonPerm, int fExact )
1314 {
1315 int fNaive = 1;
1316 int pStore[17];
1317 //static word pTruth[1024];
1318 word * pTruth = pTruthInit;
1319 unsigned uCanonPhase = 0;
1320 int nOnes, nWords = Abc_TtWordNum( nVars );
1321 int i, k;
1322 assert( nVars <= 16 );
1323
1324 // handle constant
1325 if ( nVars == 0 )
1326 {
1327 Abc_TtClear( pTruthInit, nWords );
1328 return 0;
1329 }
1330
1331 //Abc_TtCopy( pTruth, pTruthInit, nWords, 0 );
1332
1333 for ( i = 0; i < nVars; i++ )
1334 pCanonPerm[i] = i;
1335
1336 // normalize polarity
1337 nOnes = Abc_TtCountOnesInTruth( pTruth, nVars );
1338 if ( nOnes > nWords * 32 )
1339 {
1340 Abc_TtNot( pTruth, nWords );
1341 nOnes = nWords*64 - nOnes;
1342 uCanonPhase |= (1 << nVars);
1343 }
1344 // check cache
1345 if (Abc_TtHieRetrieveOrInsert(p, 0, pTruth, pTruthInit) > 0) return 0;
1346
1347 // normalize phase
1348 Abc_TtCountOnesInCofs( pTruth, nVars, pStore );
1349 pStore[nVars] = nOnes;
1350 for ( i = 0; i < nVars; i++ )
1351 {
1352 if ( pStore[i] >= nOnes - pStore[i] )
1353 continue;
1354 Abc_TtFlip( pTruth, nWords, i );
1355 uCanonPhase |= (1 << i);
1356 pStore[i] = nOnes - pStore[i];
1357 }
1358 // check cache
1359 if (Abc_TtHieRetrieveOrInsert(p, 1, pTruth, pTruthInit) > 0) return 0;
1360
1361 // normalize permutation
1362 {
1363 int k, BestK;
1364 for ( i = 0; i < nVars - 1; i++ )
1365 {
1366 BestK = i + 1;
1367 for ( k = i + 2; k < nVars; k++ )
1368 if ( pStore[BestK] > pStore[k] )
1369 BestK = k;
1370 if ( pStore[i] <= pStore[BestK] )
1371 continue;
1372 ABC_SWAP( int, pCanonPerm[i], pCanonPerm[BestK] );
1373 ABC_SWAP( int, pStore[i], pStore[BestK] );
1374 if ( ((uCanonPhase >> i) & 1) != ((uCanonPhase >> BestK) & 1) )
1375 {
1376 uCanonPhase ^= (1 << i);
1377 uCanonPhase ^= (1 << BestK);
1378 }
1379 Abc_TtSwapVars( pTruth, nVars, i, BestK );
1380 }
1381 }
1382 // check cache
1383 if (Abc_TtHieRetrieveOrInsert(p, 2, pTruth, pTruthInit) > 0) return 0;
1384
1385 // iterate TT permutations for tied variables
1386 for ( k = 0; k < 5; k++ )
1387 {
1388 int fChanges = 0;
1389 for ( i = nVars - 2; i >= 0; i-- )
1390 if ( pStore[i] == pStore[i+1] )
1391 fChanges |= Abc_TtCofactorPerm( pTruth, i, nWords, pStore[i] != pStore[nVars]/2, pCanonPerm, &uCanonPhase, fNaive );
1392 if ( !fChanges )
1393 break;
1394 fChanges = 0;
1395 for ( i = 1; i < nVars - 1; i++ )
1396 if ( pStore[i] == pStore[i+1] )
1397 fChanges |= Abc_TtCofactorPerm( pTruth, i, nWords, pStore[i] != pStore[nVars]/2, pCanonPerm, &uCanonPhase, fNaive );
1398 if ( !fChanges )
1399 break;
1400 }
1401 // check cache
1402 if (Abc_TtHieRetrieveOrInsert(p, 3, pTruth, pTruthInit) > 0) return 0;
1403
1404 // perform exact NPN using groups
1405 if ( fExact ) {
1406 extern void simpleMinimalGroups(word* x, word* pAux, word* minimal, int* pGroups, int nGroups, permInfo** pis, int nVars, int fFlipOutput, int fFlipInput);
1407 word pAuxWord[1024], pAuxWord1[1024];
1408 int pGroups[16];
1409 int nGroups = 0;
1410 permInfo * pis[17];
1411 // get groups
1412 pGroups[0] = 0;
1413 for (i = 0; i < nVars - 1; i++) {
1414 if (pStore[i] == pStore[i + 1]) {
1415 pGroups[nGroups]++;
1416 } else {
1417 pGroups[nGroups]++;
1418 nGroups++;
1419 pGroups[nGroups] = 0;
1420 }
1421 }
1422 pGroups[nGroups]++;
1423 nGroups++;
1424
1425 // compute permInfo from 0 to nVars (incl.)
1426 for (i = 0; i <= nVars; i++) {
1427 pis[i] = setPermInfoPtr(i);
1428 }
1429
1430 // do the exact matching
1431 if (nOnes == nWords * 32) /* balanced output */
1432 simpleMinimalGroups(pTruth, pAuxWord, pAuxWord1, pGroups, nGroups, pis, nVars, 1, 1);
1433 else if (pStore[0] != pStore[1] && pStore[0] == (nOnes - pStore[0])) /* balanced singleton input */
1434 simpleMinimalGroups(pTruth, pAuxWord, pAuxWord1, pGroups, nGroups, pis, nVars, 0, 1);
1435 else
1436 simpleMinimalGroups(pTruth, pAuxWord, pAuxWord1, pGroups, nGroups, pis, nVars, 0, 0);
1437
1438 // cleanup
1439 for (i = 0; i <= nVars; i++) {
1440 freePermInfoPtr(pis[i]);
1441 }
1442 }
1443 // update cache
1444 Abc_TtHieRetrieveOrInsert(p, 4, pTruth, pTruthInit);
1445 return 0;
1446 }
1447
1448
1449 /**Function*************************************************************
1450
1451 Synopsis [Adaptive exact/semi-canonical form computation.]
1452
1453 Description []
1454
1455 SideEffects []
1456
1457 SeeAlso []
1458
1459 ***********************************************************************/
1460
1461 typedef struct TiedGroup_
1462 {
1463 char iStart; // index of Abc_TgMan_t::pPerm
1464 char nGVars; // the number of variables in the group
1465 } TiedGroup;
1466
1467 typedef struct Abc_TgMan_t_
1468 {
1469 word *pTruth;
1470 int nVars; // the number of variables
1471 int nGVars; // the number of variables in groups ( symmetric variables purged )
1472 int nGroups; // the number of tied groups
1473 unsigned uPhase; // phase of each variable and the function
1474 int fPhased; // if the phases of all the variables are determined
1475 char pPerm[16]; // permutation of variables, symmetric variables purged, for grouping
1476 char pPermT[16]; // permutation of variables, symmetric variables expanded, actual transformation for pTruth
1477 char pPermTRev[16]; // reverse permutation of pPermT
1478 signed char pPermDir[16]; // for generating the next permutation
1479 TiedGroup pGroup[16]; // tied groups
1480 // symemtric group attributes
1481 char symPhase[16]; // phase type of symemtric groups
1482 signed char symLink[17]; // singly linked list, indicate the variables in symemtric groups
1483
1484 int nAlgorithm; // 0: AdjCE, 1: AdjSE, 2: E: Cost-Aware
1485 char pFGrps[16]; // tied groups to be flipped
1486 Vec_Int_t * vPhase; // candidate phase assignments
1487 } Abc_TgMan_t;
1488
1489 #if !defined(NDEBUG) && !defined(CANON_VERIFY)
1490 #define CANON_VERIFY
1491 #endif
1492 /**Function*************************************************************
1493
1494 Synopsis [Utilities.]
1495
1496 Description []
1497
1498 SideEffects []
1499
1500 SeeAlso []
1501
1502 ***********************************************************************/
1503
1504 // Johnson�CTrotter algorithm
Abc_NextPermSwapC(char * pData,signed char * pDir,int size)1505 static int Abc_NextPermSwapC(char * pData, signed char * pDir, int size)
1506 {
1507 int i, j, k = -1;
1508 for (i = 0; i < size; i++)
1509 {
1510 j = i + pDir[i];
1511 if (j >= 0 && j < size && pData[i] > pData[j] && (k < 0 || pData[i] > pData[k]))
1512 k = i;
1513 }
1514 if (k < 0) k = 0;
1515
1516 for (i = 0; i < size; i++)
1517 if (pData[i] > pData[k])
1518 pDir[i] = -pDir[i];
1519
1520 j = k + pDir[k];
1521 return j < k ? j : k;
1522 }
1523
1524 //typedef unsigned(*TtCanonicizeFunc)(Abc_TtHieMan_t * p, word * pTruth, int nVars, char * pCanonPerm, int flag);
Abc_TtCanonicizeWrap(TtCanonicizeFunc func,Abc_TtHieMan_t * p,word * pTruth,int nVars,char * pCanonPerm,int flag)1525 unsigned Abc_TtCanonicizeWrap(TtCanonicizeFunc func, Abc_TtHieMan_t * p, word * pTruth, int nVars, char * pCanonPerm, int flag)
1526 {
1527 int nWords = Abc_TtWordNum(nVars);
1528 unsigned uCanonPhase1, uCanonPhase2;
1529 char pCanonPerm2[16];
1530 static word pTruth2[1024];
1531
1532 Abc_TtNormalizeSmallTruth(pTruth, nVars);
1533 if (Abc_TtCountOnesInTruth(pTruth, nVars) != nWords * 32)
1534 return func(p, pTruth, nVars, pCanonPerm, flag);
1535 Abc_TtCopy(pTruth2, pTruth, nWords, 1);
1536 uCanonPhase1 = func(p, pTruth, nVars, pCanonPerm, flag);
1537 uCanonPhase2 = func(p, pTruth2, nVars, pCanonPerm2, flag);
1538 if (Abc_TtCompareRev(pTruth, pTruth2, nWords) <= 0)
1539 return uCanonPhase1;
1540 Abc_TtCopy(pTruth, pTruth2, nWords, 0);
1541 memcpy(pCanonPerm, pCanonPerm2, nVars);
1542 return uCanonPhase2;
1543 }
1544
1545 word gpVerCopy[1024];
Abc_TtCannonVerify(word * pTruth,int nVars,char * pCanonPerm,unsigned uCanonPhase)1546 static int Abc_TtCannonVerify(word* pTruth, int nVars, char * pCanonPerm, unsigned uCanonPhase)
1547 {
1548 #ifdef CANON_VERIFY
1549 int nWords = Abc_TtWordNum(nVars);
1550 char pCanonPermCopy[16];
1551 static word pCopy2[1024];
1552 Abc_TtVerifySmallTruth(pTruth, nVars);
1553 Abc_TtCopy(pCopy2, pTruth, nWords, 0);
1554 memcpy(pCanonPermCopy, pCanonPerm, sizeof(char) * nVars);
1555 Abc_TtImplementNpnConfig(pCopy2, nVars, pCanonPermCopy, uCanonPhase);
1556 return Abc_TtEqual(gpVerCopy, pCopy2, nWords);
1557 #else
1558 return 1;
1559 #endif
1560 }
1561
1562 /**Function*************************************************************
1563
1564 Synopsis [Tied group management.]
1565
1566 Description []
1567
1568 SideEffects []
1569
1570 SeeAlso []
1571
1572 ***********************************************************************/
1573
Abc_TgInitMan(Abc_TgMan_t * pMan,word * pTruth,int nVars,int nAlg,Vec_Int_t * vPhase)1574 static void Abc_TgInitMan(Abc_TgMan_t * pMan, word * pTruth, int nVars, int nAlg, Vec_Int_t * vPhase)
1575 {
1576 int i;
1577 pMan->pTruth = pTruth;
1578 pMan->uPhase = 0;
1579 pMan->fPhased = 0;
1580 pMan->nVars = pMan->nGVars = nVars;
1581 pMan->nGroups = 1;
1582 pMan->pGroup[0].iStart = 0;
1583 pMan->pGroup[0].nGVars = nVars;
1584 for (i = 0; i < nVars; i++)
1585 {
1586 pMan->pPerm[i] = i;
1587 pMan->pPermT[i] = i;
1588 pMan->pPermTRev[i] = i;
1589 pMan->symPhase[i] = 1;
1590 pMan->symLink[i] = -1;
1591 }
1592 pMan->symLink[i] = -1;
1593 pMan->nAlgorithm = nAlg;
1594 pMan->vPhase = vPhase;
1595 Vec_IntClear(vPhase);
1596 }
1597
Abc_TgSplitGroup(Abc_TgMan_t * pMan,TiedGroup * pGrp,int * pCoef)1598 static int Abc_TgSplitGroup(Abc_TgMan_t * pMan, TiedGroup * pGrp, int * pCoef)
1599 {
1600 int i, j, n = 0;
1601 int nGVars = pGrp->nGVars;
1602 char * pVars = pMan->pPerm + pGrp->iStart;
1603 int iGrp = pGrp - pMan->pGroup;
1604
1605 // sort variables
1606 for (i = 1; i < nGVars; i++)
1607 {
1608 int a = pCoef[i]; char aa = pVars[i];
1609 for (j = i; j > 0 && pCoef[j - 1] > a; j--)
1610 pCoef[j] = pCoef[j - 1], pVars[j] = pVars[j - 1];
1611 pCoef[j] = a; pVars[j] = aa;
1612 }
1613 for (i = 1; i < nGVars; i++)
1614 if (pCoef[i] != pCoef[i - 1]) n++;
1615 if (n == 0) return 0;
1616 memmove(pGrp + n + 1, pGrp + 1, (pMan->nGroups - iGrp - 1) * sizeof(TiedGroup));
1617 // group variables
1618 for (i = j = 1; i < nGVars; i++)
1619 {
1620 if (pCoef[i] == pCoef[i - 1]) continue;
1621 pGrp[j].iStart = pGrp->iStart + i;
1622 pGrp[j - 1].nGVars = pGrp[j].iStart - pGrp[j - 1].iStart;
1623 j++;
1624 }
1625 assert(j == n + 1);
1626 pGrp[n].nGVars = pGrp->iStart + i - pGrp[n].iStart;
1627 pMan->nGroups += n;
1628 return n;
1629 }
Abc_TgManCopy(Abc_TgMan_t * pDst,word * pDstTruth,Abc_TgMan_t * pSrc)1630 static inline void Abc_TgManCopy(Abc_TgMan_t* pDst, word* pDstTruth, Abc_TgMan_t* pSrc)
1631 {
1632 *pDst = *pSrc;
1633 Abc_TtCopy(pDstTruth, pSrc->pTruth, Abc_TtWordNum(pSrc->nVars), 0);
1634 pDst->pTruth = pDstTruth;
1635 }
1636
Abc_TgCannonVerify(Abc_TgMan_t * pMan)1637 static inline int Abc_TgCannonVerify(Abc_TgMan_t* pMan)
1638 {
1639 return Abc_TtCannonVerify(pMan->pTruth, pMan->nVars, pMan->pPermT, pMan->uPhase);
1640 }
1641
1642 extern int Abc_TgExpendSymmetry(Abc_TgMan_t * pMan, char * pDest);
1643
CheckConfig(Abc_TgMan_t * pMan)1644 static void CheckConfig(Abc_TgMan_t * pMan)
1645 {
1646 #ifndef NDEBUG
1647 int i;
1648 char pPermE[16];
1649 Abc_TgExpendSymmetry(pMan, pPermE);
1650 for (i = 0; i < pMan->nVars; i++)
1651 {
1652 assert(pPermE[i] == pMan->pPermT[i]);
1653 assert(pMan->pPermTRev[(int)pMan->pPermT[i]] == i);
1654 }
1655 assert(Abc_TgCannonVerify(pMan));
1656 #endif
1657 }
1658
1659 /**Function*************************************************************
1660
1661 Synopsis [Truthtable manipulation.]
1662
1663 Description []
1664
1665 SideEffects []
1666
1667 SeeAlso []
1668
1669 ***********************************************************************/
1670
Abc_TgFlipVar(Abc_TgMan_t * pMan,int iVar)1671 static inline void Abc_TgFlipVar(Abc_TgMan_t* pMan, int iVar)
1672 {
1673 int nWords = Abc_TtWordNum(pMan->nVars);
1674 int ivp = pMan->pPermTRev[iVar];
1675 Abc_TtFlip(pMan->pTruth, nWords, ivp);
1676 pMan->uPhase ^= 1 << ivp;
1677 }
1678
Abc_TgFlipSymGroupByVar(Abc_TgMan_t * pMan,int iVar)1679 static inline void Abc_TgFlipSymGroupByVar(Abc_TgMan_t* pMan, int iVar)
1680 {
1681 for (; iVar >= 0; iVar = pMan->symLink[iVar])
1682 if (pMan->symPhase[iVar])
1683 Abc_TgFlipVar(pMan, iVar);
1684 }
1685
Abc_TgFlipSymGroup(Abc_TgMan_t * pMan,int idx)1686 static inline void Abc_TgFlipSymGroup(Abc_TgMan_t* pMan, int idx)
1687 {
1688 Abc_TgFlipSymGroupByVar(pMan, pMan->pPerm[idx]);
1689 }
1690
Abc_TgClearSymGroupPhase(Abc_TgMan_t * pMan,int iVar)1691 static inline void Abc_TgClearSymGroupPhase(Abc_TgMan_t* pMan, int iVar)
1692 {
1693 for (; iVar >= 0; iVar = pMan->symLink[iVar])
1694 pMan->symPhase[iVar] = 0;
1695 }
1696
Abc_TgImplementPerm(Abc_TgMan_t * pMan,const char * pPermDest)1697 static void Abc_TgImplementPerm(Abc_TgMan_t* pMan, const char *pPermDest)
1698 {
1699 int i, nVars = pMan->nVars;
1700 char *pPerm = pMan->pPermT;
1701 char *pRev = pMan->pPermTRev;
1702 unsigned uPhase = pMan->uPhase & (1 << nVars);
1703
1704 for (i = 0; i < nVars; i++)
1705 pRev[(int)pPerm[i]] = i;
1706 for (i = 0; i < nVars; i++)
1707 pPerm[i] = pRev[(int)pPermDest[i]];
1708 for (i = 0; i < nVars; i++)
1709 pRev[(int)pPerm[i]] = i;
1710
1711 Abc_TtImplementNpnConfig(pMan->pTruth, nVars, pRev, 0);
1712 // Abc_TtVerifySmallTruth(pMan->pTruth, nVars);
1713
1714 for (i = 0; i < nVars; i++)
1715 {
1716 if (pMan->uPhase & (1 << pPerm[i]))
1717 uPhase |= (1 << i);
1718 pPerm[i] = pPermDest[i];
1719 pRev[(int)pPerm[i]] = i;
1720 }
1721 pMan->uPhase = uPhase;
1722 }
1723
Abc_TgSwapAdjacentSymGroups(Abc_TgMan_t * pMan,int idx)1724 static void Abc_TgSwapAdjacentSymGroups(Abc_TgMan_t* pMan, int idx)
1725 {
1726 int iVar, jVar, ix;
1727 char pPermNew[16];
1728 assert(idx < pMan->nGVars - 1);
1729 iVar = pMan->pPerm[idx];
1730 jVar = pMan->pPerm[idx + 1];
1731 pMan->pPerm[idx] = jVar;
1732 pMan->pPerm[idx + 1] = iVar;
1733 ABC_SWAP(char, pMan->pPermDir[idx], pMan->pPermDir[idx + 1]);
1734 if (pMan->symLink[iVar] >= 0 || pMan->symLink[jVar] >= 0)
1735 {
1736 Abc_TgExpendSymmetry(pMan, pPermNew);
1737 Abc_TgImplementPerm(pMan, pPermNew);
1738 return;
1739 }
1740 // plain variable swap
1741 ix = pMan->pPermTRev[iVar];
1742 assert(pMan->pPermT[ix] == iVar && pMan->pPermT[ix + 1] == jVar);
1743 Abc_TtSwapAdjacent(pMan->pTruth, Abc_TtWordNum(pMan->nVars), ix);
1744 pMan->pPermT[ix] = jVar;
1745 pMan->pPermT[ix + 1] = iVar;
1746 pMan->pPermTRev[iVar] = ix + 1;
1747 pMan->pPermTRev[jVar] = ix;
1748 if (((pMan->uPhase >> ix) & 1) != ((pMan->uPhase >> (ix + 1)) & 1))
1749 pMan->uPhase ^= 1 << ix | 1 << (ix + 1);
1750 assert(Abc_TgCannonVerify(pMan));
1751 }
1752
1753 /**Function*************************************************************
1754
1755 Synopsis [semmetry of two variables.]
1756
1757 Description []
1758
1759 SideEffects []
1760
1761 SeeAlso []
1762
1763 ***********************************************************************/
1764
1765 static word pSymCopy[1024];
1766
Abc_TtIsSymmetric(word * pTruth,int nVars,int iVar,int jVar,int fPhase)1767 static int Abc_TtIsSymmetric(word * pTruth, int nVars, int iVar, int jVar, int fPhase)
1768 {
1769 int rv;
1770 int nWords = Abc_TtWordNum(nVars);
1771 Abc_TtCopy(pSymCopy, pTruth, nWords, 0);
1772 Abc_TtSwapVars(pSymCopy, nVars, iVar, jVar);
1773 rv = Abc_TtEqual(pTruth, pSymCopy, nWords) * 2;
1774 if (!fPhase) return rv;
1775 Abc_TtFlip(pSymCopy, nWords, iVar);
1776 Abc_TtFlip(pSymCopy, nWords, jVar);
1777 return rv + Abc_TtEqual(pTruth, pSymCopy, nWords);
1778 }
1779
Abc_TtIsSymmetricHigh(Abc_TgMan_t * pMan,int iVar,int jVar,int fPhase)1780 static int Abc_TtIsSymmetricHigh(Abc_TgMan_t * pMan, int iVar, int jVar, int fPhase)
1781 {
1782 int rv, iv, jv, n;
1783 int nWords = Abc_TtWordNum(pMan->nVars);
1784 Abc_TtCopy(pSymCopy, pMan->pTruth, nWords, 0);
1785 for (n = 0, iv = iVar, jv = jVar; iv >= 0 && jv >= 0; iv = pMan->symLink[iv], jv = pMan->symLink[jv], n++)
1786 Abc_TtSwapVars(pSymCopy, pMan->nVars, iv, jv);
1787 assert(iv < 0 && jv < 0); // two symmetric groups must have the same size
1788 rv = Abc_TtEqual(pMan->pTruth, pSymCopy, nWords) * 2;
1789 if (!fPhase) return rv;
1790 for (iv = iVar, jv = jVar; iv >= 0 && jv >= 0; iv = pMan->symLink[iv], jv = pMan->symLink[jv])
1791 {
1792 if (pMan->symPhase[iv]) Abc_TtFlip(pSymCopy, nWords, iv);
1793 if (pMan->symPhase[jv]) Abc_TtFlip(pSymCopy, nWords, jv);
1794 }
1795 return rv + Abc_TtEqual(pMan->pTruth, pSymCopy, nWords);
1796 }
1797
1798 /**Function*************************************************************
1799
1800 Synopsis [Create groups by cofactor signatures]
1801
1802 Description [Similar to Abc_TtSemiCanonicize.
1803 Use stable insertion sort to keep the order of the variables in the groups.
1804 Defer permutation. ]
1805
1806 SideEffects []
1807
1808 SeeAlso []
1809
1810 ***********************************************************************/
1811
Abc_TgCreateGroups(Abc_TgMan_t * pMan)1812 static void Abc_TgCreateGroups(Abc_TgMan_t * pMan)
1813 {
1814 int pStore[17];
1815 int i, nOnes;
1816 int nVars = pMan->nVars, nWords = Abc_TtWordNum(nVars);
1817 //TiedGroup * pGrp = pMan->pGroup;
1818 assert(nVars <= 16);
1819 // normalize polarity
1820 nOnes = Abc_TtCountOnesInTruth(pMan->pTruth, nVars);
1821 if (nOnes > nWords * 32)
1822 {
1823 Abc_TtNot(pMan->pTruth, nWords);
1824 nOnes = nWords * 64 - nOnes;
1825 pMan->uPhase |= (1 << nVars);
1826 }
1827 // normalize phase
1828 Abc_TtCountOnesInCofs(pMan->pTruth, nVars, pStore);
1829 pStore[nVars] = nOnes;
1830 for (i = 0; i < nVars; i++)
1831 {
1832 if (pStore[i] >= nOnes - pStore[i])
1833 continue;
1834 Abc_TtFlip(pMan->pTruth, nWords, i);
1835 pMan->uPhase |= (1 << i);
1836 pStore[i] = nOnes - pStore[i];
1837 }
1838
1839 Abc_TgSplitGroup(pMan, pMan->pGroup, pStore);
1840 pMan->fPhased = pStore[0] * 2 != nOnes;
1841 }
1842
1843 /**Function*************************************************************
1844
1845 Synopsis [Group symmetric variables.]
1846
1847 Description []
1848
1849 SideEffects []
1850
1851 SeeAlso []
1852
1853 ***********************************************************************/
1854
Abc_TgGroupSymmetry(Abc_TgMan_t * pMan,TiedGroup * pGrp,int fHigh)1855 static int Abc_TgGroupSymmetry(Abc_TgMan_t * pMan, TiedGroup * pGrp, int fHigh)
1856 {
1857 int i, j, iVar, jVar, nsym = 0;
1858 int fDone[16], scnt[16], stype[16];
1859 signed char *symLink = pMan->symLink;
1860 // char * symPhase = pMan->symPhase;
1861 int nGVars = pGrp->nGVars;
1862 int fPhase = (pGrp == pMan->pGroup) && !pMan->fPhased;
1863 char * pVars = pMan->pPerm + pGrp->iStart;
1864 int modified;
1865
1866 for (i = 0; i < nGVars; i++)
1867 fDone[i] = 0, scnt[i] = 1;
1868
1869 do {
1870 modified = 0;
1871 for (i = 0; i < nGVars - 1; i++)
1872 {
1873 iVar = pVars[i];
1874 if (iVar < 0 || fDone[i]) continue;
1875 // if (!pGrp->fPhased && !Abc_TtHasVar(pMan->pTruth, pMan->nVars, iVar)) continue;
1876 // Mark symmetric variables/groups
1877 for (j = i + 1; j < nGVars; j++)
1878 {
1879 jVar = pVars[j];
1880 if (jVar < 0 || scnt[j] != scnt[i]) // || pMan->symPhase[jVar] != pMan->symPhase[iVar])
1881 stype[j] = 0;
1882 else if (scnt[j] == 1)
1883 stype[j] = Abc_TtIsSymmetric(pMan->pTruth, pMan->nVars, iVar, jVar, fPhase);
1884 else
1885 stype[j] = Abc_TtIsSymmetricHigh(pMan, iVar, jVar, fPhase);
1886 }
1887 fDone[i] = 1;
1888 // Merge symmetric groups
1889 for (j = i + 1; j < nGVars; j++)
1890 {
1891 int ii;
1892 jVar = pVars[j];
1893 switch (stype[j])
1894 {
1895 case 1: // E-Symmetry
1896 Abc_TgFlipSymGroupByVar(pMan, jVar);
1897 // fallthrough
1898 case 2: // NE-Symmetry
1899 pMan->symPhase[iVar] += pMan->symPhase[jVar];
1900 break;
1901 case 3: // multiform Symmetry
1902 Abc_TgClearSymGroupPhase(pMan, jVar);
1903 break;
1904 default: // case 0: No Symmetry
1905 continue;
1906 }
1907
1908 for (ii = iVar; symLink[ii] >= 0; ii = symLink[ii])
1909 ;
1910 symLink[ii] = jVar;
1911 pVars[j] = -1;
1912 scnt[i] += scnt[j];
1913 modified = 1;
1914 fDone[i] = 0;
1915 nsym++;
1916 }
1917 }
1918 // if (++order > 3) printf("%d", order);
1919 } while (fHigh && modified);
1920
1921 return nsym;
1922 }
1923
Abc_TgPurgeSymmetry(Abc_TgMan_t * pMan,int fHigh)1924 static void Abc_TgPurgeSymmetry(Abc_TgMan_t * pMan, int fHigh)
1925 {
1926 int i, j, k, sum = 0, nVars = pMan->nVars;
1927 signed char *symLink = pMan->symLink;
1928 char gcnt[16] = { 0 };
1929 char * pPerm = pMan->pPerm;
1930
1931 // purge unsupported variables
1932 if (!pMan->fPhased)
1933 {
1934 int iVar = pMan->nVars;
1935 for (j = 0; j < pMan->pGroup[0].nGVars; j++)
1936 {
1937 int jVar = pPerm[j];
1938 assert(jVar >= 0);
1939 if (!Abc_TtHasVar(pMan->pTruth, nVars, jVar))
1940 {
1941 symLink[jVar] = symLink[iVar];
1942 symLink[iVar] = jVar;
1943 pPerm[j] = -1;
1944 gcnt[0]++;
1945 }
1946 }
1947 }
1948
1949 for (k = 0; k < pMan->nGroups; k++)
1950 gcnt[k] += Abc_TgGroupSymmetry(pMan, pMan->pGroup + k, fHigh);
1951
1952 for (i = 0; i < nVars && pPerm[i] >= 0; i++)
1953 ;
1954 for (j = i + 1; ; i++, j++)
1955 {
1956 while (j < nVars && pPerm[j] < 0) j++;
1957 if (j >= nVars) break;
1958 pPerm[i] = pPerm[j];
1959 }
1960 for (k = 0; k < pMan->nGroups; k++)
1961 {
1962 pMan->pGroup[k].nGVars -= gcnt[k];
1963 pMan->pGroup[k].iStart -= sum;
1964 sum += gcnt[k];
1965 }
1966 if (pMan->pGroup[0].nGVars == 0)
1967 {
1968 pMan->nGroups--;
1969 memmove(pMan->pGroup, pMan->pGroup + 1, sizeof(TiedGroup) * pMan->nGroups);
1970 assert(pMan->pGroup[0].iStart == 0);
1971 }
1972 pMan->nGVars -= sum;
1973 }
1974
Abc_TgExpendSymmetry(Abc_TgMan_t * pMan,char * pDest)1975 int Abc_TgExpendSymmetry(Abc_TgMan_t * pMan, char * pDest)
1976 {
1977 int i = 0, j, k, s;
1978 char * pPerm = pMan->pPerm;
1979 for (j = 0; j < pMan->nGVars; j++)
1980 for (k = pPerm[j]; k >= 0; k = pMan->symLink[k])
1981 pDest[i++] = k;
1982 s = i;
1983 for (k = pMan->symLink[pMan->nVars]; k >= 0; k = pMan->symLink[k])
1984 pDest[i++] = k;
1985 assert(i == pMan->nVars);
1986 return s;
1987 }
1988
Abc_TgResetGroup(Abc_TgMan_t * pMan)1989 static void Abc_TgResetGroup(Abc_TgMan_t * pMan)
1990 {
1991 int i, j;
1992 char * pPerm = pMan->pPerm;
1993 char pPermNew[16];
1994 int nGVars = pMan->nGVars;
1995 for (i = 1; i < nGVars; i++)
1996 {
1997 char t = pPerm[i];
1998 for (j = i; j > 0 && pPerm[j - 1] > t; j--)
1999 pPerm[j] = pPerm[j - 1];
2000 pPerm[j] = t;
2001 }
2002 Abc_TgExpendSymmetry(pMan, pPermNew);
2003 Abc_TgImplementPerm(pMan, pPermNew);
2004 pMan->fPhased = 0;
2005 pMan->nGroups = 1;
2006 pMan->pGroup->nGVars = nGVars;
2007 Vec_IntClear(pMan->vPhase);
2008 }
2009
Abc_TgResetGroup1(Abc_TgMan_t * pMan)2010 static void Abc_TgResetGroup1(Abc_TgMan_t * pMan)
2011 {
2012 int i, j;
2013 char pPermNew[16];
2014 int nSVars = Abc_TgExpendSymmetry(pMan, pPermNew);
2015 for (i = 1; i < nSVars; i++)
2016 {
2017 char t = pPermNew[i];
2018 for (j = i; j > 0 && pPermNew[j - 1] > t; j--)
2019 pPermNew[j] = pPermNew[j - 1];
2020 pPermNew[j] = t;
2021 }
2022 Abc_TgImplementPerm(pMan, pPermNew);
2023 pMan->fPhased = 0;
2024 pMan->nGroups = 1;
2025 pMan->nGVars = pMan->pGroup->nGVars = nSVars;
2026 for (i = 0; i < pMan->nVars; i++)
2027 {
2028 pMan->pPerm[i] = pPermNew[i];
2029 pMan->symPhase[i] = 1;
2030 pMan->symLink[i] = -1;
2031 }
2032 Vec_IntClear(pMan->vPhase);
2033 }
2034
2035 /**Function*************************************************************
2036
2037 Synopsis [Semi-canonical form computation.]
2038
2039 Description [simple config enumeration]
2040
2041 SideEffects []
2042
2043 SeeAlso []
2044
2045 ***********************************************************************/
Abc_TgSymGroupPerm(Abc_TgMan_t * pMan,int idx,int fSwapOnly)2046 static int Abc_TgSymGroupPerm(Abc_TgMan_t* pMan, int idx, int fSwapOnly)
2047 {
2048 word* pTruth = pMan->pTruth;
2049 static word pCopy[1024];
2050 static word pBest[1024];
2051 int Config = 0;
2052 int nWords = Abc_TtWordNum(pMan->nVars);
2053 Abc_TgMan_t tgManCopy, tgManBest;
2054
2055 CheckConfig(pMan);
2056 if (fSwapOnly)
2057 {
2058 Abc_TgManCopy(&tgManCopy, pCopy, pMan);
2059 Abc_TgSwapAdjacentSymGroups(&tgManCopy, idx);
2060 CheckConfig(&tgManCopy);
2061 if (Abc_TtCompareRev(pTruth, pCopy, nWords) < 0)
2062 {
2063 Abc_TgManCopy(pMan, pTruth, &tgManCopy);
2064 return 4;
2065 }
2066 return 0;
2067 }
2068
2069 // save two copies
2070 Abc_TgManCopy(&tgManCopy, pCopy, pMan);
2071 Abc_TgManCopy(&tgManBest, pBest, pMan);
2072 // PXY
2073 // 001
2074 Abc_TgFlipSymGroup(&tgManCopy, idx);
2075 CheckConfig(&tgManCopy);
2076 if (Abc_TtCompareRev(pBest, pCopy, nWords) == 1)
2077 Abc_TgManCopy(&tgManBest, pBest, &tgManCopy), Config = 1;
2078 // PXY
2079 // 011
2080 Abc_TgFlipSymGroup(&tgManCopy, idx + 1);
2081 CheckConfig(&tgManCopy);
2082 if (Abc_TtCompareRev(pBest, pCopy, nWords) == 1)
2083 Abc_TgManCopy(&tgManBest, pBest, &tgManCopy), Config = 3;
2084 // PXY
2085 // 010
2086 Abc_TgFlipSymGroup(&tgManCopy, idx);
2087 CheckConfig(&tgManCopy);
2088 if (Abc_TtCompareRev(pBest, pCopy, nWords) == 1)
2089 Abc_TgManCopy(&tgManBest, pBest, &tgManCopy), Config = 2;
2090 // PXY
2091 // 110
2092 Abc_TgSwapAdjacentSymGroups(&tgManCopy, idx);
2093 CheckConfig(&tgManCopy);
2094 if (Abc_TtCompareRev(pBest, pCopy, nWords) == 1)
2095 Abc_TgManCopy(&tgManBest, pBest, &tgManCopy), Config = 6;
2096 // PXY
2097 // 111
2098 Abc_TgFlipSymGroup(&tgManCopy, idx + 1);
2099 CheckConfig(&tgManCopy);
2100 if (Abc_TtCompareRev(pBest, pCopy, nWords) == 1)
2101 Abc_TgManCopy(&tgManBest, pBest, &tgManCopy), Config = 7;
2102 // PXY
2103 // 101
2104 Abc_TgFlipSymGroup(&tgManCopy, idx);
2105 CheckConfig(&tgManCopy);
2106 if (Abc_TtCompareRev(pBest, pCopy, nWords) == 1)
2107 Abc_TgManCopy(&tgManBest, pBest, &tgManCopy), Config = 5;
2108 // PXY
2109 // 100
2110 Abc_TgFlipSymGroup(&tgManCopy, idx + 1);
2111 CheckConfig(&tgManCopy);
2112 if (Abc_TtCompareRev(pBest, pCopy, nWords) == 1)
2113 Abc_TgManCopy(&tgManBest, pBest, &tgManCopy), Config = 4;
2114 // PXY
2115 // 000
2116 Abc_TgSwapAdjacentSymGroups(&tgManCopy, idx);
2117 CheckConfig(&tgManCopy);
2118 assert(Abc_TtEqual(pTruth, pCopy, nWords));
2119 if (Config == 0)
2120 return 0;
2121 assert(Abc_TtCompareRev(pTruth, pBest, nWords) == 1);
2122 Abc_TgManCopy(pMan, pTruth, &tgManBest);
2123 return Config;
2124 }
2125
Abc_TgPermPhase(Abc_TgMan_t * pMan,int iVar)2126 static int Abc_TgPermPhase(Abc_TgMan_t* pMan, int iVar)
2127 {
2128 static word pCopy[1024];
2129 int nWords = Abc_TtWordNum(pMan->nVars);
2130 int ivp = pMan->pPermTRev[iVar];
2131 Abc_TtCopy(pCopy, pMan->pTruth, nWords, 0);
2132 Abc_TtFlip(pCopy, nWords, ivp);
2133 if (Abc_TtCompareRev(pMan->pTruth, pCopy, nWords) == 1)
2134 {
2135 Abc_TtCopy(pMan->pTruth, pCopy, nWords, 0);
2136 pMan->uPhase ^= 1 << ivp;
2137 return 16;
2138 }
2139 return 0;
2140 }
2141
Abc_TgSimpleEnumeration(Abc_TgMan_t * pMan)2142 static void Abc_TgSimpleEnumeration(Abc_TgMan_t * pMan)
2143 {
2144 int i, j, k;
2145 int pGid[16];
2146
2147 for (k = j = 0; j < pMan->nGroups; j++)
2148 for (i = 0; i < pMan->pGroup[j].nGVars; i++, k++)
2149 pGid[k] = j;
2150 assert(k == pMan->nGVars);
2151
2152 for (k = 0; k < 5; k++)
2153 {
2154 int fChanges = 0;
2155 for (i = pMan->nGVars - 2; i >= 0; i--)
2156 if (pGid[i] == pGid[i + 1])
2157 fChanges |= Abc_TgSymGroupPerm(pMan, i, pGid[i] > 0 || pMan->fPhased);
2158 for (i = 1; i < pMan->nGVars - 1; i++)
2159 if (pGid[i] == pGid[i + 1])
2160 fChanges |= Abc_TgSymGroupPerm(pMan, i, pGid[i] > 0 || pMan->fPhased);
2161
2162 for (i = pMan->nVars - 1; i >= 0; i--)
2163 if (pMan->symPhase[i])
2164 fChanges |= Abc_TgPermPhase(pMan, i);
2165 for (i = 1; i < pMan->nVars; i++)
2166 if (pMan->symPhase[i])
2167 fChanges |= Abc_TgPermPhase(pMan, i);
2168 if (!fChanges) break;
2169 }
2170 assert(Abc_TgCannonVerify(pMan));
2171 }
2172
2173 /**Function*************************************************************
2174
2175 Synopsis [Exact canonical form computation.]
2176
2177 Description [full config enumeration]
2178
2179 SideEffects []
2180
2181 SeeAlso []
2182
2183 ***********************************************************************/
2184
Abc_TgIsInitPerm(char * pData,signed char * pDir,int size)2185 static int Abc_TgIsInitPerm(char * pData, signed char * pDir, int size)
2186 {
2187 int i;
2188 if (pDir[0] != -1) return 0;
2189 for (i = 1; i < size; i++)
2190 if (pDir[i] != -1 || pData[i] < pData[i - 1])
2191 return 0;
2192 return 1;
2193 }
2194
Abc_TgFirstPermutation(Abc_TgMan_t * pMan)2195 static void Abc_TgFirstPermutation(Abc_TgMan_t * pMan)
2196 {
2197 int i;
2198 for (i = 0; i < pMan->nGVars; i++)
2199 pMan->pPermDir[i] = -1;
2200 #ifndef NDEBUG
2201 for (i = 0; i < pMan->nGroups; i++)
2202 {
2203 TiedGroup * pGrp = pMan->pGroup + i;
2204 int nGvars = pGrp->nGVars;
2205 char * pVars = pMan->pPerm + pGrp->iStart;
2206 signed char * pDirs = pMan->pPermDir + pGrp->iStart;
2207 assert(Abc_TgIsInitPerm(pVars, pDirs, nGvars));
2208 }
2209 #endif
2210 }
2211
Abc_TgNextPermutation(Abc_TgMan_t * pMan)2212 static int Abc_TgNextPermutation(Abc_TgMan_t * pMan)
2213 {
2214 int i, j, nGvars;
2215 TiedGroup * pGrp;
2216 char * pVars;
2217 signed char * pDirs;
2218 for (i = 0; i < pMan->nGroups; i++)
2219 {
2220 pGrp = pMan->pGroup + i;
2221 nGvars = pGrp->nGVars;
2222 if (nGvars == 1) continue;
2223 pVars = pMan->pPerm + pGrp->iStart;
2224 pDirs = pMan->pPermDir + pGrp->iStart;
2225 j = Abc_NextPermSwapC(pVars, pDirs, nGvars);
2226 if (j >= 0)
2227 {
2228 Abc_TgSwapAdjacentSymGroups(pMan, j + pGrp->iStart);
2229 return 1;
2230 }
2231 Abc_TgSwapAdjacentSymGroups(pMan, pGrp->iStart);
2232 assert(Abc_TgIsInitPerm(pVars, pDirs, nGvars));
2233 }
2234 return 0;
2235 }
2236
grayCode(unsigned a)2237 static inline unsigned grayCode(unsigned a) { return a ^ (a >> 1); }
2238
grayFlip(unsigned a)2239 static int grayFlip(unsigned a)
2240 {
2241 int i;
2242 for (i = 0, a++; ; i++)
2243 if (a & (1 << i)) return i;
2244 }
2245
Abc_TgSaveBest(Abc_TgMan_t * pMan,Abc_TgMan_t * pBest)2246 static inline void Abc_TgSaveBest(Abc_TgMan_t * pMan, Abc_TgMan_t * pBest)
2247 {
2248 if (Abc_TtCompareRev(pBest->pTruth, pMan->pTruth, Abc_TtWordNum(pMan->nVars)) == 1)
2249 Abc_TgManCopy(pBest, pBest->pTruth, pMan);
2250 }
2251
Abc_TgPhaseEnumeration(Abc_TgMan_t * pMan,Abc_TgMan_t * pBest)2252 static void Abc_TgPhaseEnumeration(Abc_TgMan_t * pMan, Abc_TgMan_t * pBest)
2253 {
2254 char pFGrps[16];
2255 int i, j, n = pMan->pGroup->nGVars;
2256
2257 Abc_TgSaveBest(pMan, pBest);
2258 if (pMan->fPhased) return;
2259
2260 // sort by symPhase
2261 for (i = 0; i < n; i++)
2262 {
2263 char iv = pMan->pPerm[i];
2264 for (j = i; j > 0 && pMan->symPhase[(int)pFGrps[j-1]] > pMan->symPhase[(int)iv]; j--)
2265 pFGrps[j] = pFGrps[j - 1];
2266 pFGrps[j] = iv;
2267 }
2268
2269 for (i = 0; i < (1 << n) - 1; i++)
2270 {
2271 Abc_TgFlipSymGroupByVar(pMan, pFGrps[grayFlip(i)]);
2272 Abc_TgSaveBest(pMan, pBest);
2273 }
2274 }
2275
2276 /**Function*************************************************************
2277
2278 Synopsis [Hybrid exact canonical form computation.]
2279
2280 Description []
2281
2282 SideEffects []
2283
2284 SeeAlso []
2285
2286 ***********************************************************************/
Abc_TgCalcScc(Abc_TgMan_t * pMan,int * pOut,int fSort)2287 static void Abc_TgCalcScc(Abc_TgMan_t * pMan, int * pOut, int fSort)
2288 {
2289 int i, j, k;
2290 TiedGroup * pGrp;
2291
2292 Abc_TtSccInCofs(pMan->pTruth, pMan->nVars, pOut);
2293
2294 for (i = j = 0; j < pMan->nGVars; j++)
2295 {
2296 pOut[j] = pOut[i];
2297 for (k = pMan->pPerm[j]; k >= 0; k = pMan->symLink[k])
2298 {
2299 i++;
2300 assert(pMan->symLink[k] < 0 || pOut[j] == pOut[i]);
2301 }
2302 }
2303 if (!fSort) return;
2304
2305 for (pGrp = pMan->pGroup; pGrp < pMan->pGroup + pMan->nGroups; pGrp++)
2306 {
2307 int vb = pGrp->iStart, ve = vb + pGrp->nGVars;
2308 for (i = vb + 1; i < ve; i++)
2309 {
2310 int a = pOut[i];
2311 for (j = i; j > vb && pOut[j - 1] > a; j--)
2312 pOut[j] = pOut[j - 1];
2313 pOut[j] = a;
2314 }
2315 }
2316 }
2317
Abc_TgSplitGroupsByScc(Abc_TgMan_t * pMan)2318 static void Abc_TgSplitGroupsByScc(Abc_TgMan_t * pMan)
2319 {
2320 int pScc[16];
2321 char pPermT[16];
2322 TiedGroup * pGrp;
2323
2324 Abc_TgCalcScc(pMan, pScc, 0);
2325 for (pGrp = pMan->pGroup; pGrp < pMan->pGroup + pMan->nGroups; pGrp++)
2326 pGrp += Abc_TgSplitGroup(pMan, pGrp, pScc + pGrp->iStart);
2327
2328 Abc_TgExpendSymmetry(pMan, pPermT);
2329 Abc_TgImplementPerm(pMan, pPermT);
2330 assert(Abc_TgCannonVerify(pMan));
2331 }
2332
Abc_TgCompareCoef(int * pIn1,int * pIn2,int n)2333 static int Abc_TgCompareCoef(int * pIn1, int * pIn2, int n)
2334 {
2335 int i;
2336 for (i = 0; i < n; i++)
2337 if (pIn1[i] != pIn2[i])
2338 return (pIn1[i] < pIn2[i]) ? -1 : 1;
2339 return 0;
2340 }
2341
2342 // log2(n!)*100
2343 static const int log2fn[17] = { 0, 0, 100, 258, 458, 691, 949, 1230, 1530, 1847, 2179, 2525, 2884, 3254, 3634, 4025, 4425 };
Abc_TgPermCostScc(Abc_TgMan_t * pMan,int * pScc)2344 static int Abc_TgPermCostScc(Abc_TgMan_t * pMan, int *pScc)
2345 {
2346 int i, j, k, cost = 0;
2347
2348 for (i = k = 0; i < pMan->nGroups; i++)
2349 {
2350 int n = pMan->pGroup[i].nGVars;
2351 int d = 1;
2352 for (j = 1, k++; j < n; j++, k++)
2353 if (pScc[k] == pScc[k - 1]) d++;
2354 else {
2355 cost += log2fn[d];
2356 d = 1;
2357 }
2358 cost += log2fn[d];
2359 }
2360 return cost;
2361 }
2362
Abc_TgPermEnumerationScc(Abc_TgMan_t * pMan,Abc_TgMan_t * pBest)2363 static void Abc_TgPermEnumerationScc(Abc_TgMan_t * pMan, Abc_TgMan_t * pBest)
2364 {
2365 static word pCopy[1024];
2366 Abc_TgMan_t tgManCopy;
2367 Abc_TgManCopy(&tgManCopy, pCopy, pMan);
2368 if (pMan->nAlgorithm > 1)
2369 Abc_TgSplitGroupsByScc(&tgManCopy);
2370 Abc_TgFirstPermutation(&tgManCopy);
2371 do {
2372 Abc_TgSaveBest(&tgManCopy, pBest);
2373 } while (Abc_TgNextPermutation(&tgManCopy));
2374 }
2375
Abc_TgReorderFGrps(Abc_TgMan_t * pMan)2376 static void Abc_TgReorderFGrps(Abc_TgMan_t * pMan)
2377 {
2378 char * pFGrps = pMan->pFGrps;
2379 int i, j, n = pMan->fPhased ? 0 : pMan->pGroup->nGVars;
2380
2381 // sort by symPhase
2382 for (i = 0; i < n; i++)
2383 {
2384 char iv = pMan->pPerm[i];
2385 for (j = i; j > 0 && pMan->symPhase[(int)pFGrps[j - 1]] > pMan->symPhase[(int)iv]; j--)
2386 pFGrps[j] = pFGrps[j - 1];
2387 pFGrps[j] = iv;
2388 }
2389 }
2390
ilog2(int n)2391 static int ilog2(int n)
2392 {
2393 int i;
2394 for (i = 0; n /= 2; i++)
2395 ;
2396 return i;
2397 }
2398
2399 typedef struct Abc_SccCost_t_ {
2400 int cNeg, cPhase, cPerm;
2401 } Abc_SccCost_t;
2402
Abc_TgRecordPhase(Abc_TgMan_t * pMan,int mode)2403 static Abc_SccCost_t Abc_TgRecordPhase(Abc_TgMan_t * pMan, int mode)
2404 {
2405 Vec_Int_t * vPhase = pMan->vPhase;
2406 int i, j, n = pMan->pGroup->nGVars;
2407 int nStart = mode == 0 ? 1 : 0;
2408 int nCoefs = pMan->nGVars + 2 - nStart;
2409 int pScc[18], pMinScc[18];
2410 Abc_SccCost_t ret;
2411
2412 if (pMan->fPhased)
2413 {
2414 ret.cNeg = 0;
2415 ret.cPhase = 0;
2416 Abc_TgCalcScc(pMan, pScc + 2, 1);
2417 ret.cPerm = Abc_TgPermCostScc(pMan, pScc + 2);
2418 return ret;
2419 }
2420
2421 Abc_TgReorderFGrps(pMan);
2422 pMinScc[1] = Abc_TtScc(pMan->pTruth, pMan->nVars);
2423 Abc_TgCalcScc(pMan, pMinScc + 2, 1);
2424 pMinScc[0] = mode == 0 ? 0 : Abc_TgPermCostScc(pMan, pMinScc + 2);
2425 Vec_IntPush(vPhase, 0);
2426 for (i = 0; (j = grayFlip(i)) < n; i++)
2427 {
2428 Abc_TgFlipSymGroupByVar(pMan, pMan->pFGrps[j]);
2429 pScc[1] = Abc_TtScc(pMan->pTruth, pMan->nVars);
2430 if (mode == 0 && pScc[1] > pMinScc[1]) continue;
2431 Abc_TgCalcScc(pMan, pScc + 2, 1);
2432 if (mode > 0)
2433 pScc[0] = Abc_TgPermCostScc(pMan, pScc + 2);
2434 if (Abc_TgCompareCoef(pScc + nStart, pMinScc + nStart, nCoefs) < 0)
2435 {
2436 memcpy(pMinScc + nStart, pScc + nStart, nCoefs * sizeof(int));
2437 Vec_IntClear(vPhase);
2438 }
2439 if (Abc_TgCompareCoef(pScc + nStart, pMinScc + nStart, nCoefs) == 0)
2440 Vec_IntPush(vPhase, grayCode(i+1));
2441 }
2442 Abc_TgFlipSymGroupByVar(pMan, pMan->pFGrps[n - 1]);
2443
2444 ret.cNeg = n;
2445 ret.cPhase = ilog2(Vec_IntSize(vPhase));
2446 ret.cPerm = Abc_TgPermCostScc(pMan, pMinScc + 2);
2447 return ret;
2448 }
2449
Abc_TgRecordPhase1(Abc_TgMan_t * pMan)2450 static int Abc_TgRecordPhase1(Abc_TgMan_t * pMan) // for AdjSE
2451 {
2452 Vec_Int_t * vPhase = pMan->vPhase;
2453 int i, j, n = pMan->pGroup->nGVars;
2454 //int nCoefs = pMan->nGVars + 2;
2455 int nScc, nMinScc;
2456
2457 assert (Vec_IntSize(vPhase) == 0);
2458 if (pMan->fPhased) return 0;
2459
2460 Abc_TgReorderFGrps(pMan);
2461 nMinScc = Abc_TtScc(pMan->pTruth, pMan->nVars);
2462 Vec_IntPush(vPhase, 0);
2463 for (i = 0; (j = grayFlip(i)) < n; i++)
2464 {
2465 Abc_TgFlipSymGroupByVar(pMan, pMan->pFGrps[j]);
2466 nScc = Abc_TtScc(pMan->pTruth, pMan->nVars);
2467 if (nScc > nMinScc) continue;
2468 if (nScc < nMinScc)
2469 {
2470 nMinScc = nScc;
2471 Vec_IntClear(vPhase);
2472 }
2473 Vec_IntPush(vPhase, grayCode(i + 1));
2474 }
2475
2476 Abc_TgFlipSymGroupByVar(pMan, pMan->pFGrps[n - 1]);
2477 return ilog2(Vec_IntSize(vPhase));
2478 }
2479
Abc_TgPhaseEnumerationScc(Abc_TgMan_t * pMan,Abc_TgMan_t * pBest)2480 static void Abc_TgPhaseEnumerationScc(Abc_TgMan_t * pMan, Abc_TgMan_t * pBest)
2481 {
2482 Vec_Int_t * vPhase = pMan->vPhase;
2483 int i, j, n = pMan->pGroup->nGVars;
2484 int ph0 = 0, ph, flp;
2485 static word pCopy[1024];
2486 Abc_TgMan_t tgManCopy;
2487
2488 if (pMan->fPhased)
2489 {
2490 Abc_TgPermEnumerationScc(pMan, pBest);
2491 return;
2492 }
2493
2494 Abc_TgManCopy(&tgManCopy, pCopy, pMan);
2495 Vec_IntForEachEntry(vPhase, ph, i)
2496 {
2497 flp = ph ^ ph0;
2498 for (j = 0; j < n; j++)
2499 if (flp & (1 << j))
2500 Abc_TgFlipSymGroupByVar(&tgManCopy, pMan->pFGrps[j]);
2501 ph0 = ph;
2502 Abc_TgPermEnumerationScc(&tgManCopy, pBest);
2503 }
2504 }
2505
Abc_TgFullEnumeration(Abc_TgMan_t * pWork,Abc_TgMan_t * pBest)2506 static void Abc_TgFullEnumeration(Abc_TgMan_t * pWork, Abc_TgMan_t * pBest)
2507 {
2508 if (pWork->nAlgorithm > 0)
2509 {
2510 Abc_TtFill(pBest->pTruth, Abc_TtWordNum(pBest->nVars));
2511 Abc_TgPhaseEnumerationScc(pWork, pBest);
2512 }
2513 else
2514 {
2515 Abc_TgFirstPermutation(pWork);
2516 do Abc_TgPhaseEnumeration(pWork, pBest);
2517 while (Abc_TgNextPermutation(pWork));
2518 }
2519 pBest->uPhase |= 1 << 30;
2520 }
2521
2522 // runtime cost for Abc_TgRecordPhase (mode = 1)
Abc_SccPhaseCost(Abc_TgMan_t * pMan)2523 static inline double Abc_SccPhaseCost(Abc_TgMan_t * pMan)
2524 {
2525 return pMan->nVars * 0.997 + pMan->nGVars * 1.043 - 15.9;
2526 }
2527
2528 // runtime cost for Abc_TgFullEnumeration
Abc_SccEnumCost(Abc_TgMan_t * pMan,Abc_SccCost_t c)2529 static inline double Abc_SccEnumCost(Abc_TgMan_t * pMan, Abc_SccCost_t c)
2530 {
2531 switch (pMan->nAlgorithm)
2532 {
2533 case 0: return pMan->nVars + c.cPhase * 1.09 + c.cPerm * 0.01144;
2534 case 1: return pMan->nVars + c.cPhase * 0.855 + c.cPerm * 0.00797;
2535 case 2: return pMan->nVars * 0.94 + c.cPhase * 0.885 + c.cPerm * 0.00855 - 20.59;
2536 }
2537 return 0;
2538 }
2539
Abc_TgEnumerationCost(Abc_TgMan_t * pMan)2540 static int Abc_TgEnumerationCost(Abc_TgMan_t * pMan)
2541 {
2542 int i;
2543 Abc_SccCost_t c = { 0,0,0 };
2544 if (pMan->nGroups == 0) return 0;
2545
2546 for (i = 0; i < pMan->nGroups; i++)
2547 c.cPerm += log2fn[(int)pMan->pGroup[i].nGVars];
2548
2549 c.cPhase = pMan->fPhased ? 0
2550 : pMan->nAlgorithm == 0 ? pMan->pGroup->nGVars
2551 : Abc_TgRecordPhase1(pMan);
2552
2553 // coefficients computed by linear regression
2554 return Abc_SccEnumCost(pMan, c) + 0.5;
2555 }
2556
2557 /**Function*************************************************************
2558
2559 Synopsis [Adaptive heuristic/exact canonical form computation.]
2560
2561 Description []
2562
2563 SideEffects []
2564
2565 SeeAlso []
2566
2567 ***********************************************************************/
Abc_TtCanonicizeAda(Abc_TtHieMan_t * p,word * pTruth,int nVars,char * pCanonPerm,int iThres)2568 unsigned Abc_TtCanonicizeAda(Abc_TtHieMan_t * p, word * pTruth, int nVars, char * pCanonPerm, int iThres)
2569 {
2570 int nWords = Abc_TtWordNum(nVars);
2571 unsigned fExac = 0, fHash = 1 << 29;
2572 static word pCopy[1024];
2573 Abc_TgMan_t tgMan, tgManCopy;
2574 int iCost;
2575 const int MaxCost = 84; // maximun posible cost for function with 16 inputs
2576 const int nAlg = iThres >= 1000 ? 1 : 0;
2577 const int fHigh = (iThres % 1000) >= 100, nEnumThres = iThres % 100;
2578
2579 // handle constant
2580 if ( nVars == 0 ) {
2581 Abc_TtClear( pTruth, nWords );
2582 return 0;
2583 }
2584
2585 Abc_TtVerifySmallTruth(pTruth, nVars);
2586 #ifdef CANON_VERIFY
2587 Abc_TtCopy(gpVerCopy, pTruth, nWords, 0);
2588 #endif
2589
2590 assert(nVars <= 16);
2591 assert(!(nAlg && p == NULL));
2592 if (p && Abc_TtHieRetrieveOrInsert(p, -5, pTruth, pTruth) > 0) return fHash;
2593 Abc_TgInitMan(&tgMan, pTruth, nVars, nAlg, p ? p->vPhase : NULL);
2594 Abc_TgCreateGroups(&tgMan);
2595 if (p && Abc_TtHieRetrieveOrInsert(p, -4, pTruth, pTruth) > 0) return fHash;
2596 Abc_TgPurgeSymmetry(&tgMan, fHigh);
2597
2598 Abc_TgExpendSymmetry(&tgMan, pCanonPerm);
2599 Abc_TgImplementPerm(&tgMan, pCanonPerm);
2600 assert(Abc_TgCannonVerify(&tgMan));
2601
2602 iCost = Abc_TgEnumerationCost(&tgMan);
2603 if (p == NULL || p->nLastLevel == 0) {
2604 if (nEnumThres > MaxCost || iCost < nEnumThres) {
2605 Abc_TgManCopy(&tgManCopy, pCopy, &tgMan);
2606 Abc_TgFullEnumeration(&tgManCopy, &tgMan);
2607 }
2608 else
2609 Abc_TgSimpleEnumeration(&tgMan);
2610 }
2611 else {
2612 if (nEnumThres > MaxCost || iCost < nEnumThres) fExac = 1 << 30;
2613 if (Abc_TtHieRetrieveOrInsert(p, -3, pTruth, pTruth) > 0) return fHash + fExac;
2614 Abc_TgManCopy(&tgManCopy, pCopy, &tgMan);
2615 Abc_TgSimpleEnumeration(&tgMan);
2616 if (Abc_TtHieRetrieveOrInsert(p, -2, pTruth, pTruth) > 0) return fHash + fExac;
2617 if (fExac) {
2618 Abc_TgManCopy(&tgMan, pTruth, &tgManCopy);
2619 Abc_TgFullEnumeration(&tgManCopy, &tgMan);
2620 }
2621 Abc_TtHieRetrieveOrInsert(p, -1, pTruth, pTruth);
2622 }
2623 memcpy(pCanonPerm, tgMan.pPermT, sizeof(char) * nVars);
2624
2625 #ifdef CANON_VERIFY
2626 if (!Abc_TgCannonVerify(&tgMan))
2627 printf("Canonical form verification failed!\n");
2628 #endif
2629 return tgMan.uPhase;
2630 }
2631
Abc_TtCanonicizeCA(Abc_TtHieMan_t * p,word * pTruth,int nVars,char * pCanonPerm,int fCA)2632 unsigned Abc_TtCanonicizeCA(Abc_TtHieMan_t * p, word * pTruth, int nVars, char * pCanonPerm, int fCA)
2633 {
2634 int nWords = Abc_TtWordNum(nVars);
2635 unsigned fHard = 0, fHash = 1 << 29;
2636 static word pCopy[1024];
2637 Abc_TgMan_t tgMan, tgManCopy;
2638 Abc_SccCost_t sc;
2639
2640 // handle constant
2641 if (nVars == 0) {
2642 Abc_TtClear(pTruth, nWords);
2643 return 0;
2644 }
2645
2646 Abc_TtVerifySmallTruth(pTruth, nVars);
2647 #ifdef CANON_VERIFY
2648 Abc_TtCopy(gpVerCopy, pTruth, nWords, 0);
2649 #endif
2650
2651 assert(nVars <= 16);
2652 assert(p != NULL);
2653 if (Abc_TtHieRetrieveOrInsert(p, -5, pTruth, pTruth) > 0) return fHash;
2654 Abc_TgInitMan(&tgMan, pTruth, nVars, 2, p->vPhase);
2655
2656 Abc_TgCreateGroups(&tgMan);
2657 if (p && Abc_TtHieRetrieveOrInsert(p, -4, pTruth, pTruth) > 0) return fHash;
2658 Abc_TgPurgeSymmetry(&tgMan, 1);
2659
2660 Abc_TgExpendSymmetry(&tgMan, pCanonPerm);
2661 Abc_TgImplementPerm(&tgMan, pCanonPerm);
2662 assert(Abc_TgCannonVerify(&tgMan));
2663
2664 if (Abc_TtHieRetrieveOrInsert(p, -3, pTruth, pTruth) > 0) return fHash;
2665 Abc_TgManCopy(&tgManCopy, pCopy, &tgMan);
2666 Abc_TgSimpleEnumeration(&tgMan);
2667 if (Abc_TtHieRetrieveOrInsert(p, -2, pTruth, pTruth) > 0) return fHash;
2668 Abc_TgManCopy(&tgMan, pTruth, &tgManCopy);
2669 Abc_TtFill(pTruth, nWords);
2670
2671 assert(Abc_TgCannonVerify(&tgManCopy));
2672 sc = Abc_TgRecordPhase(&tgManCopy, 0);
2673 if (fCA && Abc_SccEnumCost(&tgManCopy, sc) > Abc_SccPhaseCost(&tgManCopy))
2674 {
2675 Abc_TgResetGroup(&tgManCopy);
2676 sc = Abc_TgRecordPhase(&tgManCopy, 1);
2677 fHard = 1 << 28;
2678 }
2679 Abc_TgFullEnumeration(&tgManCopy, &tgMan);
2680 Abc_TtHieRetrieveOrInsert(p, -1, pTruth, pTruth);
2681 memcpy(pCanonPerm, tgMan.pPermT, sizeof(char) * nVars);
2682
2683 #ifdef CANON_VERIFY
2684 if (!Abc_TgCannonVerify(&tgMan))
2685 printf("Canonical form verification failed!\n");
2686 #endif
2687 return tgMan.uPhase | fHard;
2688 }
2689
2690
2691 ////////////////////////////////////////////////////////////////////////
2692 /// END OF FILE ///
2693 ////////////////////////////////////////////////////////////////////////
2694
2695
2696 ABC_NAMESPACE_IMPL_END
2697
2698