1 /**CFile****************************************************************
2
3 FileName [dauDsd.c]
4
5 SystemName [ABC: Logic synthesis and verification system.]
6
7 PackageName [DAG-aware unmapping.]
8
9 Synopsis [Disjoint-support decomposition.]
10
11 Author [Alan Mishchenko]
12
13 Affiliation [UC Berkeley]
14
15 Date [Ver. 1.0. Started - June 20, 2005.]
16
17 Revision [$Id: dauDsd.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
24 ABC_NAMESPACE_IMPL_START
25
26 ////////////////////////////////////////////////////////////////////////
27 /// DECLARATIONS ///
28 ////////////////////////////////////////////////////////////////////////
29
30 /*
31 This code performs truth-table-based decomposition for 6-variable functions.
32 Representation of operations:
33 ! = not;
34 (ab) = a and b;
35 [ab] = a xor b;
36 <abc> = ITE( a, b, c )
37 FUNCTION{abc} = FUNCTION( a, b, c )
38 */
39
40
41 ////////////////////////////////////////////////////////////////////////
42 /// FUNCTION DEFINITIONS ///
43 ////////////////////////////////////////////////////////////////////////
44
45 /**Function*************************************************************
46
47 Synopsis [Elementary truth tables.]
48
49 Description []
50
51 SideEffects []
52
53 SeeAlso []
54
55 ***********************************************************************/
Dau_DsdTtElems()56 static inline word ** Dau_DsdTtElems()
57 {
58 static word TtElems[DAU_MAX_VAR+1][DAU_MAX_WORD], * pTtElems[DAU_MAX_VAR+1] = {NULL};
59 if ( pTtElems[0] == NULL )
60 {
61 int v;
62 for ( v = 0; v <= DAU_MAX_VAR; v++ )
63 pTtElems[v] = TtElems[v];
64 Abc_TtElemInit( pTtElems, DAU_MAX_VAR );
65 }
66 return pTtElems;
67 }
68
69 /**Function*************************************************************
70
71 Synopsis [DSD formula manipulation.]
72
73 Description []
74
75 SideEffects []
76
77 SeeAlso []
78
79 ***********************************************************************/
Dau_DsdComputeMatches(char * p)80 int * Dau_DsdComputeMatches( char * p )
81 {
82 static int pMatches[DAU_MAX_STR];
83 int pNested[DAU_MAX_VAR];
84 int v, nNested = 0;
85 for ( v = 0; p[v]; v++ )
86 {
87 pMatches[v] = 0;
88 if ( p[v] == '(' || p[v] == '[' || p[v] == '<' || p[v] == '{' )
89 pNested[nNested++] = v;
90 else if ( p[v] == ')' || p[v] == ']' || p[v] == '>' || p[v] == '}' )
91 pMatches[pNested[--nNested]] = v;
92 assert( nNested < DAU_MAX_VAR );
93 }
94 assert( nNested == 0 );
95 return pMatches;
96 }
97
98 /**Function*************************************************************
99
100 Synopsis [Generate random permutation.]
101
102 Description []
103
104 SideEffects []
105
106 SeeAlso []
107
108 ***********************************************************************/
Dau_DsdFindVarNum(char * pDsd)109 int Dau_DsdFindVarNum( char * pDsd )
110 {
111 int vMax = 0;
112 pDsd--;
113 while ( *++pDsd )
114 if ( *pDsd >= 'a' && *pDsd <= 'z' )
115 vMax = Abc_MaxInt( vMax, *pDsd - 'a' );
116 return vMax + 1;
117 }
Dau_DsdGenRandPerm(int * pPerm,int nVars)118 void Dau_DsdGenRandPerm( int * pPerm, int nVars )
119 {
120 int v, vNew;
121 for ( v = 0; v < nVars; v++ )
122 pPerm[v] = v;
123 for ( v = 0; v < nVars; v++ )
124 {
125 vNew = rand() % nVars;
126 ABC_SWAP( int, pPerm[v], pPerm[vNew] );
127 }
128 }
Dau_DsdPermute(char * pDsd)129 void Dau_DsdPermute( char * pDsd )
130 {
131 int pPerm[16];
132 int nVars = Dau_DsdFindVarNum( pDsd );
133 Dau_DsdGenRandPerm( pPerm, nVars );
134 pDsd--;
135 while ( *++pDsd )
136 if ( *pDsd >= 'a' && *pDsd < 'a' + nVars )
137 *pDsd = 'a' + pPerm[*pDsd - 'a'];
138 }
139
140 /**Function*************************************************************
141
142 Synopsis [Normalize the ordering of components.]
143
144 Description []
145
146 SideEffects []
147
148 SeeAlso []
149
150 ***********************************************************************/
Dau_DsdNormalizeCopy(char * pDest,char * pSour,int * pMarks,int i)151 char * Dau_DsdNormalizeCopy( char * pDest, char * pSour, int * pMarks, int i )
152 {
153 int s;
154 for ( s = pMarks[i]; s < pMarks[i+1]; s++ )
155 *pDest++ = pSour[s];
156 return pDest;
157 }
Dau_DsdNormalizeCompare(char * pStr,int * pMarks,int i,int j)158 int Dau_DsdNormalizeCompare( char * pStr, int * pMarks, int i, int j )
159 {
160 char * pStr1 = pStr + pMarks[i];
161 char * pStr2 = pStr + pMarks[j];
162 char * pLimit1 = pStr + pMarks[i+1];
163 char * pLimit2 = pStr + pMarks[j+1];
164 for ( ; pStr1 < pLimit1 && pStr2 < pLimit2; pStr1++, pStr2++ )
165 {
166 if ( !(*pStr1 >= 'a' && *pStr1 <= 'z') )
167 {
168 pStr2--;
169 continue;
170 }
171 if ( !(*pStr2 >= 'a' && *pStr2 <= 'z') )
172 {
173 pStr1--;
174 continue;
175 }
176 if ( *pStr1 < *pStr2 )
177 return -1;
178 if ( *pStr1 > *pStr2 )
179 return 1;
180 }
181 assert( pStr1 < pLimit1 || pStr2 < pLimit2 );
182 if ( pStr1 == pLimit1 )
183 return -1;
184 if ( pStr2 == pLimit2 )
185 return 1;
186 assert( 0 );
187 return 0;
188 }
Dau_DsdNormalizePerm(char * pStr,int * pMarks,int nMarks)189 int * Dau_DsdNormalizePerm( char * pStr, int * pMarks, int nMarks )
190 {
191 static int pPerm[DAU_MAX_VAR];
192 int i, k;
193 for ( i = 0; i < nMarks; i++ )
194 pPerm[i] = i;
195 for ( i = 0; i < nMarks; i++ )
196 {
197 int iBest = i;
198 for ( k = i + 1; k < nMarks; k++ )
199 if ( Dau_DsdNormalizeCompare( pStr, pMarks, pPerm[iBest], pPerm[k] ) == 1 )
200 iBest = k;
201 ABC_SWAP( int, pPerm[i], pPerm[iBest] );
202 }
203 return pPerm;
204 }
Dau_DsdNormalize_rec(char * pStr,char ** p,int * pMatches)205 void Dau_DsdNormalize_rec( char * pStr, char ** p, int * pMatches )
206 {
207 static char pBuffer[DAU_MAX_STR];
208 if ( **p == '!' )
209 (*p)++;
210 while ( (**p >= 'A' && **p <= 'F') || (**p >= '0' && **p <= '9') )
211 (*p)++;
212 if ( **p == '<' )
213 {
214 char * q = pStr + pMatches[*p - pStr];
215 if ( *(q+1) == '{' )
216 *p = q+1;
217 }
218 if ( **p >= 'a' && **p <= 'z' ) // var
219 return;
220 if ( **p == '(' || **p == '[' ) // and/or/xor
221 {
222 char * pStore, * pOld = *p + 1;
223 char * q = pStr + pMatches[ *p - pStr ];
224 int i, * pPerm, nMarks = 0, pMarks[DAU_MAX_VAR+1];
225 assert( *q == **p + 1 + (**p != '(') );
226 for ( (*p)++; *p < q; (*p)++ )
227 {
228 pMarks[nMarks++] = *p - pStr;
229 Dau_DsdNormalize_rec( pStr, p, pMatches );
230 }
231 pMarks[nMarks] = *p - pStr;
232 assert( *p == q );
233 // add to buffer in good order
234 pPerm = Dau_DsdNormalizePerm( pStr, pMarks, nMarks );
235 // copy to the buffer
236 pStore = pBuffer;
237 for ( i = 0; i < nMarks; i++ )
238 pStore = Dau_DsdNormalizeCopy( pStore, pStr, pMarks, pPerm[i] );
239 assert( pStore - pBuffer == *p - pOld );
240 memcpy( pOld, pBuffer, (size_t)(pStore - pBuffer) );
241 return;
242 }
243 if ( **p == '<' || **p == '{' ) // mux
244 {
245 char * q = pStr + pMatches[ *p - pStr ];
246 assert( *q == **p + 1 + (**p != '(') );
247 if ( (**p == '<') && (*(q+1) == '{') )
248 {
249 *p = q+1;
250 Dau_DsdNormalize_rec( pStr, p, pMatches );
251 return;
252 }
253 for ( (*p)++; *p < q; (*p)++ )
254 Dau_DsdNormalize_rec( pStr, p, pMatches );
255 assert( *p == q );
256 return;
257 }
258 assert( 0 );
259 }
Dau_DsdNormalize(char * pDsd)260 void Dau_DsdNormalize( char * pDsd )
261 {
262 if ( pDsd[1] != 0 )
263 Dau_DsdNormalize_rec( pDsd, &pDsd, Dau_DsdComputeMatches(pDsd) );
264 }
265
266
267
268 /**Function*************************************************************
269
270 Synopsis []
271
272 Description []
273
274 SideEffects []
275
276 SeeAlso []
277
278 ***********************************************************************/
Dau_DsdCountAnds_rec(char * pStr,char ** p,int * pMatches)279 int Dau_DsdCountAnds_rec( char * pStr, char ** p, int * pMatches )
280 {
281 if ( **p == '!' )
282 (*p)++;
283 while ( (**p >= 'A' && **p <= 'F') || (**p >= '0' && **p <= '9') )
284 (*p)++;
285 if ( **p == '<' )
286 {
287 char * q = pStr + pMatches[*p - pStr];
288 if ( *(q+1) == '{' )
289 *p = q+1;
290 }
291 if ( **p >= 'a' && **p <= 'z' ) // var
292 return 0;
293 if ( **p == '(' || **p == '[' ) // and/or/xor
294 {
295 int Counter = 0, AddOn = (**p == '(')? 1 : 3;
296 char * q = pStr + pMatches[ *p - pStr ];
297 assert( *q == **p + 1 + (**p != '(') );
298 for ( (*p)++; *p < q; (*p)++ )
299 Counter += AddOn + Dau_DsdCountAnds_rec( pStr, p, pMatches );
300 assert( *p == q );
301 return Counter - AddOn;
302 }
303 if ( **p == '<' || **p == '{' ) // mux
304 {
305 int Counter = 3;
306 char * q = pStr + pMatches[ *p - pStr ];
307 assert( *q == **p + 1 + (**p != '(') );
308 for ( (*p)++; *p < q; (*p)++ )
309 Counter += Dau_DsdCountAnds_rec( pStr, p, pMatches );
310 assert( *p == q );
311 return Counter;
312 }
313 assert( 0 );
314 return 0;
315 }
Dau_DsdCountAnds(char * pDsd)316 int Dau_DsdCountAnds( char * pDsd )
317 {
318 if ( pDsd[1] == 0 )
319 return 0;
320 return Dau_DsdCountAnds_rec( pDsd, &pDsd, Dau_DsdComputeMatches(pDsd) );
321 }
322
323 /**Function*************************************************************
324
325 Synopsis [Computes truth table for the DSD formula.]
326
327 Description []
328
329 SideEffects []
330
331 SeeAlso []
332
333 ***********************************************************************/
Dau_Dsd6TruthCompose_rec(word Func,word * pFanins,int nVars)334 word Dau_Dsd6TruthCompose_rec( word Func, word * pFanins, int nVars )
335 {
336 word t0, t1;
337 if ( Func == 0 )
338 return 0;
339 if ( Func == ~(word)0 )
340 return ~(word)0;
341 assert( nVars > 0 );
342 if ( --nVars == 0 )
343 {
344 assert( Func == s_Truths6[0] || Func == s_Truths6Neg[0] );
345 return (Func == s_Truths6[0]) ? pFanins[0] : ~pFanins[0];
346 }
347 if ( !Abc_Tt6HasVar(Func, nVars) )
348 return Dau_Dsd6TruthCompose_rec( Func, pFanins, nVars );
349 t0 = Dau_Dsd6TruthCompose_rec( Abc_Tt6Cofactor0(Func, nVars), pFanins, nVars );
350 t1 = Dau_Dsd6TruthCompose_rec( Abc_Tt6Cofactor1(Func, nVars), pFanins, nVars );
351 return (~pFanins[nVars] & t0) | (pFanins[nVars] & t1);
352 }
Dau_Dsd6ToTruth_rec(char * pStr,char ** p,int * pMatches,word * pTruths)353 word Dau_Dsd6ToTruth_rec( char * pStr, char ** p, int * pMatches, word * pTruths )
354 {
355 int fCompl = 0;
356 if ( **p == '!' )
357 (*p)++, fCompl = 1;
358 if ( **p >= 'a' && **p <= 'f' ) // var
359 {
360 assert( **p - 'a' >= 0 && **p - 'a' < 6 );
361 return fCompl ? ~pTruths[**p - 'a'] : pTruths[**p - 'a'];
362 }
363 if ( **p == '(' ) // and/or
364 {
365 char * q = pStr + pMatches[ *p - pStr ];
366 word Res = ~(word)0;
367 assert( **p == '(' && *q == ')' );
368 for ( (*p)++; *p < q; (*p)++ )
369 Res &= Dau_Dsd6ToTruth_rec( pStr, p, pMatches, pTruths );
370 assert( *p == q );
371 return fCompl ? ~Res : Res;
372 }
373 if ( **p == '[' ) // xor
374 {
375 char * q = pStr + pMatches[ *p - pStr ];
376 word Res = 0;
377 assert( **p == '[' && *q == ']' );
378 for ( (*p)++; *p < q; (*p)++ )
379 Res ^= Dau_Dsd6ToTruth_rec( pStr, p, pMatches, pTruths );
380 assert( *p == q );
381 return fCompl ? ~Res : Res;
382 }
383 if ( **p == '<' ) // mux
384 {
385 int nVars = 0;
386 word Temp[3], * pTemp = Temp, Res;
387 word Fanins[6], * pTruths2;
388 char * pOld = *p;
389 char * q = pStr + pMatches[ *p - pStr ];
390 // read fanins
391 if ( *(q+1) == '{' )
392 {
393 char * q2;
394 *p = q+1;
395 q2 = pStr + pMatches[ *p - pStr ];
396 assert( **p == '{' && *q2 == '}' );
397 for ( nVars = 0, (*p)++; *p < q2; (*p)++, nVars++ )
398 Fanins[nVars] = Dau_Dsd6ToTruth_rec( pStr, p, pMatches, pTruths );
399 assert( *p == q2 );
400 pTruths2 = Fanins;
401 }
402 else
403 pTruths2 = pTruths;
404 // read MUX
405 *p = pOld;
406 q = pStr + pMatches[ *p - pStr ];
407 assert( **p == '<' && *q == '>' );
408 // verify internal variables
409 if ( nVars )
410 for ( ; pOld < q; pOld++ )
411 if ( *pOld >= 'a' && *pOld <= 'z' )
412 assert( *pOld - 'a' < nVars );
413 // derive MAX components
414 for ( (*p)++; *p < q; (*p)++ )
415 *pTemp++ = Dau_Dsd6ToTruth_rec( pStr, p, pMatches, pTruths2 );
416 assert( pTemp == Temp + 3 );
417 assert( *p == q );
418 if ( *(q+1) == '{' ) // and/or
419 {
420 char * q = pStr + pMatches[ ++(*p) - pStr ];
421 assert( **p == '{' && *q == '}' );
422 *p = q;
423 }
424 Res = (Temp[0] & Temp[1]) | (~Temp[0] & Temp[2]);
425 return fCompl ? ~Res : Res;
426 }
427 if ( (**p >= 'A' && **p <= 'F') || (**p >= '0' && **p <= '9') )
428 {
429 word Func, Fanins[6], Res;
430 char * q;
431 int i, nVars = Abc_TtReadHex( &Func, *p );
432 *p += Abc_TtHexDigitNum( nVars );
433 q = pStr + pMatches[ *p - pStr ];
434 assert( **p == '{' && *q == '}' );
435 for ( i = 0, (*p)++; *p < q; (*p)++, i++ )
436 Fanins[i] = Dau_Dsd6ToTruth_rec( pStr, p, pMatches, pTruths );
437 assert( i == nVars );
438 assert( *p == q );
439 Res = Dau_Dsd6TruthCompose_rec( Func, Fanins, nVars );
440 return fCompl ? ~Res : Res;
441 }
442 assert( 0 );
443 return 0;
444 }
Dau_Dsd6ToTruth(char * p)445 word Dau_Dsd6ToTruth( char * p )
446 {
447 word Res;
448 if ( *p == '0' && *(p+1) == 0 )
449 Res = 0;
450 else if ( *p == '1' && *(p+1) == 0 )
451 Res = ~(word)0;
452 else
453 Res = Dau_Dsd6ToTruth_rec( p, &p, Dau_DsdComputeMatches(p), s_Truths6 );
454 assert( *++p == 0 );
455 return Res;
456 }
457
458 /**Function*************************************************************
459
460 Synopsis [Computes truth table for the DSD formula.]
461
462 Description []
463
464 SideEffects []
465
466 SeeAlso []
467
468 ***********************************************************************/
Dau_DsdTruth6Compose_rec(word Func,word pFanins[DAU_MAX_VAR][DAU_MAX_WORD],word * pRes,int nVars,int nWordsR)469 void Dau_DsdTruth6Compose_rec( word Func, word pFanins[DAU_MAX_VAR][DAU_MAX_WORD], word * pRes, int nVars, int nWordsR )
470 {
471 if ( Func == 0 )
472 {
473 Abc_TtConst0( pRes, nWordsR );
474 return;
475 }
476 if ( Func == ~(word)0 )
477 {
478 Abc_TtConst1( pRes, nWordsR );
479 return;
480 }
481 assert( nVars > 0 );
482 if ( --nVars == 0 )
483 {
484 assert( Func == s_Truths6[0] || Func == s_Truths6Neg[0] );
485 Abc_TtCopy( pRes, pFanins[0], nWordsR, Func == s_Truths6Neg[0] );
486 return;
487 }
488 if ( !Abc_Tt6HasVar(Func, nVars) )
489 {
490 Dau_DsdTruth6Compose_rec( Func, pFanins, pRes, nVars, nWordsR );
491 return;
492 }
493 {
494 word pTtTemp[2][DAU_MAX_WORD];
495 Dau_DsdTruth6Compose_rec( Abc_Tt6Cofactor0(Func, nVars), pFanins, pTtTemp[0], nVars, nWordsR );
496 Dau_DsdTruth6Compose_rec( Abc_Tt6Cofactor1(Func, nVars), pFanins, pTtTemp[1], nVars, nWordsR );
497 Abc_TtMux( pRes, pFanins[nVars], pTtTemp[1], pTtTemp[0], nWordsR );
498 return;
499 }
500 }
Dau_DsdTruthCompose_rec(word * pFunc,word pFanins[DAU_MAX_VAR][DAU_MAX_WORD],word * pRes,int nVars,int nWordsR)501 void Dau_DsdTruthCompose_rec( word * pFunc, word pFanins[DAU_MAX_VAR][DAU_MAX_WORD], word * pRes, int nVars, int nWordsR )
502 {
503 int nWordsF;
504 if ( nVars <= 6 )
505 {
506 Dau_DsdTruth6Compose_rec( pFunc[0], pFanins, pRes, nVars, nWordsR );
507 return;
508 }
509 nWordsF = Abc_TtWordNum( nVars );
510 assert( nWordsF > 1 );
511 if ( Abc_TtIsConst0(pFunc, nWordsF) )
512 {
513 Abc_TtConst0( pRes, nWordsR );
514 return;
515 }
516 if ( Abc_TtIsConst1(pFunc, nWordsF) )
517 {
518 Abc_TtConst1( pRes, nWordsR );
519 return;
520 }
521 if ( !Abc_TtHasVar( pFunc, nVars, nVars-1 ) )
522 {
523 Dau_DsdTruthCompose_rec( pFunc, pFanins, pRes, nVars-1, nWordsR );
524 return;
525 }
526 {
527 word pTtTemp[2][DAU_MAX_WORD];
528 nVars--;
529 Dau_DsdTruthCompose_rec( pFunc, pFanins, pTtTemp[0], nVars, nWordsR );
530 Dau_DsdTruthCompose_rec( pFunc + nWordsF/2, pFanins, pTtTemp[1], nVars, nWordsR );
531 Abc_TtMux( pRes, pFanins[nVars], pTtTemp[1], pTtTemp[0], nWordsR );
532 return;
533 }
534 }
Dau_DsdToTruth_rec(char * pStr,char ** p,int * pMatches,word ** pTtElems,word * pRes,int nVars)535 void Dau_DsdToTruth_rec( char * pStr, char ** p, int * pMatches, word ** pTtElems, word * pRes, int nVars )
536 {
537 int nWords = Abc_TtWordNum( nVars );
538 int fCompl = 0;
539 if ( **p == '!' )
540 (*p)++, fCompl = 1;
541 if ( **p >= 'a' && **p <= 'z' ) // var
542 {
543 assert( **p - 'a' >= 0 && **p - 'a' < nVars );
544 Abc_TtCopy( pRes, pTtElems[**p - 'a'], nWords, fCompl );
545 return;
546 }
547 if ( **p == '(' ) // and/or
548 {
549 char * q = pStr + pMatches[ *p - pStr ];
550 word pTtTemp[DAU_MAX_WORD];
551 assert( **p == '(' && *q == ')' );
552 Abc_TtConst1( pRes, nWords );
553 for ( (*p)++; *p < q; (*p)++ )
554 {
555 Dau_DsdToTruth_rec( pStr, p, pMatches, pTtElems, pTtTemp, nVars );
556 Abc_TtAnd( pRes, pRes, pTtTemp, nWords, 0 );
557 }
558 assert( *p == q );
559 if ( fCompl ) Abc_TtNot( pRes, nWords );
560 return;
561 }
562 if ( **p == '[' ) // xor
563 {
564 char * q = pStr + pMatches[ *p - pStr ];
565 word pTtTemp[DAU_MAX_WORD];
566 assert( **p == '[' && *q == ']' );
567 Abc_TtConst0( pRes, nWords );
568 for ( (*p)++; *p < q; (*p)++ )
569 {
570 Dau_DsdToTruth_rec( pStr, p, pMatches, pTtElems, pTtTemp, nVars );
571 Abc_TtXor( pRes, pRes, pTtTemp, nWords, 0 );
572 }
573 assert( *p == q );
574 if ( fCompl ) Abc_TtNot( pRes, nWords );
575 return;
576 }
577 if ( **p == '<' ) // mux
578 {
579 char * q = pStr + pMatches[ *p - pStr ];
580 word pTtTemp[3][DAU_MAX_WORD];
581 int i;
582 assert( **p == '<' && *q == '>' );
583 for ( i = 0, (*p)++; *p < q; (*p)++, i++ )
584 Dau_DsdToTruth_rec( pStr, p, pMatches, pTtElems, pTtTemp[i], nVars );
585 assert( i == 3 );
586 Abc_TtMux( pRes, pTtTemp[0], pTtTemp[1], pTtTemp[2], nWords );
587 assert( *p == q );
588 if ( fCompl ) Abc_TtNot( pRes, nWords );
589 return;
590 }
591 if ( (**p >= 'A' && **p <= 'F') || (**p >= '0' && **p <= '9') )
592 {
593 word pFanins[DAU_MAX_VAR][DAU_MAX_WORD], pFunc[DAU_MAX_WORD];
594 char * q;
595 int i, nVarsF = Abc_TtReadHex( pFunc, *p );
596 *p += Abc_TtHexDigitNum( nVarsF );
597 q = pStr + pMatches[ *p - pStr ];
598 assert( **p == '{' && *q == '}' );
599 for ( i = 0, (*p)++; *p < q; (*p)++, i++ )
600 Dau_DsdToTruth_rec( pStr, p, pMatches, pTtElems, pFanins[i], nVars );
601 assert( i == nVarsF );
602 assert( *p == q );
603 Dau_DsdTruthCompose_rec( pFunc, pFanins, pRes, nVarsF, nWords );
604 if ( fCompl ) Abc_TtNot( pRes, nWords );
605 return;
606 }
607 assert( 0 );
608 }
Dau_DsdToTruth(char * p,int nVars)609 word * Dau_DsdToTruth( char * p, int nVars )
610 {
611 int nWords = Abc_TtWordNum( nVars );
612 word ** pTtElems = Dau_DsdTtElems();
613 word * pRes = pTtElems[DAU_MAX_VAR];
614 assert( nVars <= DAU_MAX_VAR );
615 if ( Dau_DsdIsConst0(p) )
616 Abc_TtConst0( pRes, nWords );
617 else if ( Dau_DsdIsConst1(p) )
618 Abc_TtConst1( pRes, nWords );
619 else
620 Dau_DsdToTruth_rec( p, &p, Dau_DsdComputeMatches(p), pTtElems, pRes, nVars );
621 assert( *++p == 0 );
622 return pRes;
623 }
624
625
626 /**Function*************************************************************
627
628 Synopsis []
629
630 Description []
631
632 SideEffects []
633
634 SeeAlso []
635
636 ***********************************************************************/
Dau_DsdTest2()637 void Dau_DsdTest2()
638 {
639 // char * p = Abc_UtilStrsav( "!(ab!(de[cf]))" );
640 // char * p = Abc_UtilStrsav( "!(a![d<ecf>]b)" );
641 // word t = Dau_Dsd6ToTruth( p );
642 }
643
644
645
646 /**Function*************************************************************
647
648 Synopsis [Performs DSD.]
649
650 Description []
651
652 SideEffects []
653
654 SeeAlso []
655
656 ***********************************************************************/
Dau_DsdPerformReplace(char * pBuffer,int PosStart,int Pos,int Symb,char * pNext)657 static inline int Dau_DsdPerformReplace( char * pBuffer, int PosStart, int Pos, int Symb, char * pNext )
658 {
659 static char pTemp[DAU_MAX_STR];
660 char * pCur = pTemp;
661 int i, k, RetValue;
662 for ( i = PosStart; i < Pos; i++ )
663 if ( pBuffer[i] != Symb )
664 *pCur++ = pBuffer[i];
665 else
666 for ( k = 0; pNext[k]; k++ )
667 *pCur++ = pNext[k];
668 RetValue = PosStart + (pCur - pTemp);
669 for ( i = PosStart; i < RetValue; i++ )
670 pBuffer[i] = pTemp[i-PosStart];
671 return RetValue;
672 }
Dau_DsdPerform_rec(word t,char * pBuffer,int Pos,int * pVars,int nVars)673 int Dau_DsdPerform_rec( word t, char * pBuffer, int Pos, int * pVars, int nVars )
674 {
675 char pNest[10];
676 word Cof0[6], Cof1[6], Cof[4];
677 int pVarsNew[6], nVarsNew, PosStart;
678 int v, u, vBest, CountBest;
679 assert( Pos < DAU_MAX_STR );
680 // perform support minimization
681 nVarsNew = 0;
682 for ( v = 0; v < nVars; v++ )
683 if ( Abc_Tt6HasVar( t, pVars[v] ) )
684 pVarsNew[ nVarsNew++ ] = pVars[v];
685 assert( nVarsNew > 0 );
686 // special case when function is a var
687 if ( nVarsNew == 1 )
688 {
689 if ( t == s_Truths6[ pVarsNew[0] ] )
690 {
691 pBuffer[Pos++] = 'a' + pVarsNew[0];
692 return Pos;
693 }
694 if ( t == ~s_Truths6[ pVarsNew[0] ] )
695 {
696 pBuffer[Pos++] = '!';
697 pBuffer[Pos++] = 'a' + pVarsNew[0];
698 return Pos;
699 }
700 assert( 0 );
701 return Pos;
702 }
703 // decompose on the output side
704 for ( v = 0; v < nVarsNew; v++ )
705 {
706 Cof0[v] = Abc_Tt6Cofactor0( t, pVarsNew[v] );
707 Cof1[v] = Abc_Tt6Cofactor1( t, pVarsNew[v] );
708 assert( Cof0[v] != Cof1[v] );
709 if ( Cof0[v] == 0 ) // ax
710 {
711 pBuffer[Pos++] = '(';
712 pBuffer[Pos++] = 'a' + pVarsNew[v];
713 Pos = Dau_DsdPerform_rec( Cof1[v], pBuffer, Pos, pVarsNew, nVarsNew );
714 pBuffer[Pos++] = ')';
715 return Pos;
716 }
717 if ( Cof0[v] == ~(word)0 ) // !(ax)
718 {
719 pBuffer[Pos++] = '!';
720 pBuffer[Pos++] = '(';
721 pBuffer[Pos++] = 'a' + pVarsNew[v];
722 Pos = Dau_DsdPerform_rec( ~Cof1[v], pBuffer, Pos, pVarsNew, nVarsNew );
723 pBuffer[Pos++] = ')';
724 return Pos;
725 }
726 if ( Cof1[v] == 0 ) // !ax
727 {
728 pBuffer[Pos++] = '(';
729 pBuffer[Pos++] = '!';
730 pBuffer[Pos++] = 'a' + pVarsNew[v];
731 Pos = Dau_DsdPerform_rec( Cof0[v], pBuffer, Pos, pVarsNew, nVarsNew );
732 pBuffer[Pos++] = ')';
733 return Pos;
734 }
735 if ( Cof1[v] == ~(word)0 ) // !(!ax)
736 {
737 pBuffer[Pos++] = '!';
738 pBuffer[Pos++] = '(';
739 pBuffer[Pos++] = '!';
740 pBuffer[Pos++] = 'a' + pVarsNew[v];
741 Pos = Dau_DsdPerform_rec( ~Cof0[v], pBuffer, Pos, pVarsNew, nVarsNew );
742 pBuffer[Pos++] = ')';
743 return Pos;
744 }
745 if ( Cof0[v] == ~Cof1[v] ) // a^x
746 {
747 pBuffer[Pos++] = '[';
748 pBuffer[Pos++] = 'a' + pVarsNew[v];
749 Pos = Dau_DsdPerform_rec( Cof0[v], pBuffer, Pos, pVarsNew, nVarsNew );
750 pBuffer[Pos++] = ']';
751 return Pos;
752 }
753 }
754 // decompose on the input side
755 for ( v = 0; v < nVarsNew; v++ )
756 for ( u = v+1; u < nVarsNew; u++ )
757 {
758 Cof[0] = Abc_Tt6Cofactor0( Cof0[v], pVarsNew[u] );
759 Cof[1] = Abc_Tt6Cofactor1( Cof0[v], pVarsNew[u] );
760 Cof[2] = Abc_Tt6Cofactor0( Cof1[v], pVarsNew[u] );
761 Cof[3] = Abc_Tt6Cofactor1( Cof1[v], pVarsNew[u] );
762 if ( Cof[0] == Cof[1] && Cof[0] == Cof[2] ) // vu
763 {
764 PosStart = Pos;
765 sprintf( pNest, "(%c%c)", 'a' + pVarsNew[v], 'a' + pVarsNew[u] );
766 Pos = Dau_DsdPerform_rec( (s_Truths6[pVarsNew[u]] & Cof[3]) | (~s_Truths6[pVarsNew[u]] & Cof[0]), pBuffer, Pos, pVarsNew, nVarsNew );
767 Pos = Dau_DsdPerformReplace( pBuffer, PosStart, Pos, 'a' + pVarsNew[u], pNest );
768 return Pos;
769 }
770 if ( Cof[0] == Cof[1] && Cof[0] == Cof[3] ) // v!u
771 {
772 PosStart = Pos;
773 sprintf( pNest, "(%c!%c)", 'a' + pVarsNew[v], 'a' + pVarsNew[u] );
774 Pos = Dau_DsdPerform_rec( (s_Truths6[pVarsNew[u]] & Cof[2]) | (~s_Truths6[pVarsNew[u]] & Cof[0]), pBuffer, Pos, pVarsNew, nVarsNew );
775 Pos = Dau_DsdPerformReplace( pBuffer, PosStart, Pos, 'a' + pVarsNew[u], pNest );
776 return Pos;
777 }
778 if ( Cof[0] == Cof[2] && Cof[0] == Cof[3] ) // !vu
779 {
780 PosStart = Pos;
781 sprintf( pNest, "(!%c%c)", 'a' + pVarsNew[v], 'a' + pVarsNew[u] );
782 Pos = Dau_DsdPerform_rec( (s_Truths6[pVarsNew[u]] & Cof[1]) | (~s_Truths6[pVarsNew[u]] & Cof[0]), pBuffer, Pos, pVarsNew, nVarsNew );
783 Pos = Dau_DsdPerformReplace( pBuffer, PosStart, Pos, 'a' + pVarsNew[u], pNest );
784 return Pos;
785 }
786 if ( Cof[1] == Cof[2] && Cof[1] == Cof[3] ) // !v!u
787 {
788 PosStart = Pos;
789 sprintf( pNest, "(!%c!%c)", 'a' + pVarsNew[v], 'a' + pVarsNew[u] );
790 Pos = Dau_DsdPerform_rec( (s_Truths6[pVarsNew[u]] & Cof[0]) | (~s_Truths6[pVarsNew[u]] & Cof[1]), pBuffer, Pos, pVarsNew, nVarsNew );
791 Pos = Dau_DsdPerformReplace( pBuffer, PosStart, Pos, 'a' + pVarsNew[u], pNest );
792 return Pos;
793 }
794 if ( Cof[0] == Cof[3] && Cof[1] == Cof[2] ) // v+u
795 {
796 PosStart = Pos;
797 sprintf( pNest, "[%c%c]", 'a' + pVarsNew[v], 'a' + pVarsNew[u] );
798 Pos = Dau_DsdPerform_rec( (s_Truths6[pVarsNew[u]] & Cof[1]) | (~s_Truths6[pVarsNew[u]] & Cof[0]), pBuffer, Pos, pVarsNew, nVarsNew );
799 Pos = Dau_DsdPerformReplace( pBuffer, PosStart, Pos, 'a' + pVarsNew[u], pNest );
800 return Pos;
801 }
802 }
803 // find best variable for MUX decomposition
804 vBest = -1;
805 CountBest = 10;
806 for ( v = 0; v < nVarsNew; v++ )
807 {
808 int CountCur = 0;
809 for ( u = 0; u < nVarsNew; u++ )
810 if ( u != v && Abc_Tt6HasVar(Cof0[v], pVarsNew[u]) && Abc_Tt6HasVar(Cof1[v], pVarsNew[u]) )
811 CountCur++;
812 if ( CountBest > CountCur )
813 {
814 CountBest = CountCur;
815 vBest = v;
816 }
817 if ( CountCur == 0 )
818 break;
819 }
820 // perform MUX decomposition
821 pBuffer[Pos++] = '<';
822 pBuffer[Pos++] = 'a' + pVarsNew[vBest];
823 Pos = Dau_DsdPerform_rec( Cof1[vBest], pBuffer, Pos, pVarsNew, nVarsNew );
824 Pos = Dau_DsdPerform_rec( Cof0[vBest], pBuffer, Pos, pVarsNew, nVarsNew );
825 pBuffer[Pos++] = '>';
826 return Pos;
827 }
Dau_DsdPerform(word t)828 char * Dau_DsdPerform( word t )
829 {
830 static char pBuffer[DAU_MAX_STR];
831 int pVarsNew[6] = {0, 1, 2, 3, 4, 5};
832 int Pos = 0;
833 if ( t == 0 )
834 pBuffer[Pos++] = '0';
835 else if ( t == ~(word)0 )
836 pBuffer[Pos++] = '1';
837 else
838 Pos = Dau_DsdPerform_rec( t, pBuffer, Pos, pVarsNew, 6 );
839 pBuffer[Pos++] = 0;
840 // printf( "%d ", strlen(pBuffer) );
841 // printf( "%s ->", pBuffer );
842 Dau_DsdRemoveBraces( pBuffer, Dau_DsdComputeMatches(pBuffer) );
843 // printf( " %s\n", pBuffer );
844 return pBuffer;
845 }
846
847 /**Function*************************************************************
848
849 Synopsis []
850
851 Description []
852
853 SideEffects []
854
855 SeeAlso []
856
857 ***********************************************************************/
Dau_DsdTest3()858 void Dau_DsdTest3()
859 {
860 // word t = s_Truths6[0] & s_Truths6[1] & s_Truths6[2];
861 // word t = ~s_Truths6[0] | (s_Truths6[1] ^ ~s_Truths6[2]);
862 // word t = (s_Truths6[1] & s_Truths6[2]) | (s_Truths6[0] & s_Truths6[3]);
863 // word t = (~s_Truths6[1] & ~s_Truths6[2]) | (s_Truths6[0] ^ s_Truths6[3]);
864 // word t = ((~s_Truths6[1] & ~s_Truths6[2]) | (s_Truths6[0] ^ s_Truths6[3])) ^ s_Truths6[5];
865 // word t = ((s_Truths6[1] & ~s_Truths6[2]) ^ (s_Truths6[0] & s_Truths6[3])) & s_Truths6[5];
866 // word t = (~(~s_Truths6[0] & ~s_Truths6[4]) & s_Truths6[2]) | (~s_Truths6[1] & ~s_Truths6[0] & ~s_Truths6[4]);
867 // word t = 0x0000000000005F3F;
868 // word t = 0xF3F5030503050305;
869 // word t = (s_Truths6[0] & s_Truths6[1] & (s_Truths6[2] ^ s_Truths6[4])) | (~s_Truths6[0] & ~s_Truths6[1] & ~(s_Truths6[2] ^ s_Truths6[4]));
870 // word t = 0x05050500f5f5f5f3;
871 word t = ABC_CONST(0x9ef7a8d9c7193a0f);
872 char * p = Dau_DsdPerform( t );
873 word t2 = Dau_Dsd6ToTruth( p );
874 if ( t != t2 )
875 printf( "Verification failed.\n" );
876 }
877
878
879
880
881 /**Function*************************************************************
882
883 Synopsis [Find the best cofactoring variable.]
884
885 Description [Return -2 if non-DSD; -1 if full DSD; otherwise,
886 returns cofactoring variables i (i >= 0).]
887
888 SideEffects []
889
890 SeeAlso []
891
892 ***********************************************************************/
Dau_DsdCheck1Step(void * p,word * pTruth,int nVarsInit,int * pVarLevels)893 int Dau_DsdCheck1Step( void * p, word * pTruth, int nVarsInit, int * pVarLevels )
894 {
895 word pCofTemp[DAU_MAX_WORD];
896 int pVarPrios[DAU_MAX_VAR];
897 int nWords = Abc_TtWordNum(nVarsInit);
898 int nSizeNonDec, nSizeNonDec0, nSizeNonDec1;
899 int i, vBest = -2, nSumCofsBest = ABC_INFINITY, nSumCofs;
900 nSizeNonDec = Dau_DsdDecompose( pTruth, nVarsInit, 0, 0, NULL );
901 if ( nSizeNonDec == 0 )
902 return -1;
903 assert( nSizeNonDec > 0 );
904 // find variable priority
905 for ( i = 0; i < nVarsInit; i++ )
906 pVarPrios[i] = i;
907 if ( pVarLevels )
908 {
909 extern int Dau_DsdLevelVar( void * pMan, int iVar );
910 int pVarLevels[DAU_MAX_VAR];
911 for ( i = 0; i < nVarsInit; i++ )
912 pVarLevels[i] = -Dau_DsdLevelVar( p, i );
913 // for ( i = 0; i < nVarsInit; i++ )
914 // printf( "%d ", -pVarLevels[i] );
915 // printf( "\n" );
916 Vec_IntSelectSortCost2( pVarPrios, nVarsInit, pVarLevels );
917 // for ( i = 0; i < nVarsInit; i++ )
918 // printf( "%d ", pVarPrios[i] );
919 // printf( "\n\n" );
920 }
921 for ( i = 0; i < nVarsInit; i++ )
922 {
923 assert( pVarPrios[i] >= 0 && pVarPrios[i] < nVarsInit );
924 // try first cofactor
925 Abc_TtCofactor0p( pCofTemp, pTruth, nWords, pVarPrios[i] );
926 nSumCofs = Abc_TtSupportSize( pCofTemp, nVarsInit );
927 nSizeNonDec0 = Dau_DsdDecompose( pCofTemp, nVarsInit, 0, 0, NULL );
928 // try second cofactor
929 Abc_TtCofactor1p( pCofTemp, pTruth, nWords, pVarPrios[i] );
930 nSumCofs += Abc_TtSupportSize( pCofTemp, nVarsInit );
931 nSizeNonDec1 = Dau_DsdDecompose( pCofTemp, nVarsInit, 0, 0, NULL );
932 // compare cofactors
933 if ( nSizeNonDec0 || nSizeNonDec1 )
934 continue;
935 if ( nSumCofsBest > nSumCofs )
936 {
937 vBest = pVarPrios[i];
938 nSumCofsBest = nSumCofs;
939 }
940 }
941 return vBest;
942 }
943
944 /**Function*************************************************************
945
946 Synopsis [Data-structure to store DSD information.]
947
948 Description []
949
950 SideEffects []
951
952 SeeAlso []
953
954 ***********************************************************************/
955 typedef struct Dau_Dsd_t_ Dau_Dsd_t;
956 struct Dau_Dsd_t_
957 {
958 int nVarsInit; // the initial number of variables
959 int nVarsUsed; // the current number of variables
960 int nPos; // writing position
961 int nSizeNonDec; // size of the largest non-decomposable block
962 int nConsts; // the number of constant decompositions
963 int uConstMask; // constant decomposition mask
964 int fSplitPrime; // represent prime function as 1-step DSD
965 int fWriteTruth; // writing truth table as a hex string
966 int * pVarLevels; // variable levels
967 char pVarDefs[32][8]; // variable definitions
968 char Cache[32][32]; // variable cache
969 char pOutput[DAU_MAX_STR]; // output stream
970 };
971
972 static abctime s_Times[3] = {0};
973
974 /**Function*************************************************************
975
976 Synopsis [Manipulation of DSD data-structure.]
977
978 Description []
979
980 SideEffects []
981
982 SeeAlso []
983
984 ***********************************************************************/
Dau_DsdInitialize(Dau_Dsd_t * p,int nVarsInit)985 static inline void Dau_DsdInitialize( Dau_Dsd_t * p, int nVarsInit )
986 {
987 int i, v, u;
988 assert( nVarsInit >= 0 && nVarsInit <= 16 );
989 p->nVarsInit = nVarsInit;
990 p->nVarsUsed = nVarsInit;
991 p->nPos = 0;
992 p->nSizeNonDec = 0;
993 p->nConsts = 0;
994 p->uConstMask = 0;
995 for ( i = 0; i < nVarsInit; i++ )
996 p->pVarDefs[i][0] = 'a' + i, p->pVarDefs[i][1] = 0;
997 for ( v = 0; v < nVarsInit; v++ )
998 for ( u = 0; u < nVarsInit; u++ )
999 p->Cache[v][u] = 0;
1000
1001 }
Dau_DsdWriteString(Dau_Dsd_t * p,char * pStr)1002 static inline void Dau_DsdWriteString( Dau_Dsd_t * p, char * pStr )
1003 {
1004 while ( *pStr )
1005 p->pOutput[ p->nPos++ ] = *pStr++;
1006 }
Dau_DsdWriteVar(Dau_Dsd_t * p,int iVar,int fInv)1007 static inline void Dau_DsdWriteVar( Dau_Dsd_t * p, int iVar, int fInv )
1008 {
1009 char * pStr;
1010 if ( fInv )
1011 p->pOutput[ p->nPos++ ] = '!';
1012 for ( pStr = p->pVarDefs[iVar]; *pStr; pStr++ )
1013 if ( *pStr >= 'a' + p->nVarsInit && *pStr < 'a' + p->nVarsUsed )
1014 Dau_DsdWriteVar( p, *pStr - 'a', 0 );
1015 else
1016 p->pOutput[ p->nPos++ ] = *pStr;
1017 }
Dau_DsdLevelVar(void * pMan,int iVar)1018 int Dau_DsdLevelVar( void * pMan, int iVar )
1019 {
1020 Dau_Dsd_t * p = (Dau_Dsd_t *)pMan;
1021 char * pStr;
1022 int LevelMax = 0, Level;
1023 for ( pStr = p->pVarDefs[iVar]; *pStr; pStr++ )
1024 {
1025 if ( *pStr >= 'a' + p->nVarsInit && *pStr < 'a' + p->nVarsUsed )
1026 Level = 1 + Dau_DsdLevelVar( p, *pStr - 'a' );
1027 else
1028 Level = p->pVarLevels[*pStr - 'a'];
1029 LevelMax = Abc_MaxInt( LevelMax, Level );
1030 }
1031 return LevelMax;
1032 }
Dau_DsdTranslate(Dau_Dsd_t * p,int * pVars,int nVars,char * pStr)1033 static inline void Dau_DsdTranslate( Dau_Dsd_t * p, int * pVars, int nVars, char * pStr )
1034 {
1035 for ( ; *pStr; pStr++ )
1036 if ( *pStr >= 'a' && *pStr < 'a' + nVars )
1037 Dau_DsdWriteVar( p, pVars[*pStr - 'a'], 0 );
1038 else
1039 p->pOutput[ p->nPos++ ] = *pStr;
1040 }
Dau_DsdWritePrime(Dau_Dsd_t * p,word * pTruth,int * pVars,int nVars)1041 static inline int Dau_DsdWritePrime( Dau_Dsd_t * p, word * pTruth, int * pVars, int nVars )
1042 {
1043 int v, RetValue = 2;
1044 assert( nVars > 2 );
1045 if ( p->fSplitPrime )
1046 {
1047 word pCofTemp[DAU_MAX_WORD];
1048 int nWords = Abc_TtWordNum(nVars);
1049 int vBest = Dau_DsdCheck1Step( p, pTruth, nVars, p->pVarLevels );
1050 assert( vBest != -1 );
1051 if ( vBest == -2 ) // non-dec
1052 p->nPos += Abc_TtWriteHexRev( p->pOutput + p->nPos, pTruth, nVars );
1053 else
1054 {
1055 char pRes[DAU_MAX_STR];
1056 int nNonDecSize;
1057 // compose the result
1058 Dau_DsdWriteString( p, "<" );
1059 Dau_DsdWriteVar( p, vBest, 0 );
1060 // split decomposition
1061 Abc_TtCofactor1p( pCofTemp, pTruth, nWords, vBest );
1062 nNonDecSize = Dau_DsdDecompose( pCofTemp, nVars, 0, p->fWriteTruth, pRes );
1063 assert( nNonDecSize == 0 );
1064 Dau_DsdWriteString( p, pRes );
1065 // split decomposition
1066 Abc_TtCofactor0p( pCofTemp, pTruth, nWords, vBest );
1067 nNonDecSize = Dau_DsdDecompose( pCofTemp, nVars, 0, p->fWriteTruth, pRes );
1068 assert( nNonDecSize == 0 );
1069 Dau_DsdWriteString( p, pRes );
1070 Dau_DsdWriteString( p, ">" );
1071 RetValue = 1;
1072 }
1073 }
1074 else if ( p->fWriteTruth )
1075 p->nPos += Abc_TtWriteHexRev( p->pOutput + p->nPos, pTruth, nVars );
1076 Dau_DsdWriteString( p, "{" );
1077 for ( v = 0; v < nVars; v++ )
1078 Dau_DsdWriteVar( p, pVars[v], 0 );
1079 Dau_DsdWriteString( p, "}" );
1080 p->nSizeNonDec = nVars;
1081 return RetValue;
1082 }
Dau_DsdFinalize(Dau_Dsd_t * p)1083 static inline void Dau_DsdFinalize( Dau_Dsd_t * p )
1084 {
1085 int i;
1086 for ( i = 0; i < p->nConsts; i++ )
1087 p->pOutput[ p->nPos++ ] = ((p->uConstMask >> (p->nConsts-1-i)) & 1) ? ']' : ')';
1088 p->pOutput[ p->nPos++ ] = 0;
1089 }
Dau_DsdAddVarDef(Dau_Dsd_t * p,char * pStr)1090 static inline int Dau_DsdAddVarDef( Dau_Dsd_t * p, char * pStr )
1091 {
1092 int u;
1093 assert( strlen(pStr) < 8 );
1094 assert( p->nVarsUsed < 32 );
1095 for ( u = 0; u < p->nVarsUsed; u++ )
1096 p->Cache[p->nVarsUsed][u] = 0;
1097 for ( u = 0; u < p->nVarsUsed; u++ )
1098 p->Cache[u][p->nVarsUsed] = 0;
1099 sprintf( p->pVarDefs[p->nVarsUsed++], "%s", pStr );
1100 return p->nVarsUsed - 1;
1101 }
Dau_DsdFindVarDef(int * pVars,int nVars,int VarDef)1102 static inline int Dau_DsdFindVarDef( int * pVars, int nVars, int VarDef )
1103 {
1104 int v;
1105 for ( v = 0; v < nVars; v++ )
1106 if ( pVars[v] == VarDef )
1107 break;
1108 assert( v < nVars );
1109 return v;
1110 }
Dau_DsdInsertVarCache(Dau_Dsd_t * p,int v,int u,int Status)1111 static inline void Dau_DsdInsertVarCache( Dau_Dsd_t * p, int v, int u, int Status )
1112 {
1113 assert( v != u );
1114 assert( Status > 0 && Status < 4 );
1115 assert( p->Cache[v][u] == 0 );
1116 p->Cache[v][u] = Status;
1117 }
Dau_DsdLookupVarCache(Dau_Dsd_t * p,int v,int u)1118 static inline int Dau_DsdLookupVarCache( Dau_Dsd_t * p, int v, int u )
1119 {
1120 return p->Cache[v][u];
1121 }
1122
1123 /**Function*************************************************************
1124
1125 Synopsis [Procedures specialized for 6-variable functions.]
1126
1127 Description []
1128
1129 SideEffects []
1130
1131 SeeAlso []
1132
1133 ***********************************************************************/
Dau_Dsd6DecomposeSingleVarOne(Dau_Dsd_t * p,word * pTruth,int * pVars,int nVars,int v)1134 static inline int Dau_Dsd6DecomposeSingleVarOne( Dau_Dsd_t * p, word * pTruth, int * pVars, int nVars, int v )
1135 {
1136 // consider negative cofactors
1137 if ( pTruth[0] & 1 )
1138 {
1139 if ( Abc_Tt6Cof0IsConst1( pTruth[0], v ) ) // !(ax)
1140 {
1141 Dau_DsdWriteString( p, "!(" );
1142 pTruth[0] = ~Abc_Tt6Cofactor1( pTruth[0], v );
1143 goto finish;
1144 }
1145 }
1146 else
1147 {
1148 if ( Abc_Tt6Cof0IsConst0( pTruth[0], v ) ) // ax
1149 {
1150 Dau_DsdWriteString( p, "(" );
1151 pTruth[0] = Abc_Tt6Cofactor1( pTruth[0], v );
1152 goto finish;
1153 }
1154 }
1155 // consider positive cofactors
1156 if ( pTruth[0] >> 63 )
1157 {
1158 if ( Abc_Tt6Cof1IsConst1( pTruth[0], v ) ) // !(!ax)
1159 {
1160 Dau_DsdWriteString( p, "!(!" );
1161 pTruth[0] = ~Abc_Tt6Cofactor0( pTruth[0], v );
1162 goto finish;
1163 }
1164 }
1165 else
1166 {
1167 if ( Abc_Tt6Cof1IsConst0( pTruth[0], v ) ) // !ax
1168 {
1169 Dau_DsdWriteString( p, "(!" );
1170 pTruth[0] = Abc_Tt6Cofactor0( pTruth[0], v );
1171 goto finish;
1172 }
1173 }
1174 // consider equal cofactors
1175 if ( Abc_Tt6CofsOpposite( pTruth[0], v ) ) // [ax]
1176 {
1177 Dau_DsdWriteString( p, "[" );
1178 pTruth[0] = Abc_Tt6Cofactor0( pTruth[0], v );
1179 p->uConstMask |= (1 << p->nConsts);
1180 goto finish;
1181 }
1182 return 0;
1183
1184 finish:
1185 p->nConsts++;
1186 Dau_DsdWriteVar( p, pVars[v], 0 );
1187 pVars[v] = pVars[nVars-1];
1188 Abc_TtSwapVars( pTruth, nVars, v, nVars-1 );
1189 return 1;
1190 }
Dau_Dsd6DecomposeSingleVar(Dau_Dsd_t * p,word * pTruth,int * pVars,int nVars)1191 int Dau_Dsd6DecomposeSingleVar( Dau_Dsd_t * p, word * pTruth, int * pVars, int nVars )
1192 {
1193 abctime clk = Abc_Clock();
1194 assert( nVars > 1 );
1195 while ( 1 )
1196 {
1197 int v;
1198 for ( v = nVars - 1; v >= 0 && nVars > 1; v-- )
1199 if ( Dau_Dsd6DecomposeSingleVarOne( p, pTruth, pVars, nVars, v ) )
1200 {
1201 nVars--;
1202 break;
1203 }
1204 if ( v == -1 || nVars == 1 )
1205 break;
1206 }
1207 if ( nVars == 1 )
1208 Dau_DsdWriteVar( p, pVars[--nVars], (int)(pTruth[0] & 1) );
1209 s_Times[0] += Abc_Clock() - clk;
1210 return nVars;
1211 }
Dau_Dsd6FindSupportOne(Dau_Dsd_t * p,word tCof0,word tCof1,int * pVars,int nVars,int v,int u)1212 static inline int Dau_Dsd6FindSupportOne( Dau_Dsd_t * p, word tCof0, word tCof1, int * pVars, int nVars, int v, int u )
1213 {
1214 int Status = p ? Dau_DsdLookupVarCache( p, pVars[v], pVars[u] ) : 0;
1215 if ( Status == 0 )
1216 {
1217 Status = (Abc_Tt6HasVar(tCof1, u) << 1) | Abc_Tt6HasVar(tCof0, u);
1218 if ( p )
1219 Dau_DsdInsertVarCache( p, pVars[v], pVars[u], Status );
1220 }
1221 return Status;
1222 }
Dau_Dsd6FindSupports(Dau_Dsd_t * p,word * pTruth,int * pVars,int nVars,int v)1223 static inline unsigned Dau_Dsd6FindSupports( Dau_Dsd_t * p, word * pTruth, int * pVars, int nVars, int v )
1224 {
1225 int u;
1226 unsigned uSupports = 0;
1227 word tCof0 = Abc_Tt6Cofactor0( pTruth[0], v );
1228 word tCof1 = Abc_Tt6Cofactor1( pTruth[0], v );
1229 //Kit_DsdPrintFromTruth( (unsigned *)&tCof0, 6 );printf( "\n" );
1230 //Kit_DsdPrintFromTruth( (unsigned *)&tCof1, 6 );printf( "\n" );
1231 for ( u = 0; u < nVars; u++ )
1232 if ( u != v )
1233 uSupports |= (Dau_Dsd6FindSupportOne( p, tCof0, tCof1, pVars, nVars, v, u ) << (2 * u));
1234 return uSupports;
1235 }
Dau_DsdPrintSupports(unsigned uSupp,int nVars)1236 static inline void Dau_DsdPrintSupports( unsigned uSupp, int nVars )
1237 {
1238 int v, Value;
1239 printf( "Cofactor supports: " );
1240 for ( v = nVars - 1; v >= 0; v-- )
1241 {
1242 Value = ((uSupp >> (2*v)) & 3);
1243 if ( Value == 1 )
1244 printf( "01" );
1245 else if ( Value == 2 )
1246 printf( "10" );
1247 else if ( Value == 3 )
1248 printf( "11" );
1249 else
1250 printf( "00" );
1251 if ( v )
1252 printf( "-" );
1253 }
1254 printf( "\n" );
1255 }
1256 // checks decomposability with respect to the pair (v, u)
Dau_Dsd6DecomposeDoubleVarsOne(Dau_Dsd_t * p,word * pTruth,int * pVars,int nVars,int v,int u)1257 static inline int Dau_Dsd6DecomposeDoubleVarsOne( Dau_Dsd_t * p, word * pTruth, int * pVars, int nVars, int v, int u )
1258 {
1259 char pBuffer[10] = { 0 };
1260 word tCof0 = Abc_Tt6Cofactor0( pTruth[0], v );
1261 word tCof1 = Abc_Tt6Cofactor1( pTruth[0], v );
1262 int Status = Dau_Dsd6FindSupportOne( p, tCof0, tCof1, pVars, nVars, v, u );
1263 assert( v > u );
1264 //printf( "Checking %s and %s.\n", p->pVarDefs[pVars[v]], p->pVarDefs[pVars[u]] );
1265
1266 // Kit_DsdPrintFromTruth( (unsigned *)pTruth, 6 );printf( "\n" );
1267 if ( Status == 3 )
1268 {
1269 // both F(v=0) and F(v=1) depend on u
1270 if ( Abc_Tt6Cof0EqualCof1(tCof0, tCof1, u) && Abc_Tt6Cof0EqualCof1(tCof1, tCof0, u) ) // v+u
1271 {
1272 pTruth[0] = (s_Truths6[u] & Abc_Tt6Cofactor1(tCof0, u)) | (~s_Truths6[u] & Abc_Tt6Cofactor0(tCof0, u));
1273 sprintf( pBuffer, "[%c%c]", 'a' + pVars[v], 'a' + pVars[u] );
1274 goto finish;
1275 }
1276 }
1277 else if ( Status == 2 )
1278 {
1279 // F(v=0) does not depend on u; F(v=1) depends on u
1280 if ( Abc_Tt6Cof0EqualCof0(tCof0, tCof1, u) ) // vu
1281 {
1282 sprintf( pBuffer, "(%c%c)", 'a' + pVars[v], 'a' + pVars[u] );
1283 pTruth[0] = (s_Truths6[u] & Abc_Tt6Cofactor1(tCof1, u)) | (~s_Truths6[u] & Abc_Tt6Cofactor0(tCof0, u));
1284 goto finish;
1285 }
1286 if ( Abc_Tt6Cof0EqualCof1(tCof0, tCof1, u) ) // v!u
1287 {
1288 sprintf( pBuffer, "(%c!%c)", 'a' + pVars[v], 'a' + pVars[u] );
1289 pTruth[0] = (s_Truths6[u] & Abc_Tt6Cofactor0(tCof1, u)) | (~s_Truths6[u] & Abc_Tt6Cofactor0(tCof0, u));
1290 goto finish;
1291 }
1292 }
1293 else if ( Status == 1 )
1294 {
1295 // F(v=0) depends on u; F(v=1) does not depend on u
1296 if ( Abc_Tt6Cof0EqualCof1(tCof0, tCof1, u) ) // !vu
1297 {
1298 sprintf( pBuffer, "(!%c%c)", 'a' + pVars[v], 'a' + pVars[u] );
1299 pTruth[0] = (s_Truths6[u] & Abc_Tt6Cofactor1(tCof0, u)) | (~s_Truths6[u] & Abc_Tt6Cofactor0(tCof0, u));
1300 goto finish;
1301 }
1302 if ( Abc_Tt6Cof1EqualCof1(tCof0, tCof1, u) ) // !v!u
1303 {
1304 sprintf( pBuffer, "(!%c!%c)", 'a' + pVars[v], 'a' + pVars[u] );
1305 pTruth[0] = (s_Truths6[u] & Abc_Tt6Cofactor0(tCof0, u)) | (~s_Truths6[u] & Abc_Tt6Cofactor1(tCof1, u));
1306 goto finish;
1307 }
1308 }
1309 return nVars;
1310 finish:
1311 // finalize decomposition
1312 assert( pBuffer[0] );
1313 pVars[u] = Dau_DsdAddVarDef( p, pBuffer );
1314 pVars[v] = pVars[nVars-1];
1315 Abc_TtSwapVars( pTruth, nVars, v, nVars-1 );
1316 if ( Dau_Dsd6DecomposeSingleVarOne( p, pTruth, pVars, --nVars, u ) )
1317 nVars = Dau_Dsd6DecomposeSingleVar( p, pTruth, pVars, --nVars );
1318 return nVars;
1319 }
Dau_Dsd6DecomposeDoubleVars(Dau_Dsd_t * p,word * pTruth,int * pVars,int nVars)1320 int Dau_Dsd6DecomposeDoubleVars( Dau_Dsd_t * p, word * pTruth, int * pVars, int nVars )
1321 {
1322 abctime clk = Abc_Clock();
1323 while ( 1 )
1324 {
1325 int v, u, nVarsOld;
1326 for ( v = nVars - 1; v > 0; v-- )
1327 {
1328 for ( u = v - 1; u >= 0; u-- )
1329 {
1330 if ( Dau_DsdLookupVarCache( p, pVars[v], pVars[u] ) )
1331 continue;
1332 nVarsOld = nVars;
1333 nVars = Dau_Dsd6DecomposeDoubleVarsOne( p, pTruth, pVars, nVars, v, u );
1334 if ( nVars == 0 )
1335 {
1336 s_Times[1] += Abc_Clock() - clk;
1337 return 0;
1338 }
1339 if ( nVarsOld > nVars )
1340 break;
1341 }
1342 if ( u >= 0 ) // found
1343 break;
1344 }
1345 if ( v == 0 ) // not found
1346 break;
1347 }
1348 s_Times[1] += Abc_Clock() - clk;
1349 return nVars;
1350 }
1351
1352 // look for MUX-decomposable variable on top or at the bottom
Dau_Dsd6DecomposeTripleVarsOuter(Dau_Dsd_t * p,word * pTruth,int * pVars,int nVars,int v)1353 static inline int Dau_Dsd6DecomposeTripleVarsOuter( Dau_Dsd_t * p, word * pTruth, int * pVars, int nVars, int v )
1354 {
1355 extern int Dau_DsdDecomposeInt( Dau_Dsd_t * p, word * pTruth, int nVarsInit );
1356 Dau_Dsd_t P1, * p1 = &P1;
1357 word tCof0, tCof1;
1358 p1->fSplitPrime = 0;
1359 p1->fWriteTruth = p->fWriteTruth;
1360 // move this variable to the top
1361 ABC_SWAP( int, pVars[v], pVars[nVars-1] );
1362 Abc_TtSwapVars( pTruth, nVars, v, nVars-1 );
1363 // cofactor w.r.t the last variable
1364 tCof0 = Abc_Tt6Cofactor0( pTruth[0], nVars - 1 );
1365 tCof1 = Abc_Tt6Cofactor1( pTruth[0], nVars - 1 );
1366 // compose the result
1367 Dau_DsdWriteString( p, "<" );
1368 Dau_DsdWriteVar( p, pVars[nVars - 1], 0 );
1369 // split decomposition
1370 Dau_DsdDecomposeInt( p1, &tCof1, nVars - 1 );
1371 Dau_DsdTranslate( p, pVars, nVars - 1, p1->pOutput );
1372 p->nSizeNonDec = p1->nSizeNonDec;
1373 if ( p1->nSizeNonDec )
1374 *pTruth = tCof1;
1375 // split decomposition
1376 Dau_DsdDecomposeInt( p1, &tCof0, nVars - 1 );
1377 Dau_DsdTranslate( p, pVars, nVars - 1, p1->pOutput );
1378 Dau_DsdWriteString( p, ">" );
1379 p->nSizeNonDec = Abc_MaxInt( p->nSizeNonDec, p1->nSizeNonDec );
1380 if ( p1->nSizeNonDec )
1381 *pTruth = tCof0;
1382 return 0;
1383 }
Dau_Dsd6DecomposeTripleVarsInner(Dau_Dsd_t * p,word * pTruth,int * pVars,int nVars,int v,unsigned uSupports)1384 static inline int Dau_Dsd6DecomposeTripleVarsInner( Dau_Dsd_t * p, word * pTruth, int * pVars, int nVars, int v, unsigned uSupports )
1385 {
1386 int iVar0 = Abc_TtSuppFindFirst( uSupports & (~uSupports >> 1) & 0x55555555 ) >> 1;
1387 int iVar1 = Abc_TtSuppFindFirst( ~uSupports & ( uSupports >> 1) & 0x55555555 ) >> 1;
1388 word tCof0 = Abc_Tt6Cofactor0( pTruth[0], v );
1389 word tCof1 = Abc_Tt6Cofactor1( pTruth[0], v );
1390 word C00 = Abc_Tt6Cofactor0( tCof0, iVar0 );
1391 word C01 = Abc_Tt6Cofactor1( tCof0, iVar0 );
1392 word C10 = Abc_Tt6Cofactor0( tCof1, iVar1 );
1393 word C11 = Abc_Tt6Cofactor1( tCof1, iVar1 );
1394 int fEqual0 = (C00 == C10) && (C01 == C11);
1395 int fEqual1 = (C00 == C11) && (C01 == C10);
1396 if ( fEqual0 || fEqual1 )
1397 {
1398 char pBuffer[10];
1399 int VarId = pVars[iVar0];
1400 pTruth[0] = (s_Truths6[v] & C11) | (~s_Truths6[v] & C10);
1401 sprintf( pBuffer, "<%c%c%s%c>", 'a' + pVars[v], 'a' + pVars[iVar1], fEqual1 ? "!":"", 'a' + pVars[iVar0] );
1402 pVars[v] = Dau_DsdAddVarDef( p, pBuffer );
1403 // remove iVar1
1404 ABC_SWAP( int, pVars[iVar1], pVars[nVars-1] );
1405 Abc_TtSwapVars( pTruth, nVars, iVar1, nVars-1 ); nVars--;
1406 // remove iVar0
1407 iVar0 = Dau_DsdFindVarDef( pVars, nVars, VarId );
1408 ABC_SWAP( int, pVars[iVar0], pVars[nVars-1] );
1409 Abc_TtSwapVars( pTruth, nVars, iVar0, nVars-1 ); nVars--;
1410 // find the new var
1411 v = Dau_DsdFindVarDef( pVars, nVars, p->nVarsUsed-1 );
1412 // remove single variables if possible
1413 if ( Dau_Dsd6DecomposeSingleVarOne( p, pTruth, pVars, nVars, v ) )
1414 nVars = Dau_Dsd6DecomposeSingleVar( p, pTruth, pVars, --nVars );
1415 return nVars;
1416 }
1417 return nVars;
1418 }
Dau_Dsd6DecomposeTripleVars(Dau_Dsd_t * p,word * pTruth,int * pVars,int nVars)1419 int Dau_Dsd6DecomposeTripleVars( Dau_Dsd_t * p, word * pTruth, int * pVars, int nVars )
1420 {
1421 abctime clk = Abc_Clock();
1422 while ( 1 )
1423 {
1424 int v;
1425 // Kit_DsdPrintFromTruth( (unsigned *)pTruth, 6 ); printf( "\n" );
1426 for ( v = nVars - 1; v >= 0; v-- )
1427 {
1428 unsigned uSupports = Dau_Dsd6FindSupports( p, pTruth, pVars, nVars, v );
1429 // Dau_DsdPrintSupports( uSupports, nVars );
1430 if ( (uSupports & (uSupports >> 1) & 0x55555555) == 0 ) // non-overlapping supports
1431 return Dau_Dsd6DecomposeTripleVarsOuter( p, pTruth, pVars, nVars, v );
1432 if ( Abc_TtSuppOnlyOne( uSupports & (~uSupports >> 1) & 0x55555555) &&
1433 Abc_TtSuppOnlyOne(~uSupports & ( uSupports >> 1) & 0x55555555) ) // one unique variable in each cofactor
1434 {
1435 int nVarsNew = Dau_Dsd6DecomposeTripleVarsInner( p, pTruth, pVars, nVars, v, uSupports );
1436 if ( nVarsNew == nVars )
1437 continue;
1438 if ( nVarsNew == 0 )
1439 {
1440 s_Times[2] += Abc_Clock() - clk;
1441 return 0;
1442 }
1443 nVars = Dau_Dsd6DecomposeDoubleVars( p, pTruth, pVars, nVarsNew );
1444 if ( nVars == 0 )
1445 {
1446 s_Times[2] += Abc_Clock() - clk;
1447 return 0;
1448 }
1449 break;
1450 }
1451 }
1452 if ( v == -1 )
1453 {
1454 s_Times[2] += Abc_Clock() - clk;
1455 return nVars;
1456 }
1457 }
1458 assert( 0 );
1459 return -1;
1460 }
Dau_Dsd6DecomposeInternal(Dau_Dsd_t * p,word * pTruth,int * pVars,int nVars)1461 int Dau_Dsd6DecomposeInternal( Dau_Dsd_t * p, word * pTruth, int * pVars, int nVars )
1462 {
1463 // decompose single variales on the output side
1464 nVars = Dau_Dsd6DecomposeSingleVar( p, pTruth, pVars, nVars );
1465 if ( nVars == 0 )
1466 return 0;
1467 // decompose double variables on the input side
1468 nVars = Dau_Dsd6DecomposeDoubleVars( p, pTruth, pVars, nVars );
1469 if ( nVars == 0 )
1470 return 0;
1471 // decompose MUX on the output/input side
1472 nVars = Dau_Dsd6DecomposeTripleVars( p, pTruth, pVars, nVars );
1473 if ( nVars == 0 )
1474 return 0;
1475 // write non-decomposable function
1476 return Dau_DsdWritePrime( p, pTruth, pVars, nVars );
1477 }
1478
1479 /**Function*************************************************************
1480
1481 Synopsis [Procedures specialized for 6-variable functions.]
1482
1483 Description []
1484
1485 SideEffects []
1486
1487 SeeAlso []
1488
1489 ***********************************************************************/
Dau_DsdDecomposeSingleVarOne(Dau_Dsd_t * p,word * pTruth,int * pVars,int nVars,int v)1490 static inline int Dau_DsdDecomposeSingleVarOne( Dau_Dsd_t * p, word * pTruth, int * pVars, int nVars, int v )
1491 {
1492 int nWords = Abc_TtWordNum(nVars);
1493 // consider negative cofactors
1494 if ( pTruth[0] & 1 )
1495 {
1496 if ( Abc_TtCof0IsConst1( pTruth, nWords, v ) ) // !(ax)
1497 {
1498 Dau_DsdWriteString( p, "!(" );
1499 Abc_TtCofactor1( pTruth, nWords, v );
1500 Abc_TtNot( pTruth, nWords );
1501 goto finish;
1502 }
1503 }
1504 else
1505 {
1506 if ( Abc_TtCof0IsConst0( pTruth, nWords, v ) ) // ax
1507 {
1508 Dau_DsdWriteString( p, "(" );
1509 Abc_TtCofactor1( pTruth, nWords, v );
1510 goto finish;
1511 }
1512 }
1513 // consider positive cofactors
1514 if ( pTruth[nWords-1] >> 63 )
1515 {
1516 if ( Abc_TtCof1IsConst1( pTruth, nWords, v ) ) // !(!ax)
1517 {
1518 Dau_DsdWriteString( p, "!(!" );
1519 Abc_TtCofactor0( pTruth, nWords, v );
1520 Abc_TtNot( pTruth, nWords );
1521 goto finish;
1522 }
1523 }
1524 else
1525 {
1526 if ( Abc_TtCof1IsConst0( pTruth, nWords, v ) ) // !ax
1527 {
1528 Dau_DsdWriteString( p, "(!" );
1529 Abc_TtCofactor0( pTruth, nWords, v );
1530 goto finish;
1531 }
1532 }
1533 // consider equal cofactors
1534 if ( Abc_TtCofsOpposite( pTruth, nWords, v ) ) // [ax]
1535 {
1536 Dau_DsdWriteString( p, "[" );
1537 Abc_TtCofactor0( pTruth, nWords, v );
1538 p->uConstMask |= (1 << p->nConsts);
1539 goto finish;
1540 }
1541 return 0;
1542
1543 finish:
1544 p->nConsts++;
1545 Dau_DsdWriteVar( p, pVars[v], 0 );
1546 pVars[v] = pVars[nVars-1];
1547 Abc_TtSwapVars( pTruth, nVars, v, nVars-1 );
1548 return 1;
1549 }
Dau_DsdDecomposeSingleVar(Dau_Dsd_t * p,word * pTruth,int * pVars,int nVars)1550 int Dau_DsdDecomposeSingleVar( Dau_Dsd_t * p, word * pTruth, int * pVars, int nVars )
1551 {
1552 abctime clk = Abc_Clock();
1553 assert( nVars > 1 );
1554 while ( 1 )
1555 {
1556 int v;
1557 for ( v = nVars - 1; v >= 0 && nVars > 1; v-- )
1558 if ( Dau_DsdDecomposeSingleVarOne( p, pTruth, pVars, nVars, v ) )
1559 {
1560 nVars--;
1561 break;
1562 }
1563 if ( v == -1 || nVars == 1 )
1564 break;
1565 }
1566 if ( nVars == 1 )
1567 Dau_DsdWriteVar( p, pVars[--nVars], (int)(pTruth[0] & 1) );
1568 s_Times[0] += Abc_Clock() - clk;
1569 return nVars;
1570 }
1571
Dau_DsdFindSupportOne(Dau_Dsd_t * p,word * pTruth,int * pVars,int nVars,int v,int u)1572 static inline int Dau_DsdFindSupportOne( Dau_Dsd_t * p, word * pTruth, int * pVars, int nVars, int v, int u )
1573 {
1574 int nWords = Abc_TtWordNum(nVars);
1575 int Status = p ? Dau_DsdLookupVarCache( p, pVars[v], pVars[u] ) : 0;
1576 if ( Status == 0 )
1577 {
1578 // Status = (Abc_Tt6HasVar(tCof1, u) << 1) | Abc_Tt6HasVar(tCof0, u);
1579 if ( v < u )
1580 Status = (!Abc_TtCheckEqualCofs(pTruth, nWords, v, u, 1, 3) << 1) | !Abc_TtCheckEqualCofs(pTruth, nWords, v, u, 0, 2);
1581 else // if ( v > u )
1582 Status = (!Abc_TtCheckEqualCofs(pTruth, nWords, u, v, 2, 3) << 1) | !Abc_TtCheckEqualCofs(pTruth, nWords, u, v, 0, 1);
1583 assert( Status != 0 );
1584 if ( p )
1585 Dau_DsdInsertVarCache( p, pVars[v], pVars[u], Status );
1586 }
1587 return Status;
1588 }
Dau_DsdFindSupports(Dau_Dsd_t * p,word * pTruth,int * pVars,int nVars,int v)1589 static inline unsigned Dau_DsdFindSupports( Dau_Dsd_t * p, word * pTruth, int * pVars, int nVars, int v )
1590 {
1591 int u;
1592 unsigned uSupports = 0;
1593 //Kit_DsdPrintFromTruth( (unsigned *)&tCof0, 6 );printf( "\n" );
1594 //Kit_DsdPrintFromTruth( (unsigned *)&tCof1, 6 );printf( "\n" );
1595 for ( u = 0; u < nVars; u++ )
1596 if ( u != v )
1597 uSupports |= (Dau_DsdFindSupportOne( p, pTruth, pVars, nVars, v, u ) << (2 * u));
1598 return uSupports;
1599 }
1600
1601 // checks decomposability with respect to the pair (v, u)
Dau_DsdDecomposeDoubleVarsOne(Dau_Dsd_t * p,word * pTruth,int * pVars,int nVars,int v,int u)1602 static inline int Dau_DsdDecomposeDoubleVarsOne( Dau_Dsd_t * p, word * pTruth, int * pVars, int nVars, int v, int u )
1603 {
1604 char pBuffer[10] = { 0 };
1605 int nWords = Abc_TtWordNum(nVars);
1606 int Status = Dau_DsdFindSupportOne( p, pTruth, pVars, nVars, v, u );
1607 assert( v > u );
1608 //printf( "Checking %s and %s.\n", p->pVarDefs[pVars[v]], p->pVarDefs[pVars[u]] );
1609 if ( Status == 3 )
1610 {
1611 // both F(v=0) and F(v=1) depend on u
1612 // if ( Abc_Tt6Cof0EqualCof1(tCof0, tCof1, u) && Abc_Tt6Cof0EqualCof1(tCof1, tCof0, u) ) // v+u
1613 if ( Abc_TtCheckEqualCofs(pTruth, nWords, u, v, 0, 3) && Abc_TtCheckEqualCofs(pTruth, nWords, u, v, 1, 2) ) // 00=11 01=10 v+u
1614 {
1615 word pTtTemp[2][DAU_MAX_WORD];
1616 sprintf( pBuffer, "[%c%c]", 'a' + pVars[v], 'a' + pVars[u] );
1617 // pTruth[0] = (s_Truths6[u] & Abc_Tt6Cofactor1(tCof0, u)) | (~s_Truths6[u] & Abc_Tt6Cofactor0(tCof0, u));
1618 Abc_TtCofactor0p( pTtTemp[0], pTruth, nWords, v );
1619 Abc_TtCofactor0( pTtTemp[0], nWords, u );
1620 Abc_TtCofactor0p( pTtTemp[1], pTruth, nWords, v );
1621 Abc_TtCofactor1( pTtTemp[1], nWords, u );
1622 Abc_TtMux( pTruth, Dau_DsdTtElems()[u], pTtTemp[1], pTtTemp[0], nWords );
1623 goto finish;
1624 }
1625 }
1626 else if ( Status == 2 )
1627 {
1628 // F(v=0) does not depend on u; F(v=1) depends on u
1629 // if ( Abc_Tt6Cof0EqualCof0(tCof0, tCof1, u) ) // vu
1630 if ( Abc_TtCheckEqualCofs(pTruth, nWords, u, v, 0, 2) ) // 00=10 vu
1631 {
1632 word pTtTemp[2][DAU_MAX_WORD];
1633 sprintf( pBuffer, "(%c%c)", 'a' + pVars[v], 'a' + pVars[u] );
1634 // pTruth[0] = (s_Truths6[u] & Abc_Tt6Cofactor1(tCof1, u)) | (~s_Truths6[u] & Abc_Tt6Cofactor0(tCof0, u));
1635 Abc_TtCofactor0p( pTtTemp[0], pTruth, nWords, v );
1636 Abc_TtCofactor0( pTtTemp[0], nWords, u );
1637 Abc_TtCofactor1p( pTtTemp[1], pTruth, nWords, v );
1638 Abc_TtCofactor1( pTtTemp[1], nWords, u );
1639 Abc_TtMux( pTruth, Dau_DsdTtElems()[u], pTtTemp[1], pTtTemp[0], nWords );
1640 goto finish;
1641 }
1642 // if ( Abc_Tt6Cof0EqualCof1(tCof0, tCof1, u) ) // v!u
1643 if ( Abc_TtCheckEqualCofs(pTruth, nWords, u, v, 0, 3) ) // 00=11 v!u
1644 {
1645 word pTtTemp[2][DAU_MAX_WORD];
1646 sprintf( pBuffer, "(%c!%c)", 'a' + pVars[v], 'a' + pVars[u] );
1647 // pTruth[0] = (s_Truths6[u] & Abc_Tt6Cofactor0(tCof1, u)) | (~s_Truths6[u] & Abc_Tt6Cofactor0(tCof0, u));
1648 Abc_TtCofactor0p( pTtTemp[0], pTruth, nWords, v );
1649 Abc_TtCofactor0( pTtTemp[0], nWords, u );
1650 Abc_TtCofactor1p( pTtTemp[1], pTruth, nWords, v );
1651 Abc_TtCofactor0( pTtTemp[1], nWords, u );
1652 Abc_TtMux( pTruth, Dau_DsdTtElems()[u], pTtTemp[1], pTtTemp[0], nWords );
1653 goto finish;
1654 }
1655 }
1656 else if ( Status == 1 )
1657 {
1658 // F(v=0) depends on u; F(v=1) does not depend on u
1659 // if ( Abc_Tt6Cof0EqualCof1(tCof0, tCof1, u) ) // !vu
1660 if ( Abc_TtCheckEqualCofs(pTruth, nWords, u, v, 0, 3) ) // 00=11 !vu
1661 {
1662 word pTtTemp[2][DAU_MAX_WORD];
1663 sprintf( pBuffer, "(!%c%c)", 'a' + pVars[v], 'a' + pVars[u] );
1664 // pTruth[0] = (s_Truths6[u] & Abc_Tt6Cofactor1(tCof0, u)) | (~s_Truths6[u] & Abc_Tt6Cofactor0(tCof0, u));
1665 Abc_TtCofactor0p( pTtTemp[0], pTruth, nWords, v );
1666 Abc_TtCofactor0( pTtTemp[0], nWords, u );
1667 Abc_TtCofactor0p( pTtTemp[1], pTruth, nWords, v );
1668 Abc_TtCofactor1( pTtTemp[1], nWords, u );
1669 Abc_TtMux( pTruth, Dau_DsdTtElems()[u], pTtTemp[1], pTtTemp[0], nWords );
1670 goto finish;
1671 }
1672 // if ( Abc_Tt6Cof1EqualCof1(tCof0, tCof1, u) ) // !v!u
1673 if ( Abc_TtCheckEqualCofs(pTruth, nWords, u, v, 1, 3) ) // 01=11 !v!u
1674 {
1675 word pTtTemp[2][DAU_MAX_WORD];
1676 sprintf( pBuffer, "(!%c!%c)", 'a' + pVars[v], 'a' + pVars[u] );
1677 // pTruth[0] = (s_Truths6[u] & Abc_Tt6Cofactor0(tCof0, u)) | (~s_Truths6[u] & Abc_Tt6Cofactor1(tCof1, u));
1678 Abc_TtCofactor1p( pTtTemp[0], pTruth, nWords, v );
1679 Abc_TtCofactor1( pTtTemp[0], nWords, u );
1680 Abc_TtCofactor0p( pTtTemp[1], pTruth, nWords, v );
1681 Abc_TtCofactor0( pTtTemp[1], nWords, u );
1682 Abc_TtMux( pTruth, Dau_DsdTtElems()[u], pTtTemp[1], pTtTemp[0], nWords );
1683 goto finish;
1684 }
1685 }
1686 return nVars;
1687 finish:
1688 // finalize decomposition
1689 assert( pBuffer[0] );
1690 pVars[u] = Dau_DsdAddVarDef( p, pBuffer );
1691 pVars[v] = pVars[nVars-1];
1692 Abc_TtSwapVars( pTruth, nVars, v, nVars-1 );
1693 if ( Dau_DsdDecomposeSingleVarOne( p, pTruth, pVars, --nVars, u ) )
1694 nVars = Dau_DsdDecomposeSingleVar( p, pTruth, pVars, --nVars );
1695 return nVars;
1696 }
Dau_DsdDecomposeDoubleVars(Dau_Dsd_t * p,word * pTruth,int * pVars,int nVars)1697 int Dau_DsdDecomposeDoubleVars( Dau_Dsd_t * p, word * pTruth, int * pVars, int nVars )
1698 {
1699 abctime clk = Abc_Clock();
1700 while ( 1 )
1701 {
1702 int v, u, nVarsOld;
1703 for ( v = nVars - 1; v > 0; v-- )
1704 {
1705 for ( u = v - 1; u >= 0; u-- )
1706 {
1707 if ( Dau_DsdLookupVarCache( p, pVars[v], pVars[u] ) )
1708 continue;
1709 nVarsOld = nVars;
1710 nVars = Dau_DsdDecomposeDoubleVarsOne( p, pTruth, pVars, nVars, v, u );
1711 if ( nVars == 0 )
1712 {
1713 s_Times[1] += Abc_Clock() - clk;
1714 return 0;
1715 }
1716 if ( nVarsOld > nVars )
1717 break;
1718 }
1719 if ( u >= 0 ) // found
1720 break;
1721 }
1722 if ( v == 0 ) // not found
1723 break;
1724 }
1725 s_Times[1] += Abc_Clock() - clk;
1726 return nVars;
1727 }
1728
1729 // look for MUX-decomposable variable on top or at the bottom
Dau_DsdDecomposeTripleVarsOuter(Dau_Dsd_t * p,word * pTruth,int * pVars,int nVars,int v)1730 static inline int Dau_DsdDecomposeTripleVarsOuter( Dau_Dsd_t * p, word * pTruth, int * pVars, int nVars, int v )
1731 {
1732 extern int Dau_DsdDecomposeInt( Dau_Dsd_t * p, word * pTruth, int nVarsInit );
1733 Dau_Dsd_t P1, * p1 = &P1;
1734 word pTtCof[2][DAU_MAX_WORD];
1735 int nWords = Abc_TtWordNum(nVars);
1736 p1->fSplitPrime = 0;
1737 p1->fWriteTruth = p->fWriteTruth;
1738 // move this variable to the top
1739 ABC_SWAP( int, pVars[v], pVars[nVars-1] );
1740 Abc_TtSwapVars( pTruth, nVars, v, nVars-1 );
1741 // cofactor w.r.t the last variable
1742 // tCof0 = Abc_Tt6Cofactor0( pTruth[0], nVars - 1 );
1743 // tCof1 = Abc_Tt6Cofactor1( pTruth[0], nVars - 1 );
1744 Abc_TtCofactor0p( pTtCof[0], pTruth, nWords, nVars - 1 );
1745 Abc_TtCofactor1p( pTtCof[1], pTruth, nWords, nVars - 1 );
1746 // compose the result
1747 Dau_DsdWriteString( p, "<" );
1748 Dau_DsdWriteVar( p, pVars[nVars - 1], 0 );
1749 // split decomposition
1750 Dau_DsdDecomposeInt( p1, pTtCof[1], nVars - 1 );
1751 Dau_DsdTranslate( p, pVars, nVars - 1, p1->pOutput );
1752 p->nSizeNonDec = p1->nSizeNonDec;
1753 if ( p1->nSizeNonDec )
1754 Abc_TtCopy( pTruth, pTtCof[1], Abc_TtWordNum(p1->nSizeNonDec), 0 );
1755 // split decomposition
1756 Dau_DsdDecomposeInt( p1, pTtCof[0], nVars - 1 );
1757 Dau_DsdTranslate( p, pVars, nVars - 1, p1->pOutput );
1758 Dau_DsdWriteString( p, ">" );
1759 p->nSizeNonDec = Abc_MaxInt( p->nSizeNonDec, p1->nSizeNonDec );
1760 if ( p1->nSizeNonDec )
1761 Abc_TtCopy( pTruth, pTtCof[0], Abc_TtWordNum(p1->nSizeNonDec), 0 );
1762 return 0;
1763 }
Dau_DsdDecomposeTripleVarsInner(Dau_Dsd_t * p,word * pTruth,int * pVars,int nVars,int v,unsigned uSupports)1764 static inline int Dau_DsdDecomposeTripleVarsInner( Dau_Dsd_t * p, word * pTruth, int * pVars, int nVars, int v, unsigned uSupports )
1765 {
1766 int nWords = Abc_TtWordNum(nVars);
1767 int iVar0 = Abc_TtSuppFindFirst( uSupports & (~uSupports >> 1) & 0x55555555 ) >> 1;
1768 int iVar1 = Abc_TtSuppFindFirst( ~uSupports & ( uSupports >> 1) & 0x55555555 ) >> 1;
1769 int fEqual0, fEqual1;
1770 // word tCof0 = Abc_Tt6Cofactor0( pTruth[0], v );
1771 // word tCof1 = Abc_Tt6Cofactor1( pTruth[0], v );
1772 // word C00 = Abc_Tt6Cofactor0( tCof0, iVar0 );
1773 // word C01 = Abc_Tt6Cofactor1( tCof0, iVar0 );
1774 // word C10 = Abc_Tt6Cofactor0( tCof1, iVar1 );
1775 // word C11 = Abc_Tt6Cofactor1( tCof1, iVar1 );
1776 // int fEqual0 = (C00 == C10) && (C01 == C11);
1777 // int fEqual1 = (C00 == C11) && (C01 == C10);
1778 word pTtCof[2][DAU_MAX_WORD];
1779 word pTtFour[2][2][DAU_MAX_WORD];
1780 Abc_TtCofactor0p( pTtCof[0], pTruth, nWords, v );
1781 Abc_TtCofactor1p( pTtCof[1], pTruth, nWords, v );
1782 Abc_TtCofactor0p( pTtFour[0][0], pTtCof[0], nWords, iVar0 );
1783 Abc_TtCofactor1p( pTtFour[0][1], pTtCof[0], nWords, iVar0 );
1784 Abc_TtCofactor0p( pTtFour[1][0], pTtCof[1], nWords, iVar1 );
1785 Abc_TtCofactor1p( pTtFour[1][1], pTtCof[1], nWords, iVar1 );
1786 fEqual0 = Abc_TtEqual(pTtFour[0][0], pTtFour[1][0], nWords) && Abc_TtEqual(pTtFour[0][1], pTtFour[1][1], nWords);
1787 fEqual1 = Abc_TtEqual(pTtFour[0][0], pTtFour[1][1], nWords) && Abc_TtEqual(pTtFour[0][1], pTtFour[1][0], nWords);
1788 if ( fEqual0 || fEqual1 )
1789 {
1790 char pBuffer[10];
1791 int VarId = pVars[iVar0];
1792 // pTruth[0] = (s_Truths6[v] & C11) | (~s_Truths6[v] & C10);
1793 Abc_TtMux( pTruth, Dau_DsdTtElems()[v], pTtFour[1][1], pTtFour[1][0], nWords );
1794 sprintf( pBuffer, "<%c%c%s%c>", 'a' + pVars[v], 'a' + pVars[iVar1], fEqual1 ? "!":"", 'a' + pVars[iVar0] );
1795 pVars[v] = Dau_DsdAddVarDef( p, pBuffer );
1796 // remove iVar1
1797 ABC_SWAP( int, pVars[iVar1], pVars[nVars-1] );
1798 Abc_TtSwapVars( pTruth, nVars, iVar1, nVars-1 ); nVars--;
1799 // remove iVar0
1800 iVar0 = Dau_DsdFindVarDef( pVars, nVars, VarId );
1801 ABC_SWAP( int, pVars[iVar0], pVars[nVars-1] );
1802 Abc_TtSwapVars( pTruth, nVars, iVar0, nVars-1 ); nVars--;
1803 // find the new var
1804 v = Dau_DsdFindVarDef( pVars, nVars, p->nVarsUsed-1 );
1805 // remove single variables if possible
1806 if ( Dau_DsdDecomposeSingleVarOne( p, pTruth, pVars, nVars, v ) )
1807 nVars = Dau_DsdDecomposeSingleVar( p, pTruth, pVars, --nVars );
1808 return nVars;
1809 }
1810 return nVars;
1811 }
Dau_DsdDecomposeTripleVars(Dau_Dsd_t * p,word * pTruth,int * pVars,int nVars)1812 int Dau_DsdDecomposeTripleVars( Dau_Dsd_t * p, word * pTruth, int * pVars, int nVars )
1813 {
1814 abctime clk = Abc_Clock();
1815 while ( 1 )
1816 {
1817 int v;
1818 // Kit_DsdPrintFromTruth( (unsigned *)pTruth, 6 ); printf( "\n" );
1819 for ( v = nVars - 1; v >= 0; v-- )
1820 {
1821 unsigned uSupports = Dau_DsdFindSupports( p, pTruth, pVars, nVars, v );
1822 // Dau_DsdPrintSupports( uSupports, nVars );
1823 if ( (uSupports & (uSupports >> 1) & 0x55555555) == 0 ) // non-overlapping supports
1824 return Dau_DsdDecomposeTripleVarsOuter( p, pTruth, pVars, nVars, v );
1825 if ( Abc_TtSuppOnlyOne( uSupports & (~uSupports >> 1) & 0x55555555) &&
1826 Abc_TtSuppOnlyOne(~uSupports & ( uSupports >> 1) & 0x55555555) ) // one unique variable in each cofactor
1827 {
1828 int nVarsNew = Dau_DsdDecomposeTripleVarsInner( p, pTruth, pVars, nVars, v, uSupports );
1829 if ( nVarsNew == nVars )
1830 continue;
1831 if ( nVarsNew == 0 )
1832 {
1833 s_Times[2] += Abc_Clock() - clk;
1834 return 0;
1835 }
1836 nVars = Dau_DsdDecomposeDoubleVars( p, pTruth, pVars, nVarsNew );
1837 if ( nVars == 0 )
1838 {
1839 s_Times[2] += Abc_Clock() - clk;
1840 return 0;
1841 }
1842 break;
1843 }
1844 }
1845 if ( v == -1 )
1846 {
1847 s_Times[2] += Abc_Clock() - clk;
1848 return nVars;
1849 }
1850 }
1851 assert( 0 );
1852 return -1;
1853 }
Dau_DsdDecomposeInternal(Dau_Dsd_t * p,word * pTruth,int * pVars,int nVars)1854 int Dau_DsdDecomposeInternal( Dau_Dsd_t * p, word * pTruth, int * pVars, int nVars )
1855 {
1856 // decompose single variales on the output side
1857 nVars = Dau_DsdDecomposeSingleVar( p, pTruth, pVars, nVars );
1858 if ( nVars == 0 )
1859 return 0;
1860 // decompose double variables on the input side
1861 nVars = Dau_DsdDecomposeDoubleVars( p, pTruth, pVars, nVars );
1862 if ( nVars == 0 )
1863 return 0;
1864 // decompose MUX on the output/input side
1865 nVars = Dau_DsdDecomposeTripleVars( p, pTruth, pVars, nVars );
1866 if ( nVars == 0 )
1867 return 0;
1868 // write non-decomposable function
1869 return Dau_DsdWritePrime( p, pTruth, pVars, nVars );
1870 }
1871
1872 /**Function*************************************************************
1873
1874 Synopsis [Fast DSD for truth tables.]
1875
1876 Description []
1877
1878 SideEffects []
1879
1880 SeeAlso []
1881
1882 ***********************************************************************/
Dau_DsdMinBase(word * pTruth,int nVars,int * pVarsNew)1883 int Dau_DsdMinBase( word * pTruth, int nVars, int * pVarsNew )
1884 {
1885 int v;
1886 for ( v = 0; v < nVars; v++ )
1887 pVarsNew[v] = v;
1888 for ( v = nVars - 1; v >= 0; v-- )
1889 {
1890 if ( Abc_TtHasVar( pTruth, nVars, v ) )
1891 continue;
1892 Abc_TtSwapVars( pTruth, nVars, v, nVars-1 );
1893 pVarsNew[v] = pVarsNew[--nVars];
1894 }
1895 return nVars;
1896 }
Dau_DsdDecomposeInt(Dau_Dsd_t * p,word * pTruth,int nVarsInit)1897 int Dau_DsdDecomposeInt( Dau_Dsd_t * p, word * pTruth, int nVarsInit )
1898 {
1899 int Status = 0, nVars, pVars[16];
1900 Dau_DsdInitialize( p, nVarsInit );
1901 nVars = Dau_DsdMinBase( pTruth, nVarsInit, pVars );
1902 assert( nVars > 0 && nVars <= nVarsInit );
1903 if ( nVars == 1 )
1904 Dau_DsdWriteVar( p, pVars[0], (int)(pTruth[0] & 1) );
1905 else if ( nVars <= 6 )
1906 Status = Dau_Dsd6DecomposeInternal( p, pTruth, pVars, nVars );
1907 else
1908 Status = Dau_DsdDecomposeInternal( p, pTruth, pVars, nVars );
1909 Dau_DsdFinalize( p );
1910 return Status;
1911 }
Dau_DsdDecompose(word * pTruth,int nVarsInit,int fSplitPrime,int fWriteTruth,char * pRes)1912 int Dau_DsdDecompose( word * pTruth, int nVarsInit, int fSplitPrime, int fWriteTruth, char * pRes )
1913 {
1914 Dau_Dsd_t P, * p = &P;
1915 p->fSplitPrime = fSplitPrime;
1916 p->fWriteTruth = fWriteTruth;
1917 p->pVarLevels = NULL;
1918 p->nSizeNonDec = 0;
1919 if ( (pTruth[0] & 1) == 0 && Abc_TtIsConst0(pTruth, Abc_TtWordNum(nVarsInit)) )
1920 { if ( pRes ) pRes[0] = '0', pRes[1] = 0; }
1921 else if ( (pTruth[0] & 1) && Abc_TtIsConst1(pTruth, Abc_TtWordNum(nVarsInit)) )
1922 { if ( pRes ) pRes[0] = '1', pRes[1] = 0; }
1923 else
1924 {
1925 int Status = Dau_DsdDecomposeInt( p, pTruth, nVarsInit );
1926 Dau_DsdRemoveBraces( p->pOutput, Dau_DsdComputeMatches(p->pOutput) );
1927 if ( pRes )
1928 strcpy( pRes, p->pOutput );
1929 assert( fSplitPrime || Status != 1 );
1930 if ( fSplitPrime && Status == 2 )
1931 return -1;
1932 }
1933 // assert( p->nSizeNonDec == 0 );
1934 return p->nSizeNonDec;
1935 }
Dau_DsdDecomposeLevel(word * pTruth,int nVarsInit,int fSplitPrime,int fWriteTruth,char * pRes,int * pVarLevels)1936 int Dau_DsdDecomposeLevel( word * pTruth, int nVarsInit, int fSplitPrime, int fWriteTruth, char * pRes, int * pVarLevels )
1937 {
1938 Dau_Dsd_t P, * p = &P;
1939 p->fSplitPrime = fSplitPrime;
1940 p->fWriteTruth = fWriteTruth;
1941 p->pVarLevels = pVarLevels;
1942 p->nSizeNonDec = 0;
1943 if ( (pTruth[0] & 1) == 0 && Abc_TtIsConst0(pTruth, Abc_TtWordNum(nVarsInit)) )
1944 { if ( pRes ) pRes[0] = '0', pRes[1] = 0; }
1945 else if ( (pTruth[0] & 1) && Abc_TtIsConst1(pTruth, Abc_TtWordNum(nVarsInit)) )
1946 { if ( pRes ) pRes[0] = '1', pRes[1] = 0; }
1947 else
1948 {
1949 int Status = Dau_DsdDecomposeInt( p, pTruth, nVarsInit );
1950 Dau_DsdRemoveBraces( p->pOutput, Dau_DsdComputeMatches(p->pOutput) );
1951 if ( pRes )
1952 strcpy( pRes, p->pOutput );
1953 assert( fSplitPrime || Status != 1 );
1954 if ( fSplitPrime && Status == 2 )
1955 return -1;
1956 }
1957 // assert( p->nSizeNonDec == 0 );
1958 return p->nSizeNonDec;
1959 }
Dau_DsdPrintFromTruthFile(FILE * pFile,word * pTruth,int nVarsInit)1960 void Dau_DsdPrintFromTruthFile( FILE * pFile, word * pTruth, int nVarsInit )
1961 {
1962 char pRes[DAU_MAX_STR];
1963 word pTemp[DAU_MAX_WORD];
1964 Abc_TtCopy( pTemp, pTruth, Abc_TtWordNum(nVarsInit), 0 );
1965 Dau_DsdDecompose( pTemp, nVarsInit, 0, 1, pRes );
1966 fprintf( pFile, "%s\n", pRes );
1967 }
Dau_DsdPrintFromTruth(word * pTruth,int nVarsInit)1968 void Dau_DsdPrintFromTruth( word * pTruth, int nVarsInit )
1969 {
1970 char pRes[DAU_MAX_STR];
1971 word pTemp[DAU_MAX_WORD];
1972 Abc_TtCopy( pTemp, pTruth, Abc_TtWordNum(nVarsInit), 0 );
1973 Dau_DsdDecompose( pTemp, nVarsInit, 0, 1, pRes );
1974 fprintf( stdout, "%s\n", pRes );
1975 }
1976
Dau_DsdTest44()1977 void Dau_DsdTest44()
1978 {
1979 char pRes[DAU_MAX_STR];
1980 // char * pStr = "(!(!a<bcd>)!(!fe))";
1981 // char * pStr = "([acb]<!edf>)";
1982 // char * pStr = "!(f!(b!c!(d[ea])))";
1983 // char * pStr = "[!(a[be])!(c!df)]";
1984 // char * pStr = "<(e<bca>)fd>";
1985 // char * pStr = "[d8001{abef}c]";
1986 char * pStr = "[dc<a(cbd)(!c!b!d)>{abef}]";
1987 // char * pStr3;
1988 word t = Dau_Dsd6ToTruth( pStr );
1989 // return;
1990 int nNonDec = Dau_DsdDecompose( &t, 6, 1, 1, pRes );
1991 // Dau_DsdNormalize( pStr2 );
1992 // Dau_DsdExtract( pStr, 2, 0 );
1993 t = 0;
1994 nNonDec = 0;
1995 }
1996
1997
1998
Dau_DsdTest888()1999 void Dau_DsdTest888()
2000 {
2001 char pDsd[DAU_MAX_STR];
2002 int nVars = 9;
2003 // char * pStr = "[(abc)(def)(ghi)]";
2004 // char * pStr = "[a!b!(c!d[e(fg)hi])]";
2005 // char * pStr = "[(abc)(def)]";
2006 // char * pStr = "[(abc)(def)]";
2007 // char * pStr = "[abcdefg]";
2008 // char * pStr = "[<abc>(de[ghi])]";
2009 char * pStr = "(<abc>(<def><ghi>))";
2010 word * pTruth = Dau_DsdToTruth( pStr, 9 );
2011 int i, Status;
2012 // Kit_DsdPrintFromTruth( (unsigned *)pTruth, 9 ); printf( "\n" );
2013 /*
2014 for ( i = 0; i < 6; i++ )
2015 {
2016 unsigned uSupp = Dau_Dsd6FindSupports( NULL, pTruth, NULL, 6, i );
2017 Dau_DsdPrintSupports( uSupp, 6 );
2018 }
2019 */
2020 /*
2021 printf( "\n" );
2022 for ( i = 0; i < nVars; i++ )
2023 {
2024 unsigned uSupp = Dau_DsdFindSupports( NULL, pTruth, NULL, nVars, i );
2025 Dau_DsdPrintSupports( uSupp, nVars );
2026 }
2027 */
2028 Status = Dau_DsdDecompose( pTruth, nVars, 0, 0, pDsd );
2029 i = 0;
2030 }
2031
Dau_DsdTest555()2032 void Dau_DsdTest555()
2033 {
2034 int nVars = 10;
2035 int nWords = Abc_TtWordNum(nVars);
2036 char * pFileName = "_npn/npn/dsd10.txt";
2037 FILE * pFile = fopen( pFileName, "rb" );
2038 word Tru[2][DAU_MAX_WORD], * pTruth;
2039 char pBuffer[DAU_MAX_STR];
2040 char pRes[DAU_MAX_STR];
2041 int nSizeNonDec;
2042 int i, Counter = 0;
2043 abctime clk = Abc_Clock(), clkDec = 0, clk2;
2044 // return;
2045
2046 while ( fgets( pBuffer, DAU_MAX_STR, pFile ) != NULL )
2047 {
2048 char * pStr2 = pBuffer + strlen(pBuffer)-1;
2049 if ( *pStr2 == '\n' )
2050 *pStr2-- = 0;
2051 if ( *pStr2 == '\r' )
2052 *pStr2-- = 0;
2053 if ( pBuffer[0] == 'V' || pBuffer[0] == 0 )
2054 continue;
2055 Counter++;
2056
2057 for ( i = 0; i < 1; i++ )
2058 {
2059 // Dau_DsdPermute( pBuffer );
2060 pTruth = Dau_DsdToTruth( pBuffer[0] == '*' ? pBuffer + 1 : pBuffer, nVars );
2061 Abc_TtCopy( Tru[0], pTruth, nWords, 0 );
2062 Abc_TtCopy( Tru[1], pTruth, nWords, 0 );
2063 clk2 = Abc_Clock();
2064 nSizeNonDec = Dau_DsdDecompose( Tru[1], nVars, 0, 1, pRes );
2065 clkDec += Abc_Clock() - clk2;
2066 Dau_DsdNormalize( pRes );
2067 // pStr2 = Dau_DsdPerform( t ); nSizeNonDec = 0;
2068 assert( nSizeNonDec == 0 );
2069 pTruth = Dau_DsdToTruth( pRes, nVars );
2070 if ( !Abc_TtEqual( pTruth, Tru[0], nWords ) )
2071 {
2072 // Kit_DsdPrintFromTruth( (unsigned *)&t, 6 );
2073 // printf( " " );
2074 // Kit_DsdPrintFromTruth( (unsigned *)&t2, 6 );
2075 printf( "%s -> %s \n", pBuffer, pRes );
2076 printf( "Verification failed.\n" );
2077 }
2078 }
2079 }
2080 printf( "Finished trying %d decompositions. ", Counter );
2081 Abc_PrintTime( 1, "Time", clkDec );
2082 Abc_PrintTime( 1, "Total", Abc_Clock() - clk );
2083
2084 Abc_PrintTime( 1, "Time1", s_Times[0] );
2085 Abc_PrintTime( 1, "Time2", s_Times[1] );
2086 Abc_PrintTime( 1, "Time3", s_Times[2] );
2087
2088 fclose( pFile );
2089 }
2090
2091 ////////////////////////////////////////////////////////////////////////
2092 /// END OF FILE ///
2093 ////////////////////////////////////////////////////////////////////////
2094
2095
2096 ABC_NAMESPACE_IMPL_END
2097
2098
2099