abc-master
 All Data Structures Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros
dauDsd.c
Go to the documentation of this file.
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 ***********************************************************************/
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 ***********************************************************************/
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 ***********************************************************************/
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 }
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 }
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 ***********************************************************************/
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 }
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 }
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 }
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, 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 }
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 ***********************************************************************/
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 }
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 ***********************************************************************/
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 }
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 }
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 ***********************************************************************/
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 }
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 }
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 }
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 ***********************************************************************/
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 ***********************************************************************/
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 }
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 }
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 ***********************************************************************/
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 ***********************************************************************/
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 ***********************************************************************/
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 }
1002 static inline void Dau_DsdWriteString( Dau_Dsd_t * p, char * pStr )
1003 {
1004  while ( *pStr )
1005  p->pOutput[ p->nPos++ ] = *pStr++;
1006 }
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 }
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 }
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 }
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 }
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 }
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 }
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 }
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 }
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 ***********************************************************************/
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 }
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 }
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 }
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 }
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)
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 }
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
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 }
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 }
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 }
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 ***********************************************************************/
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 }
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 
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 }
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)
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 }
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
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 }
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 }
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 }
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 ***********************************************************************/
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 }
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 }
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 }
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 }
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 }
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 
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 
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 
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 
pTruths
static ABC_NAMESPACE_IMPL_START int pTruths[13719]
DECLARATIONS ///.
Definition: rwrTemp.c:30
Dau_DsdAddVarDef
static int Dau_DsdAddVarDef(Dau_Dsd_t *p, char *pStr)
Definition: dauDsd.c:1090
Abc_TtCheckEqualCofs
static int Abc_TtCheckEqualCofs(word *pTruth, int nWords, int iVar, int jVar, int Num1, int Num2)
Definition: utilTruth.h:475
Abc_Tt6Cof1IsConst0
static int Abc_Tt6Cof1IsConst0(word t, int iVar)
Definition: utilTruth.h:540
Dau_DsdDecomposeTripleVars
int Dau_DsdDecomposeTripleVars(Dau_Dsd_t *p, word *pTruth, int *pVars, int nVars)
Definition: dauDsd.c:1812
Dau_Dsd6DecomposeTripleVarsOuter
static int Dau_Dsd6DecomposeTripleVarsOuter(Dau_Dsd_t *p, word *pTruth, int *pVars, int nVars, int v)
Definition: dauDsd.c:1353
Dau_DsdPrintSupports
static void Dau_DsdPrintSupports(unsigned uSupp, int nVars)
Definition: dauDsd.c:1236
Abc_TtSuppFindFirst
static int Abc_TtSuppFindFirst(int Supp)
Definition: utilTruth.h:929
Dau_Dsd_t
typedefABC_NAMESPACE_IMPL_START struct Dau_Dsd_t_ Dau_Dsd_t
DECLARATIONS ///.
Definition: dauArray.c:29
Dau_Dsd_t_::nConsts
int nConsts
Definition: dauDsd.c:962
Dau_DsdDecompose
int Dau_DsdDecompose(word *pTruth, int nVarsInit, int fSplitPrime, int fWriteTruth, char *pRes)
Definition: dauDsd.c:1912
Dau_DsdPrintFromTruthFile
void Dau_DsdPrintFromTruthFile(FILE *pFile, word *pTruth, int nVarsInit)
Definition: dauDsd.c:1960
Dau_Dsd_t_::Cache
char Cache[32][32]
Definition: dauDsd.c:968
Dau_DsdDecomposeTripleVarsInner
static int Dau_DsdDecomposeTripleVarsInner(Dau_Dsd_t *p, word *pTruth, int *pVars, int nVars, int v, unsigned uSupports)
Definition: dauDsd.c:1764
Dau_DsdTest2
void Dau_DsdTest2()
Definition: dauDsd.c:637
Dau_Dsd6FindSupportOne
static int Dau_Dsd6FindSupportOne(Dau_Dsd_t *p, word tCof0, word tCof1, int *pVars, int nVars, int v, int u)
Definition: dauDsd.c:1212
p
static Llb_Mgr_t * p
Definition: llb3Image.c:950
Abc_TtCofactor1p
static void Abc_TtCofactor1p(word *pOut, word *pIn, int nWords, int iVar)
Definition: utilTruth.h:403
Abc_Tt6HasVar
static int Abc_Tt6HasVar(word t, int iVar)
Definition: utilTruth.h:949
P
static byte P[256]
Definition: kitPerm.c:76
Pos
ush Pos
Definition: deflate.h:88
Dau_DsdFindVarDef
static int Dau_DsdFindVarDef(int *pVars, int nVars, int VarDef)
Definition: dauDsd.c:1102
Abc_Tt6Cof0IsConst1
static int Abc_Tt6Cof0IsConst1(word t, int iVar)
Definition: utilTruth.h:539
Dau_DsdLevelVar
int Dau_DsdLevelVar(void *pMan, int iVar)
Definition: dauDsd.c:1018
Dau_DsdInsertVarCache
static void Dau_DsdInsertVarCache(Dau_Dsd_t *p, int v, int u, int Status)
Definition: dauDsd.c:1111
Abc_TtCof0IsConst0
static int Abc_TtCof0IsConst0(word *t, int nWords, int iVar)
Definition: utilTruth.h:561
Abc_TtIsConst0
static int Abc_TtIsConst0(word *pIn1, int nWords)
Definition: utilTruth.h:293
Dau_Dsd6DecomposeInternal
int Dau_Dsd6DecomposeInternal(Dau_Dsd_t *p, word *pTruth, int *pVars, int nVars)
Definition: dauDsd.c:1461
Dau_DsdDecomposeTripleVarsOuter
static int Dau_DsdDecomposeTripleVarsOuter(Dau_Dsd_t *p, word *pTruth, int *pVars, int nVars, int v)
Definition: dauDsd.c:1730
Dau_DsdTruth6Compose_rec
void Dau_DsdTruth6Compose_rec(word Func, word pFanins[DAU_MAX_VAR][DAU_MAX_WORD], word *pRes, int nVars, int nWordsR)
Definition: dauDsd.c:469
memcpy
char * memcpy()
Dau_DsdTest44
void Dau_DsdTest44()
Definition: dauDsd.c:1977
Dau_DsdRemoveBraces
void Dau_DsdRemoveBraces(char *pDsd, int *pMatches)
Definition: dauMerge.c:554
Dau_DsdFindSupportOne
static int Dau_DsdFindSupportOne(Dau_Dsd_t *p, word *pTruth, int *pVars, int nVars, int v, int u)
Definition: dauDsd.c:1572
Dau_DsdNormalizeCompare
int Dau_DsdNormalizeCompare(char *pStr, int *pMarks, int i, int j)
Definition: dauDsd.c:158
Abc_Clock
static abctime Abc_Clock()
Definition: abc_global.h:279
Abc_Tt6Cofactor0
static word Abc_Tt6Cofactor0(word t, int iVar)
Definition: utilTruth.h:370
Abc_MaxInt
static int Abc_MaxInt(int a, int b)
Definition: abc_global.h:238
Dau_Dsd6DecomposeTripleVarsInner
static int Dau_Dsd6DecomposeTripleVarsInner(Dau_Dsd_t *p, word *pTruth, int *pVars, int nVars, int v, unsigned uSupports)
Definition: dauDsd.c:1384
Dau_Dsd_t_::fSplitPrime
int fSplitPrime
Definition: dauDsd.c:964
Dau_Dsd_t_::nVarsInit
int nVarsInit
Definition: dauDsd.c:958
nWords
int nWords
Definition: abcNpn.c:127
Abc_TtConst1
static void Abc_TtConst1(word *pIn1, int nWords)
Definition: utilTruth.h:315
for
for(p=first;p->value< newval;p=p->next)
Abc_TtIsConst1
static int Abc_TtIsConst1(word *pIn1, int nWords)
Definition: utilTruth.h:301
ABC_SWAP
#define ABC_SWAP(Type, a, b)
Definition: abc_global.h:218
Dau_DsdNormalize_rec
void Dau_DsdNormalize_rec(char *pStr, char **p, int *pMatches)
Definition: dauDsd.c:205
Dau_DsdCountAnds
int Dau_DsdCountAnds(char *pDsd)
Definition: dauDsd.c:316
Dau_DsdMinBase
int Dau_DsdMinBase(word *pTruth, int nVars, int *pVarsNew)
Definition: dauDsd.c:1883
Dau_DsdFinalize
static void Dau_DsdFinalize(Dau_Dsd_t *p)
Definition: dauDsd.c:1083
Dau_DsdTranslate
static void Dau_DsdTranslate(Dau_Dsd_t *p, int *pVars, int nVars, char *pStr)
Definition: dauDsd.c:1033
Dau_DsdGenRandPerm
void Dau_DsdGenRandPerm(int *pPerm, int nVars)
Definition: dauDsd.c:118
Abc_TtReadHex
static int Abc_TtReadHex(word *pTruth, char *pString)
Definition: utilTruth.h:838
Abc_TtCof1IsConst1
static int Abc_TtCof1IsConst1(word *t, int nWords, int iVar)
Definition: utilTruth.h:624
Abc_PrintTime
static void Abc_PrintTime(int level, const char *pStr, abctime time)
Definition: abc_global.h:367
Dau_DsdDecomposeDoubleVarsOne
static int Dau_DsdDecomposeDoubleVarsOne(Dau_Dsd_t *p, word *pTruth, int *pVars, int nVars, int v, int u)
Definition: dauDsd.c:1602
Dau_DsdToTruth
word * Dau_DsdToTruth(char *p, int nVars)
Definition: dauDsd.c:609
Dau_DsdInitialize
static void Dau_DsdInitialize(Dau_Dsd_t *p, int nVarsInit)
Definition: dauDsd.c:985
DAU_MAX_STR
#define DAU_MAX_STR
Definition: dau.h:43
Abc_TtWriteHexRev
static int Abc_TtWriteHexRev(char *pStr, word *pTruth, int nVars)
Definition: utilTruth.h:809
Abc_TtHexDigitNum
static int Abc_TtHexDigitNum(int nVars)
Definition: utilTruth.h:171
Abc_TtCopy
static void Abc_TtCopy(word *pOut, word *pIn, int nWords, int fCompl)
Definition: utilTruth.h:221
Abc_Tt6Cofactor1
static word Abc_Tt6Cofactor1(word t, int iVar)
Definition: utilTruth.h:375
Dau_DsdTest3
void Dau_DsdTest3()
Definition: dauDsd.c:858
Abc_TtCof0IsConst1
static int Abc_TtCof0IsConst1(word *t, int nWords, int iVar)
Definition: utilTruth.h:582
Abc_TtCofactor0p
static void Abc_TtCofactor0p(word *pOut, word *pIn, int nWords, int iVar)
Definition: utilTruth.h:381
DAU_MAX_VAR
#define DAU_MAX_VAR
INCLUDES ///.
Definition: dau.h:42
Abc_Tt6Cof0IsConst0
static int Abc_Tt6Cof0IsConst0(word t, int iVar)
Definition: utilTruth.h:538
Dau_Dsd6DecomposeTripleVars
int Dau_Dsd6DecomposeTripleVars(Dau_Dsd_t *p, word *pTruth, int *pVars, int nVars)
Definition: dauDsd.c:1419
Dau_DsdDecomposeDoubleVars
int Dau_DsdDecomposeDoubleVars(Dau_Dsd_t *p, word *pTruth, int *pVars, int nVars)
Definition: dauDsd.c:1697
Dau_Dsd6DecomposeDoubleVarsOne
static int Dau_Dsd6DecomposeDoubleVarsOne(Dau_Dsd_t *p, word *pTruth, int *pVars, int nVars, int v, int u)
Definition: dauDsd.c:1257
word
unsigned __int64 word
DECLARATIONS ///.
Definition: kitPerm.c:36
Dau_Dsd_t_::pVarLevels
int * pVarLevels
Definition: dauDsd.c:966
Dau_DsdNormalize
void Dau_DsdNormalize(char *pDsd)
Definition: dauDsd.c:260
ABC_NAMESPACE_IMPL_END
#define ABC_NAMESPACE_IMPL_END
Definition: abc_global.h:108
Dau_DsdTtElems
static ABC_NAMESPACE_IMPL_START word ** Dau_DsdTtElems()
DECLARATIONS ///.
Definition: dauDsd.c:56
Abc_Tt6Cof1IsConst1
static int Abc_Tt6Cof1IsConst1(word t, int iVar)
Definition: utilTruth.h:541
Vec_IntSelectSortCost2
static void Vec_IntSelectSortCost2(int *pArray, int nSize, int *pCosts)
Definition: vecInt.h:1778
sprintf
char * sprintf()
Counter
static int Counter
Definition: extraBddMisc.c:1877
Dau_DsdLookupVarCache
static int Dau_DsdLookupVarCache(Dau_Dsd_t *p, int v, int u)
Definition: dauDsd.c:1118
Dau_Dsd6FindSupports
static unsigned Dau_Dsd6FindSupports(Dau_Dsd_t *p, word *pTruth, int *pVars, int nVars, int v)
Definition: dauDsd.c:1223
Dau_DsdFindSupports
static unsigned Dau_DsdFindSupports(Dau_Dsd_t *p, word *pTruth, int *pVars, int nVars, int v)
Definition: dauDsd.c:1589
Dau_DsdPerform
char * Dau_DsdPerform(word t)
Definition: dauDsd.c:828
Dau_DsdNormalizePerm
int * Dau_DsdNormalizePerm(char *pStr, int *pMarks, int nMarks)
Definition: dauDsd.c:189
Abc_TtHasVar
static int Abc_TtHasVar(word *t, int nVars, int iVar)
Definition: utilTruth.h:953
Dau_DsdWritePrime
static int Dau_DsdWritePrime(Dau_Dsd_t *p, word *pTruth, int *pVars, int nVars)
Definition: dauDsd.c:1041
s_Truths6Neg
static word s_Truths6Neg[6]
Definition: utilTruth.h:47
Abc_TtCofactor0
static void Abc_TtCofactor0(word *pTruth, int nWords, int iVar)
Definition: utilTruth.h:425
pPerm
static int pPerm[13719]
Definition: rwrTemp.c:32
strcpy
char * strcpy()
Dau_DsdFindVarNum
int Dau_DsdFindVarNum(char *pDsd)
Definition: dauDsd.c:109
ABC_NAMESPACE_IMPL_START
#define ABC_NAMESPACE_IMPL_START
Definition: abc_global.h:107
Dau_DsdPermute
void Dau_DsdPermute(char *pDsd)
Definition: dauDsd.c:129
Dau_Dsd6ToTruth_rec
word Dau_Dsd6ToTruth_rec(char *pStr, char **p, int *pMatches, word *pTruths)
Definition: dauDsd.c:353
DAU_MAX_WORD
#define DAU_MAX_WORD
Definition: dau.h:44
Dau_DsdPerform_rec
int Dau_DsdPerform_rec(word t, char *pBuffer, int Pos, int *pVars, int nVars)
Definition: dauDsd.c:673
Dau_Dsd_t_::pVarDefs
char pVarDefs[32][8]
Definition: dauDsd.c:967
Dau_DsdPrintFromTruth
void Dau_DsdPrintFromTruth(word *pTruth, int nVarsInit)
Definition: dauDsd.c:1968
Abc_Tt6CofsOpposite
static int Abc_Tt6CofsOpposite(word t, int iVar)
Definition: utilTruth.h:542
s_Truths6
static word s_Truths6[6]
Definition: extraUtilEnum.c:430
Dau_DsdIsConst1
static int Dau_DsdIsConst1(char *p)
Definition: dau.h:69
Dau_DsdNormalizeCopy
char * Dau_DsdNormalizeCopy(char *pDest, char *pSour, int *pMarks, int i)
Definition: dauDsd.c:151
Dau_DsdDecomposeInt
int Dau_DsdDecomposeInt(Dau_Dsd_t *p, word *pTruth, int nVarsInit)
Definition: dauDsd.c:1897
Abc_TtWordNum
static int Abc_TtWordNum(int nVars)
Definition: utilTruth.h:169
Dau_DsdTest555
void Dau_DsdTest555()
Definition: dauDsd.c:2032
Dau_DsdDecomposeInternal
int Dau_DsdDecomposeInternal(Dau_Dsd_t *p, word *pTruth, int *pVars, int nVars)
Definition: dauDsd.c:1854
Dau_DsdWriteString
static void Dau_DsdWriteString(Dau_Dsd_t *p, char *pStr)
Definition: dauDsd.c:1002
ABC_CONST
#define ABC_CONST(number)
PARAMETERS ///.
Definition: abc_global.h:206
Abc_TtMux
static void Abc_TtMux(word *pOut, word *pCtrl, word *pIn1, word *pIn0, int nWords)
Definition: utilTruth.h:263
Abc_TtCofactor1
static void Abc_TtCofactor1(word *pTruth, int nWords, int iVar)
Definition: utilTruth.h:444
Dau_Dsd6DecomposeSingleVar
int Dau_Dsd6DecomposeSingleVar(Dau_Dsd_t *p, word *pTruth, int *pVars, int nVars)
Definition: dauDsd.c:1191
Dau_DsdDecomposeSingleVar
int Dau_DsdDecomposeSingleVar(Dau_Dsd_t *p, word *pTruth, int *pVars, int nVars)
Definition: dauDsd.c:1550
Dau_DsdDecomposeSingleVarOne
static int Dau_DsdDecomposeSingleVarOne(Dau_Dsd_t *p, word *pTruth, int *pVars, int nVars, int v)
Definition: dauDsd.c:1490
Abc_TtEqual
static int Abc_TtEqual(word *pIn1, word *pIn2, int nWords)
Definition: utilTruth.h:269
Abc_TtConst0
static void Abc_TtConst0(word *pIn1, int nWords)
Definition: utilTruth.h:309
Abc_TtCofsOpposite
static int Abc_TtCofsOpposite(word *t, int nWords, int iVar)
Definition: utilTruth.h:645
Dau_DsdWriteVar
static void Dau_DsdWriteVar(Dau_Dsd_t *p, int iVar, int fInv)
Definition: dauDsd.c:1007
Dau_DsdTruthCompose_rec
void Dau_DsdTruthCompose_rec(word *pFunc, word pFanins[DAU_MAX_VAR][DAU_MAX_WORD], word *pRes, int nVars, int nWordsR)
Definition: dauDsd.c:501
Dau_Dsd_t_::nVarsUsed
int nVarsUsed
Definition: dauDsd.c:959
Abc_TtSupportSize
static int Abc_TtSupportSize(word *t, int nVars)
Definition: utilTruth.h:986
Abc_TtSuppOnlyOne
static int Abc_TtSuppOnlyOne(int Supp)
Definition: utilTruth.h:938
Dau_Dsd_t_::fWriteTruth
int fWriteTruth
Definition: dauDsd.c:965
Dau_DsdTest888
void Dau_DsdTest888()
Definition: dauDsd.c:1999
Abc_Tt6Cof0EqualCof0
static int Abc_Tt6Cof0EqualCof0(word t1, word t2, int iVar)
Definition: utilTruth.h:544
Dau_DsdDecomposeLevel
int Dau_DsdDecomposeLevel(word *pTruth, int nVarsInit, int fSplitPrime, int fWriteTruth, char *pRes, int *pVarLevels)
Definition: dauDsd.c:1936
Dau_Dsd_t_::nPos
int nPos
Definition: dauDsd.c:960
ABC_INFINITY
#define ABC_INFINITY
MACRO DEFINITIONS ///.
Definition: abc_global.h:216
Dau_DsdToTruth_rec
void Dau_DsdToTruth_rec(char *pStr, char **p, int *pMatches, word **pTtElems, word *pRes, int nVars)
Definition: dauDsd.c:535
Dau_Dsd_t_::uConstMask
int uConstMask
Definition: dauDsd.c:963
assert
#define assert(ex)
Definition: util_old.h:213
Abc_TtCof1IsConst0
static int Abc_TtCof1IsConst0(word *t, int nWords, int iVar)
Definition: utilTruth.h:603
strlen
int strlen()
Dau_Dsd_t_
Definition: dauArray.c:30
Dau_Dsd_t_::pOutput
char pOutput[DAU_MAX_STR]
Definition: dauDsd.c:969
Abc_Tt6Cof0EqualCof1
static int Abc_Tt6Cof0EqualCof1(word t1, word t2, int iVar)
Definition: utilTruth.h:543
Dau_DsdIsConst0
static int Dau_DsdIsConst0(char *p)
Definition: dau.h:68
Abc_TtSwapVars
static void Abc_TtSwapVars(word *pTruth, int nVars, int iVar, int jVar)
Definition: utilTruth.h:1228
s_Times
static abctime s_Times[3]
Definition: dauDsd.c:972
Abc_TtAnd
static void Abc_TtAnd(word *pOut, word *pIn1, word *pIn2, int nWords, int fCompl)
Definition: utilTruth.h:231
Dau_Dsd6DecomposeSingleVarOne
static int Dau_Dsd6DecomposeSingleVarOne(Dau_Dsd_t *p, word *pTruth, int *pVars, int nVars, int v)
Definition: dauDsd.c:1134
Dau_DsdCheck1Step
int Dau_DsdCheck1Step(void *p, word *pTruth, int nVarsInit, int *pVarLevels)
Definition: dauDsd.c:893
abctime
ABC_INT64_T abctime
Definition: abc_global.h:278
Dau_DsdComputeMatches
int * Dau_DsdComputeMatches(char *p)
Definition: dauDsd.c:80
Abc_Tt6Cof1EqualCof1
static int Abc_Tt6Cof1EqualCof1(word t1, word t2, int iVar)
Definition: utilTruth.h:545
Dau_Dsd6TruthCompose_rec
word Dau_Dsd6TruthCompose_rec(word Func, word *pFanins, int nVars)
Definition: dauDsd.c:334
Abc_TtXor
static void Abc_TtXor(word *pOut, word *pIn1, word *pIn2, int nWords, int fCompl)
Definition: utilTruth.h:253
Dau_DsdPerformReplace
static int Dau_DsdPerformReplace(char *pBuffer, int PosStart, int Pos, int Symb, char *pNext)
Definition: dauDsd.c:657
Dau_DsdCountAnds_rec
int Dau_DsdCountAnds_rec(char *pStr, char **p, int *pMatches)
Definition: dauDsd.c:279
Abc_TtElemInit
static void Abc_TtElemInit(word **pTtElems, int nVars)
Definition: utilTruth.h:333
Abc_TtNot
static void Abc_TtNot(word *pOut, int nWords)
Definition: utilTruth.h:215
Dau_Dsd6DecomposeDoubleVars
int Dau_Dsd6DecomposeDoubleVars(Dau_Dsd_t *p, word *pTruth, int *pVars, int nVars)
Definition: dauDsd.c:1320
Dau_Dsd6ToTruth
word Dau_Dsd6ToTruth(char *p)
Definition: dauDsd.c:445
Dau_Dsd_t_::nSizeNonDec
int nSizeNonDec
Definition: dauDsd.c:961