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