1 /**CFile****************************************************************
2
3 FileName [dauMerge.c]
4
5 SystemName [ABC: Logic synthesis and verification system.]
6
7 PackageName [DAG-aware unmapping.]
8
9 Synopsis [Enumeration of decompositions.]
10
11 Author [Alan Mishchenko]
12
13 Affiliation [UC Berkeley]
14
15 Date [Ver. 1.0. Started - June 20, 2005.]
16
17 Revision [$Id: dauMerge.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 ////////////////////////////////////////////////////////////////////////
32 /// FUNCTION DEFINITIONS ///
33 ////////////////////////////////////////////////////////////////////////
34
35
36 /**Function*************************************************************
37
38 Synopsis [Substitution storage.]
39
40 Description []
41
42 SideEffects []
43
44 SeeAlso []
45
46 ***********************************************************************/
47 typedef struct Dau_Sto_t_ Dau_Sto_t;
48 struct Dau_Sto_t_
49 {
50 int iVarUsed; // counter of used variables
51 char pOutput[DAU_MAX_STR]; // storage for reduced function
52 char * pPosOutput; // place in the output
53 char pStore[DAU_MAX_VAR][DAU_MAX_STR]; // storage for definitions
54 char * pPosStore[DAU_MAX_VAR]; // place in the store
55 };
56
Dau_DsdMergeStoreClean(Dau_Sto_t * pS,int nShared)57 static inline void Dau_DsdMergeStoreClean( Dau_Sto_t * pS, int nShared )
58 {
59 int i;
60 pS->iVarUsed = nShared;
61 for ( i = 0; i < DAU_MAX_VAR; i++ )
62 pS->pStore[i][0] = 0;
63 }
64
Dau_DsdMergeStoreCleanOutput(Dau_Sto_t * pS)65 static inline void Dau_DsdMergeStoreCleanOutput( Dau_Sto_t * pS )
66 {
67 pS->pPosOutput = pS->pOutput;
68 }
Dau_DsdMergeStoreAddToOutput(Dau_Sto_t * pS,char * pBeg,char * pEnd)69 static inline void Dau_DsdMergeStoreAddToOutput( Dau_Sto_t * pS, char * pBeg, char * pEnd )
70 {
71 while ( pBeg < pEnd )
72 *pS->pPosOutput++ = *pBeg++;
73 }
Dau_DsdMergeStoreAddToOutputChar(Dau_Sto_t * pS,char c)74 static inline void Dau_DsdMergeStoreAddToOutputChar( Dau_Sto_t * pS, char c )
75 {
76 *pS->pPosOutput++ = c;
77 }
78
Dau_DsdMergeStoreStartDef(Dau_Sto_t * pS,char c)79 static inline int Dau_DsdMergeStoreStartDef( Dau_Sto_t * pS, char c )
80 {
81 pS->pPosStore[pS->iVarUsed] = pS->pStore[pS->iVarUsed];
82 if (c) *pS->pPosStore[pS->iVarUsed]++ = c;
83 return pS->iVarUsed++;
84 }
Dau_DsdMergeStoreAddToDef(Dau_Sto_t * pS,int New,char * pBeg,char * pEnd)85 static inline void Dau_DsdMergeStoreAddToDef( Dau_Sto_t * pS, int New, char * pBeg, char * pEnd )
86 {
87 while ( pBeg < pEnd )
88 *pS->pPosStore[New]++ = *pBeg++;
89 }
Dau_DsdMergeStoreAddToDefChar(Dau_Sto_t * pS,int New,char c)90 static inline void Dau_DsdMergeStoreAddToDefChar( Dau_Sto_t * pS, int New, char c )
91 {
92 *pS->pPosStore[New]++ = c;
93 }
Dau_DsdMergeStoreStopDef(Dau_Sto_t * pS,int New,char c)94 static inline void Dau_DsdMergeStoreStopDef( Dau_Sto_t * pS, int New, char c )
95 {
96 if (c) *pS->pPosStore[New]++ = c;
97 *pS->pPosStore[New]++ = 0;
98 }
99
Dau_DsdMergeStoreCreateDef(Dau_Sto_t * pS,char * pBeg,char * pEnd)100 static inline char Dau_DsdMergeStoreCreateDef( Dau_Sto_t * pS, char * pBeg, char * pEnd )
101 {
102 int New = Dau_DsdMergeStoreStartDef( pS, 0 );
103 Dau_DsdMergeStoreAddToDef( pS, New, pBeg, pEnd );
104 Dau_DsdMergeStoreStopDef( pS, New, 0 );
105 return New;
106 }
Dau_DsdMergeStorePrintDefs(Dau_Sto_t * pS)107 static inline void Dau_DsdMergeStorePrintDefs( Dau_Sto_t * pS )
108 {
109 int i;
110 for ( i = 0; i < DAU_MAX_VAR; i++ )
111 if ( pS->pStore[i][0] )
112 printf( "%c = %s\n", 'a' + i, pS->pStore[i] );
113 }
114
115 /**Function*************************************************************
116
117 Synopsis [Creates local copy.]
118
119 Description []
120
121 SideEffects []
122
123 SeeAlso []
124
125 ***********************************************************************/
Dau_DsdMergeCopy(char * pDsd,int fCompl,char * pRes)126 static inline void Dau_DsdMergeCopy( char * pDsd, int fCompl, char * pRes )
127 {
128 if ( fCompl && pDsd[0] == '!' )
129 fCompl = 0, pDsd++;
130 if ( Dau_DsdIsConst(pDsd) ) // constant
131 pRes[0] = (fCompl ? (char)((int)pDsd[0] ^ 1) : pDsd[0]), pRes[1] = 0;
132 else
133 sprintf( pRes, "%s%s", fCompl ? "!" : "", pDsd );
134 }
135
136 /**Function*************************************************************
137
138 Synopsis [Replaces variables according to the mapping.]
139
140 Description []
141
142 SideEffects []
143
144 SeeAlso []
145
146 ***********************************************************************/
Dau_DsdMergeReplace(char * pDsd,int * pMatches,int * pMap)147 static inline void Dau_DsdMergeReplace( char * pDsd, int * pMatches, int * pMap )
148 {
149 int i;
150 for ( i = 0; pDsd[i]; i++ )
151 {
152 // skip non-DSD block
153 if ( pDsd[i] == '<' && pDsd[pMatches[i]+1] == '{' )
154 i = pMatches[i] + 1;
155 if ( (pDsd[i] >= 'A' && pDsd[i] <= 'F') || (pDsd[i] >= '0' && pDsd[i] <= '9') )
156 while ( (pDsd[i] >= 'A' && pDsd[i] <= 'F') || (pDsd[i] >= '0' && pDsd[i] <= '9') )
157 i++;
158 // detect variables
159 if ( pDsd[i] >= 'a' && pDsd[i] <= 'z' )
160 pDsd[i] = 'a' + pMap[ pDsd[i] - 'a' ];
161 }
162 }
Dau_DsdMergeMatches(char * pDsd,int * pMatches)163 static inline void Dau_DsdMergeMatches( char * pDsd, int * pMatches )
164 {
165 int pNested[DAU_MAX_VAR];
166 int i, nNested = 0;
167 for ( i = 0; pDsd[i]; i++ )
168 {
169 pMatches[i] = 0;
170 if ( pDsd[i] == '(' || pDsd[i] == '[' || pDsd[i] == '<' || pDsd[i] == '{' )
171 pNested[nNested++] = i;
172 else if ( pDsd[i] == ')' || pDsd[i] == ']' || pDsd[i] == '>' || pDsd[i] == '}' )
173 pMatches[pNested[--nNested]] = i;
174 assert( nNested < DAU_MAX_VAR );
175 }
176 assert( nNested == 0 );
177 }
Dau_DsdMergeVarPres(char * pDsd,int * pMatches,int * pPres,int Mask)178 static inline void Dau_DsdMergeVarPres( char * pDsd, int * pMatches, int * pPres, int Mask )
179 {
180 int i;
181 for ( i = 0; pDsd[i]; i++ )
182 {
183 // skip non-DSD block
184 if ( pDsd[i] == '<' && pDsd[pMatches[i]+1] == '{' )
185 i = pMatches[i] + 1;
186 if ( (pDsd[i] >= 'A' && pDsd[i] <= 'F') || (pDsd[i] >= '0' && pDsd[i] <= '9') )
187 while ( (pDsd[i] >= 'A' && pDsd[i] <= 'F') || (pDsd[i] >= '0' && pDsd[i] <= '9') )
188 i++;
189 // skip non-variables
190 if ( !(pDsd[i] >= 'a' && pDsd[i] <= 'z') )
191 continue;
192 // record the mask
193 assert( pDsd[i]-'a' < DAU_MAX_VAR );
194 pPres[pDsd[i]-'a'] |= Mask;
195 }
196 }
Dau_DsdMergeCountShared(int * pPres,int Mask)197 static inline int Dau_DsdMergeCountShared( int * pPres, int Mask )
198 {
199 int i, Counter = 0;
200 for ( i = 0; i < DAU_MAX_VAR; i++ )
201 Counter += (pPres[i] == Mask);
202 return Counter;
203 }
Dau_DsdMergeFindShared(char * pDsd0,char * pDsd1,int * pMatches0,int * pMatches1,int * pVarPres)204 static inline int Dau_DsdMergeFindShared( char * pDsd0, char * pDsd1, int * pMatches0, int * pMatches1, int * pVarPres )
205 {
206 memset( pVarPres, 0, sizeof(int)*DAU_MAX_VAR );
207 Dau_DsdMergeVarPres( pDsd0, pMatches0, pVarPres, 1 );
208 Dau_DsdMergeVarPres( pDsd1, pMatches1, pVarPres, 2 );
209 return Dau_DsdMergeCountShared( pVarPres, 3 );
210 }
Dau_DsdMergeCreateMaps(int * pVarPres,int nShared,int * pOld2New,int * pNew2Old)211 static inline int Dau_DsdMergeCreateMaps( int * pVarPres, int nShared, int * pOld2New, int * pNew2Old )
212 {
213 int i, Counter = 0, Counter2 = nShared;
214 for ( i = 0; i < DAU_MAX_VAR; i++ )
215 {
216 if ( pVarPres[i] == 0 )
217 continue;
218 if ( pVarPres[i] == 3 )
219 {
220 pOld2New[i] = Counter;
221 pNew2Old[Counter] = i;
222 Counter++;
223 continue;
224 }
225 assert( pVarPres[i] == 1 || pVarPres[i] == 2 );
226 pOld2New[i] = Counter2;
227 pNew2Old[Counter2] = i;
228 Counter2++;
229 }
230 return Counter2;
231 }
Dau_DsdMergeInlineDefinitions(char * pDsd,int * pMatches,Dau_Sto_t * pS,char * pRes,int nShared)232 static inline void Dau_DsdMergeInlineDefinitions( char * pDsd, int * pMatches, Dau_Sto_t * pS, char * pRes, int nShared )
233 {
234 int i;
235 char * pDef;
236 char * pBegin = pRes;
237 for ( i = 0; pDsd[i]; i++ )
238 {
239 // skip non-DSD block
240 if ( pDsd[i] == '<' && pDsd[pMatches[i]+1] == '{' )
241 {
242 assert( pDsd[pMatches[i]] == '>' );
243 for ( ; i <= pMatches[i]; i++ )
244 *pRes++ = pDsd[i];
245 }
246 if ( (pDsd[i] >= 'A' && pDsd[i] <= 'F') || (pDsd[i] >= '0' && pDsd[i] <= '9') )
247 while ( (pDsd[i] >= 'A' && pDsd[i] <= 'F') || (pDsd[i] >= '0' && pDsd[i] <= '9') )
248 *pRes++ = pDsd[i++];
249 // detect variables
250 if ( !(pDsd[i] >= 'a' && pDsd[i] <= 'z') || (pDsd[i] - 'a' < nShared) )
251 {
252 *pRes++ = pDsd[i];
253 continue;
254 }
255 // inline definition
256 assert( pDsd[i]-'a' < DAU_MAX_STR );
257 for ( pDef = pS->pStore[pDsd[i]-'a']; *pDef; pDef++ )
258 *pRes++ = *pDef;
259 }
260 *pRes++ = 0;
261 assert( pRes - pBegin < DAU_MAX_STR );
262 }
263
264
265 /**Function*************************************************************
266
267 Synopsis [Computes independence status for each opening parenthesis.]
268
269 Description []
270
271 SideEffects []
272
273 SeeAlso []
274
275 ***********************************************************************/
Dau_DsdMergePrintWithStatus(char * p,int * pStatus)276 static inline void Dau_DsdMergePrintWithStatus( char * p, int * pStatus )
277 {
278 int i;
279 printf( "%s\n", p );
280 for ( i = 0; p[i]; i++ )
281 if ( !(p[i] == '(' || p[i] == '[' || p[i] == '<' || p[i] == '{' || (p[i] >= 'a' && p[i] <= 'z')) )
282 printf( " " );
283 else if ( pStatus[i] >= 0 )
284 printf( "%d", pStatus[i] );
285 else
286 printf( "-" );
287 printf( "\n" );
288 }
Dau_DsdMergeStatus_rec(char * pStr,char ** p,int * pMatches,int nShared,int * pStatus)289 int Dau_DsdMergeStatus_rec( char * pStr, char ** p, int * pMatches, int nShared, int * pStatus )
290 {
291 // none pure
292 // 1 one pure
293 // 2 two or more pure
294 // 3 all pure
295 if ( **p == '!' )
296 {
297 pStatus[*p - pStr] = -1;
298 (*p)++;
299 }
300 while ( (**p >= 'A' && **p <= 'F') || (**p >= '0' && **p <= '9') )
301 {
302 pStatus[*p - pStr] = -1;
303 (*p)++;
304 }
305 if ( **p == '<' )
306 {
307 char * q = pStr + pMatches[ *p - pStr ];
308 if ( *(q+1) == '{' )
309 {
310 char * pTemp = *p;
311 *p = q+1;
312 for ( ; pTemp < q+1; pTemp++ )
313 pStatus[pTemp - pStr] = -1;
314 }
315 }
316 if ( **p >= 'a' && **p <= 'z' ) // var
317 return pStatus[*p - pStr] = (**p - 'a' < nShared) ? 0 : 3;
318 if ( **p == '(' || **p == '[' || **p == '<' || **p == '{' ) // and/or/xor
319 {
320 int Status, nPure = 0, nTotal = 0;
321 char * pOld = *p;
322 char * q = pStr + pMatches[ *p - pStr ];
323 assert( *q == **p + 1 + (**p != '(') );
324 for ( (*p)++; *p < q; (*p)++ )
325 {
326 Status = Dau_DsdMergeStatus_rec( pStr, p, pMatches, nShared, pStatus );
327 nPure += (Status == 3);
328 nTotal++;
329 }
330 assert( *p == q );
331 assert( nTotal > 1 );
332 if ( nPure == 0 )
333 Status = 0;
334 else if ( nPure == 1 )
335 Status = 1;
336 else if ( nPure < nTotal )
337 Status = 2;
338 else if ( nPure == nTotal )
339 Status = 3;
340 else assert( 0 );
341 return (pStatus[pOld - pStr] = Status);
342 }
343 assert( 0 );
344 return 0;
345 }
Dau_DsdMergeStatus(char * pDsd,int * pMatches,int nShared,int * pStatus)346 static inline int Dau_DsdMergeStatus( char * pDsd, int * pMatches, int nShared, int * pStatus )
347 {
348 return Dau_DsdMergeStatus_rec( pDsd, &pDsd, pMatches, nShared, pStatus );
349 }
350
351 /**Function*************************************************************
352
353 Synopsis [Extracts the formula.]
354
355 Description []
356
357 SideEffects []
358
359 SeeAlso []
360
361 ***********************************************************************/
Dau_DsdMergeGetStatus(char * pBeg,char * pStr,int * pMatches,int * pStatus)362 static inline int Dau_DsdMergeGetStatus( char * pBeg, char * pStr, int * pMatches, int * pStatus )
363 {
364 if ( *pBeg == '!' )
365 pBeg++;
366 while ( (*pBeg >= 'A' && *pBeg <= 'F') || (*pBeg >= '0' && *pBeg <= '9') )
367 pBeg++;
368 if ( *pBeg == '<' )
369 {
370 char * q = pStr + pMatches[pBeg - pStr];
371 if ( *(q+1) == '{' )
372 pBeg = q+1;
373 }
374 return pStatus[pBeg - pStr];
375 }
Dau_DsdMergeSubstitute_rec(Dau_Sto_t * pS,char * pStr,char ** p,int * pMatches,int * pStatus,int fWrite)376 void Dau_DsdMergeSubstitute_rec( Dau_Sto_t * pS, char * pStr, char ** p, int * pMatches, int * pStatus, int fWrite )
377 {
378 // assert( **p != '!' );
379
380 if ( **p == '!' )
381 {
382 if ( fWrite )
383 Dau_DsdMergeStoreAddToOutputChar( pS, **p );
384 (*p)++;
385 }
386
387 while ( (**p >= 'A' && **p <= 'F') || (**p >= '0' && **p <= '9') )
388 {
389 if ( fWrite )
390 Dau_DsdMergeStoreAddToOutputChar( pS, **p );
391 (*p)++;
392 }
393 if ( **p == '<' )
394 {
395 char * q = pStr + pMatches[ *p - pStr ];
396 if ( *(q+1) == '{' )
397 {
398 char * pTemp = *p;
399 *p = q+1;
400 if ( fWrite )
401 for ( ; pTemp < q+1; pTemp++ )
402 Dau_DsdMergeStoreAddToOutputChar( pS, *pTemp );
403 }
404 }
405 if ( **p >= 'a' && **p <= 'z' ) // var
406 {
407 if ( fWrite )
408 Dau_DsdMergeStoreAddToOutputChar( pS, **p );
409 return;
410 }
411 if ( **p == '(' || **p == '[' || **p == '<' || **p == '{' ) // and/or/xor
412 {
413 int New, StatusFan, Status = pStatus[*p - pStr];
414 char * pBeg, * q = pStr + pMatches[ *p - pStr ];
415 assert( *q == **p + 1 + (**p != '(') );
416 if ( !fWrite )
417 {
418 assert( Status == 3 );
419 *p = q;
420 return;
421 }
422 assert( Status != 3 );
423 if ( Status == 0 ) // none pure
424 {
425 Dau_DsdMergeStoreAddToOutputChar( pS, **p );
426 for ( (*p)++; *p < q; (*p)++ )
427 {
428 if ( **p == '!' )
429 {
430 Dau_DsdMergeStoreAddToOutputChar( pS, '!' );
431 (*p)++;
432 }
433 Dau_DsdMergeSubstitute_rec( pS, pStr, p, pMatches, pStatus, 1 );
434 }
435 Dau_DsdMergeStoreAddToOutputChar( pS, **p );
436 assert( *p == q );
437 return;
438 }
439 if ( Status == 1 || **p == '<' || **p == '{' ) // 1 pure
440 {
441 Dau_DsdMergeStoreAddToOutputChar( pS, **p );
442 for ( (*p)++; *p < q; (*p)++ )
443 {
444 if ( **p == '!' )
445 {
446 Dau_DsdMergeStoreAddToOutputChar( pS, '!' );
447 (*p)++;
448 }
449 pBeg = *p;
450 StatusFan = Dau_DsdMergeGetStatus( pBeg, pStr, pMatches, pStatus );
451 Dau_DsdMergeSubstitute_rec( pS, pStr, p, pMatches, pStatus, StatusFan != 3 );
452 if ( StatusFan == 3 )
453 {
454 int New = Dau_DsdMergeStoreCreateDef( pS, pBeg, *p+1 );
455 Dau_DsdMergeStoreAddToOutputChar( pS, (char)('a' + New) );
456 }
457 }
458 Dau_DsdMergeStoreAddToOutputChar( pS, **p );
459 assert( *p == q );
460 return;
461 }
462 if ( Status == 2 )
463 {
464 // add more than one defs
465 Dau_DsdMergeStoreAddToOutputChar( pS, **p );
466 New = Dau_DsdMergeStoreStartDef( pS, **p );
467 for ( (*p)++; *p < q; (*p)++ )
468 {
469 pBeg = *p;
470 StatusFan = Dau_DsdMergeGetStatus( pBeg, pStr, pMatches, pStatus );
471 if ( **p == '!' )
472 {
473 if ( StatusFan != 3 )
474 Dau_DsdMergeStoreAddToOutputChar( pS, '!' );
475 else
476 Dau_DsdMergeStoreAddToDefChar( pS, New, '!' );
477 (*p)++;
478 pBeg++;
479 }
480 Dau_DsdMergeSubstitute_rec( pS, pStr, p, pMatches, pStatus, StatusFan != 3 );
481 if ( StatusFan == 3 )
482 Dau_DsdMergeStoreAddToDef( pS, New, pBeg, *p+1 );
483 }
484 Dau_DsdMergeStoreStopDef( pS, New, *q );
485 Dau_DsdMergeStoreAddToOutputChar( pS, (char)('a' + New) );
486 Dau_DsdMergeStoreAddToOutputChar( pS, **p );
487 return;
488 }
489 assert( 0 );
490 return;
491 }
492 assert( 0 );
493 }
Dau_DsdMergeSubstitute(Dau_Sto_t * pS,char * pDsd,int * pMatches,int * pStatus)494 static inline void Dau_DsdMergeSubstitute( Dau_Sto_t * pS, char * pDsd, int * pMatches, int * pStatus )
495 {
496 /*
497 int fCompl = 0;
498 if ( pDsd[0] == '!' )
499 {
500 Dau_DsdMergeStoreAddToOutputChar( pS, '!' );
501 pDsd++;
502 fCompl = 1;
503 }
504 */
505 Dau_DsdMergeSubstitute_rec( pS, pDsd, &pDsd, pMatches, pStatus, 1 );
506 Dau_DsdMergeStoreAddToOutputChar( pS, 0 );
507 }
508
509 /**Function*************************************************************
510
511 Synopsis [Removes braces.]
512
513 Description []
514
515 SideEffects []
516
517 SeeAlso []
518
519 ***********************************************************************/
Dau_DsdRemoveBraces_rec(char * pStr,char ** p,int * pMatches)520 void Dau_DsdRemoveBraces_rec( char * pStr, char ** p, int * pMatches )
521 {
522 if ( **p == '!' )
523 (*p)++;
524 while ( (**p >= 'A' && **p <= 'F') || (**p >= '0' && **p <= '9') )
525 (*p)++;
526 if ( **p == '<' )
527 {
528 char * q = pStr + pMatches[*p - pStr];
529 if ( *(q+1) == '{' )
530 *p = q+1;
531 }
532 if ( **p >= 'a' && **p <= 'z' ) // var
533 return;
534 if ( **p == '(' || **p == '[' || **p == '<' || **p == '{' )
535 {
536 char * q = pStr + pMatches[ *p - pStr ];
537 assert( *q == **p + 1 + (**p != '(') );
538 for ( (*p)++; *p < q; (*p)++ )
539 {
540 int fCompl = (**p == '!');
541 char * pBeg = fCompl ? *p + 1 : *p;
542 Dau_DsdRemoveBraces_rec( pStr, p, pMatches );
543 if ( (!fCompl && *pBeg == '(' && *q == ')') || (*pBeg == '[' && *q == ']') )
544 {
545 assert( **p == ')' || **p == ']' );
546 *pBeg = **p = ' ';
547 }
548 }
549 assert( *p == q );
550 return;
551 }
552 assert( 0 );
553 }
Dau_DsdRemoveBraces(char * pDsd,int * pMatches)554 void Dau_DsdRemoveBraces( char * pDsd, int * pMatches )
555 {
556 char * q, * p = pDsd;
557 if ( pDsd[1] == 0 )
558 return;
559 Dau_DsdRemoveBraces_rec( pDsd, &pDsd, pMatches );
560 for ( q = p; *p; p++ )
561 if ( *p != ' ' )
562 {
563 if ( *p == '!' && *(q-1) == '!' && p != q )
564 {
565 q--;
566 continue;
567 }
568 *q++ = *p;
569 }
570 *q = 0;
571 }
572
573
574 abctime s_TimeComp[4] = {0};
575
576 /**Function*************************************************************
577
578 Synopsis [Performs merging of two DSD formulas.]
579
580 Description []
581
582 SideEffects []
583
584 SeeAlso []
585
586 ***********************************************************************/
Dau_DsdMerge(char * pDsd0i,int * pPerm0,char * pDsd1i,int * pPerm1,int fCompl0,int fCompl1,int nVars)587 char * Dau_DsdMerge( char * pDsd0i, int * pPerm0, char * pDsd1i, int * pPerm1, int fCompl0, int fCompl1, int nVars )
588 {
589 int fVerbose = 0;
590 int fCheck = 0;
591 static int Counter = 0;
592 static char pRes[2*DAU_MAX_STR+10];
593 char pDsd0[DAU_MAX_STR];
594 char pDsd1[DAU_MAX_STR];
595 int pMatches0[DAU_MAX_STR];
596 int pMatches1[DAU_MAX_STR];
597 int pVarPres[DAU_MAX_VAR];
598 int pOld2New[DAU_MAX_VAR];
599 int pNew2Old[DAU_MAX_VAR];
600 int pStatus0[DAU_MAX_STR];
601 int pStatus1[DAU_MAX_STR];
602 int pMatches[DAU_MAX_STR];
603 int nVarsShared, nVarsTotal;
604 Dau_Sto_t S, * pS = &S;
605 word * pTruth, * pt = NULL, * pt0 = NULL, * pt1 = NULL;
606 word pParts[3][DAU_MAX_WORD];
607 int Status;
608 abctime clk = Abc_Clock();
609 Counter++;
610 // create local copies
611 Dau_DsdMergeCopy( pDsd0i, fCompl0, pDsd0 );
612 Dau_DsdMergeCopy( pDsd1i, fCompl1, pDsd1 );
613 if ( fVerbose )
614 printf( "\nAfter copying:\n" );
615 if ( fVerbose )
616 printf( "%s\n", pDsd0 );
617 if ( fVerbose )
618 printf( "%s\n", pDsd1 );
619 // handle constants
620 if ( Dau_DsdIsConst(pDsd0) || Dau_DsdIsConst(pDsd1) )
621 {
622 if ( Dau_DsdIsConst0(pDsd0) )
623 strcpy( pRes, pDsd0 );
624 else if ( Dau_DsdIsConst1(pDsd0) )
625 strcpy( pRes, pDsd1 );
626 else if ( Dau_DsdIsConst0(pDsd1) )
627 strcpy( pRes, pDsd1 );
628 else if ( Dau_DsdIsConst1(pDsd1) )
629 strcpy( pRes, pDsd0 );
630 else assert( 0 );
631 return pRes;
632 }
633
634 // compute matches
635 Dau_DsdMergeMatches( pDsd0, pMatches0 );
636 Dau_DsdMergeMatches( pDsd1, pMatches1 );
637 // implement permutation
638 Dau_DsdMergeReplace( pDsd0, pMatches0, pPerm0 );
639 Dau_DsdMergeReplace( pDsd1, pMatches1, pPerm1 );
640 if ( fVerbose )
641 printf( "After replacement:\n" );
642 if ( fVerbose )
643 printf( "%s\n", pDsd0 );
644 if ( fVerbose )
645 printf( "%s\n", pDsd1 );
646
647
648 if ( fCheck )
649 {
650 pt0 = Dau_DsdToTruth( pDsd0, nVars );
651 Abc_TtCopy( pParts[0], pt0, Abc_TtWordNum(nVars), 0 );
652 }
653 if ( fCheck )
654 {
655 pt1 = Dau_DsdToTruth( pDsd1, nVars );
656 Abc_TtCopy( pParts[1], pt1, Abc_TtWordNum(nVars), 0 );
657 Abc_TtAnd( pParts[2], pParts[0], pParts[1], Abc_TtWordNum(nVars), 0 );
658 }
659
660 // find shared varaiables
661 nVarsShared = Dau_DsdMergeFindShared(pDsd0, pDsd1, pMatches0, pMatches1, pVarPres);
662 if ( nVarsShared == 0 )
663 {
664 sprintf( pRes, "(%s%s)", pDsd0, pDsd1 );
665 if ( fVerbose )
666 printf( "Disjoint:\n" );
667 if ( fVerbose )
668 printf( "%s\n", pRes );
669
670 Dau_DsdMergeMatches( pRes, pMatches );
671 Dau_DsdRemoveBraces( pRes, pMatches );
672 Dau_DsdNormalize( pRes );
673 if ( fVerbose )
674 printf( "Normalized:\n" );
675 if ( fVerbose )
676 printf( "%s\n", pRes );
677
678 s_TimeComp[0] += Abc_Clock() - clk;
679 return pRes;
680 }
681 s_TimeComp[3] += Abc_Clock() - clk;
682 // create variable mapping
683 nVarsTotal = Dau_DsdMergeCreateMaps( pVarPres, nVarsShared, pOld2New, pNew2Old );
684 // perform variable replacement
685 Dau_DsdMergeReplace( pDsd0, pMatches0, pOld2New );
686 Dau_DsdMergeReplace( pDsd1, pMatches1, pOld2New );
687 // find uniqueness status
688 Dau_DsdMergeStatus( pDsd0, pMatches0, nVarsShared, pStatus0 );
689 Dau_DsdMergeStatus( pDsd1, pMatches1, nVarsShared, pStatus1 );
690 if ( fVerbose )
691 printf( "Individual status:\n" );
692 if ( fVerbose )
693 Dau_DsdMergePrintWithStatus( pDsd0, pStatus0 );
694 if ( fVerbose )
695 Dau_DsdMergePrintWithStatus( pDsd1, pStatus1 );
696 // prepare storage
697 Dau_DsdMergeStoreClean( pS, nVarsShared );
698 // perform substitutions
699 Dau_DsdMergeStoreCleanOutput( pS );
700 Dau_DsdMergeSubstitute( pS, pDsd0, pMatches0, pStatus0 );
701 strcpy( pDsd0, pS->pOutput );
702 if ( fVerbose )
703 printf( "Substitutions:\n" );
704 if ( fVerbose )
705 printf( "%s\n", pDsd0 );
706
707 // perform substitutions
708 Dau_DsdMergeStoreCleanOutput( pS );
709 Dau_DsdMergeSubstitute( pS, pDsd1, pMatches1, pStatus1 );
710 strcpy( pDsd1, pS->pOutput );
711 if ( fVerbose )
712 printf( "%s\n", pDsd1 );
713 if ( fVerbose )
714 Dau_DsdMergeStorePrintDefs( pS );
715
716 // create new function
717 // assert( nVarsTotal <= 6 );
718 sprintf( pS->pOutput, "(%s%s)", pDsd0, pDsd1 );
719 pTruth = Dau_DsdToTruth( pS->pOutput, nVarsTotal );
720 Status = Dau_DsdDecompose( pTruth, nVarsTotal, 0, 1, pS->pOutput );
721 //printf( "%d ", Status );
722 if ( Status == -1 ) // did not find 1-step DSD
723 return NULL;
724 // if ( Status > 6 ) // non-DSD part is too large
725 // return NULL;
726 if ( Dau_DsdIsConst(pS->pOutput) )
727 {
728 strcpy( pRes, pS->pOutput );
729 return pRes;
730 }
731 if ( fVerbose )
732 printf( "Decomposition:\n" );
733 if ( fVerbose )
734 printf( "%s\n", pS->pOutput );
735 // substitute definitions
736 Dau_DsdMergeMatches( pS->pOutput, pMatches );
737 Dau_DsdMergeInlineDefinitions( pS->pOutput, pMatches, pS, pRes, nVarsShared );
738 if ( fVerbose )
739 printf( "Inlining:\n" );
740 if ( fVerbose )
741 printf( "%s\n", pRes );
742 // perform variable replacement
743 Dau_DsdMergeMatches( pRes, pMatches );
744 Dau_DsdMergeReplace( pRes, pMatches, pNew2Old );
745 Dau_DsdRemoveBraces( pRes, pMatches );
746 if ( fVerbose )
747 printf( "Replaced:\n" );
748 if ( fVerbose )
749 printf( "%s\n", pRes );
750 Dau_DsdNormalize( pRes );
751 if ( fVerbose )
752 printf( "Normalized:\n" );
753 if ( fVerbose )
754 printf( "%s\n", pRes );
755
756 if ( fCheck )
757 {
758 pt = Dau_DsdToTruth( pRes, nVars );
759 if ( !Abc_TtEqual( pParts[2], pt, Abc_TtWordNum(nVars) ) )
760 printf( "Dau_DsdMerge(): Verification failed!\n" );
761 }
762
763 if ( Status == 0 )
764 s_TimeComp[1] += Abc_Clock() - clk;
765 else
766 s_TimeComp[2] += Abc_Clock() - clk;
767 return pRes;
768 }
769
770
Dau_DsdTest66()771 void Dau_DsdTest66()
772 {
773 int Perm0[DAU_MAX_VAR] = { 0, 1, 2, 3, 4, 5 };
774 // int pMatches[DAU_MAX_STR];
775 // int pStatus[DAU_MAX_STR];
776
777 // char * pStr = "(!(!a<bcd>)!(!fe))";
778 // char * pStr = "([acb]<!edf>)";
779 // char * pStr = "!(f!(b!c!(d[ea])))";
780 char * pStr = "[!(a[be])!(c!df)]";
781 // char * pStr = "<(e<bca>)fd>";
782 // char * pStr = "[d8001{abef}c]";
783 // char * pStr1 = "(abc)";
784 // char * pStr2 = "[adf]";
785 // char * pStr1 = "(!abce)";
786 // char * pStr2 = "[adf!b]";
787 // char * pStr1 = "(!abc)";
788 // char * pStr2 = "[ab]";
789 // char * pStr1 = "[d81{abe}c]";
790 // char * pStr1 = "[d<a(bc)(!b!c)>{abe}c]";
791 // char * pStr1 = "[d81{abe}c]";
792 // char * pStr1 = "[d(a[be])c]";
793 // char * pStr2 = "(df)";
794 // char * pStr1 = "(abf)";
795 // char * pStr2 = "(a[(bc)(fde)])";
796 // char * pStr1 = "8001{abc[ef]}";
797 // char * pStr2 = "(abe)";
798
799 char * pStr1 = "(!(ab)de)";
800 char * pStr2 = "(!(ac)f)";
801
802 char * pRes;
803 word t = Dau_Dsd6ToTruth( pStr );
804 return;
805
806 // pStr2 = Dau_DsdDecompose( &t, 6, 0, NULL );
807 // Dau_DsdNormalize( pStr2 );
808
809 // Dau_DsdMergeMatches( pStr, pMatches );
810 // Dau_DsdMergeStatus( pStr, pMatches, 2, pStatus );
811 // Dau_DsdMergePrintWithStatus( pStr, pStatus );
812
813 pRes = Dau_DsdMerge( pStr1, Perm0, pStr2, Perm0, 0, 0, 6 );
814
815 t = 0;
816 }
817
818 ////////////////////////////////////////////////////////////////////////
819 /// END OF FILE ///
820 ////////////////////////////////////////////////////////////////////////
821
822
823 ABC_NAMESPACE_IMPL_END
824
825