ABC: A System for Sequential Synthesis and Verification
 
Loading...
Searching...
No Matches
mapperCut.c
Go to the documentation of this file.
1
18
19#include "mapperInt.h"
20
22
23
27
28// the largest number of cuts considered
29#define MAP_CUTS_MAX_COMPUTE 1000
30// the largest number of cuts used
31#define MAP_CUTS_MAX_USE 250
32
33// temporary hash table to store the cuts
36{
37 Map_Cut_t ** pBins; // the table used for linear probing
38 int nBins; // the size of the table
39 int * pCuts; // the array of cuts currently stored
40 int nCuts; // the number of cuts currently stored
41 Map_Cut_t ** pArray; // the temporary array of cuts
42 Map_Cut_t ** pCuts1; // the temporary array of cuts
43 Map_Cut_t ** pCuts2; // the temporary array of cuts
44};
45
46// primes used to compute the hash key
47static int s_HashPrimes[10] = { 109, 499, 557, 619, 631, 709, 797, 881, 907, 991 };
48
49static Map_Cut_t * Map_CutCompute( Map_Man_t * p, Map_CutTable_t * pTable, Map_Node_t * pNode );
50static void Map_CutFilter( Map_Man_t * p, Map_Node_t * pNode );
51static Map_Cut_t * Map_CutMergeLists( Map_Man_t * p, Map_CutTable_t * pTable, Map_Cut_t * pList1, Map_Cut_t * pList2, int fComp1, int fComp2 );
52static int Map_CutMergeTwo( Map_Cut_t * pCut1, Map_Cut_t * pCut2, Map_Node_t * ppNodes[], int nNodesMax );
53static Map_Cut_t * Map_CutUnionLists( Map_Cut_t * pList1, Map_Cut_t * pList2 );
54static int Map_CutBelongsToList( Map_Cut_t * pList, Map_Node_t * ppNodes[], int nNodes );
55
56static void Map_CutListPrint( Map_Man_t * pMan, Map_Node_t * pRoot );
57static void Map_CutListPrint2( Map_Man_t * pMan, Map_Node_t * pRoot );
58static void Map_CutPrint_( Map_Man_t * pMan, Map_Cut_t * pCut, Map_Node_t * pRoot );
59
60static Map_CutTable_t * Map_CutTableStart( Map_Man_t * pMan );
61static void Map_CutTableStop( Map_CutTable_t * p );
62static unsigned Map_CutTableHash( Map_Node_t * ppNodes[], int nNodes );
63static int Map_CutTableLookup( Map_CutTable_t * p, Map_Node_t * ppNodes[], int nNodes );
64static Map_Cut_t * Map_CutTableConsider( Map_Man_t * pMan, Map_CutTable_t * p, Map_Node_t * ppNodes[], int nNodes );
65static void Map_CutTableRestart( Map_CutTable_t * p );
66
67static Map_Cut_t * Map_CutSortCuts( Map_Man_t * pMan, Map_CutTable_t * p, Map_Cut_t * pList );
68static int Map_CutList2Array( Map_Cut_t ** pArray, Map_Cut_t * pList );
69static Map_Cut_t * Map_CutArray2List( Map_Cut_t ** pArray, int nCuts );
70
71static unsigned Map_CutComputeTruth( Map_Man_t * p, Map_Cut_t * pCut, Map_Cut_t * pTemp0, Map_Cut_t * pTemp1, int fComp0, int fComp1 );
72
73// iterator through all the cuts of the list
74#define Map_ListForEachCut( pList, pCut ) \
75 for ( pCut = pList; \
76 pCut; \
77 pCut = pCut->pNext )
78#define Map_ListForEachCutSafe( pList, pCut, pCut2 ) \
79 for ( pCut = pList, \
80 pCut2 = pCut? pCut->pNext: NULL; \
81 pCut; \
82 pCut = pCut2, \
83 pCut2 = pCut? pCut->pNext: NULL )
84
88
101{
102 Map_Node_t * pNode;
103 Map_Cut_t * pCut;
104 int i, nCuts;
105// int nCuts55 = 0, nCuts5x = 0, nCuts4x = 0, nCuts3x = 0;
106// int pCounts[7] = {0};
107 nCuts = 0;
108 for ( i = 0; i < pMan->nBins; i++ )
109 for ( pNode = pMan->pBins[i]; pNode; pNode = pNode->pNext )
110 for ( pCut = pNode->pCuts; pCut; pCut = pCut->pNext )
111 if ( pCut->nLeaves > 1 ) // skip the elementary cuts
112 {
113 nCuts++;
114/*
115 if ( Map_CutRegular(pCut->pOne)->nLeaves == 5 && Map_CutRegular(pCut->pTwo)->nLeaves == 5 )
116 nCuts55++;
117 if ( Map_CutRegular(pCut->pOne)->nLeaves == 5 || Map_CutRegular(pCut->pTwo)->nLeaves == 5 )
118 nCuts5x++;
119 else if ( Map_CutRegular(pCut->pOne)->nLeaves == 4 || Map_CutRegular(pCut->pTwo)->nLeaves == 4 )
120 nCuts4x++;
121 else if ( Map_CutRegular(pCut->pOne)->nLeaves == 3 || Map_CutRegular(pCut->pTwo)->nLeaves == 3 )
122 nCuts3x++;
123*/
124// pCounts[ Map_CutRegular(pCut->pOne)->nLeaves ]++;
125// pCounts[ Map_CutRegular(pCut->pTwo)->nLeaves ]++;
126 }
127// printf( "Total cuts = %6d. 55 = %6d. 5x = %6d. 4x = %6d. 3x = %6d.\n", nCuts, nCuts55, nCuts5x, nCuts4x, nCuts3x );
128
129// printf( "Total cuts = %6d. 6= %6d. 5= %6d. 4= %6d. 3= %6d. 2= %6d. 1= %6d.\n",
130// nCuts, pCounts[6], pCounts[5], pCounts[4], pCounts[3], pCounts[2], pCounts[1] );
131 return nCuts;
132}
133
159{
160 Map_Cut_t * pCut;
161 assert( Map_NodeIsVar(pNode) || Map_NodeIsBuf(pNode) );
162 pCut = Map_CutAlloc( p );
163 pCut->nLeaves = 1;
164 pCut->ppLeaves[0] = pNode;
165 pNode->pCuts = pCut;
166 pNode->pCutBest[0] = NULL; // negative polarity is not mapped
167 pNode->pCutBest[1] = pCut; // positive polarity is a trivial cut
168 pCut->uTruth = 0xAAAAAAAA; // the first variable "1010"
169 pCut->M[0].AreaFlow = 0.0;
170 pCut->M[1].AreaFlow = 0.0;
171}
173{
174 ProgressBar * pProgress;
175 Map_CutTable_t * pTable;
176 Map_Node_t * pNode;
177 int nCuts, nNodes, i;
178 abctime clk = Abc_Clock();
179 // set the elementary cuts for the PI variables
180 assert( p->nVarsMax > 1 && p->nVarsMax < 7 );
181 for ( i = 0; i < p->nInputs; i++ )
182 Map_MappingCutsInput( p, p->pInputs[i] );
183
184 // compute the cuts for the internal nodes
185 nNodes = p->vMapObjs->nSize;
186 pProgress = Extra_ProgressBarStart( stdout, nNodes );
187 pTable = Map_CutTableStart( p );
188 for ( i = 0; i < nNodes; i++ )
189 {
190 pNode = p->vMapObjs->pArray[i];
191 if ( Map_NodeIsBuf(pNode) )
192 Map_MappingCutsInput( p, pNode );
193 else if ( Map_NodeIsAnd(pNode) )
194 Map_CutCompute( p, pTable, pNode );
195 else continue;
196 Extra_ProgressBarUpdate( pProgress, i, "Cuts ..." );
197 }
198 Extra_ProgressBarStop( pProgress );
199 Map_CutTableStop( pTable );
200
201 // report the stats
202 if ( p->fVerbose )
203 {
204 nCuts = Map_MappingCountAllCuts(p);
205 printf( "Nodes = %6d. Total %d-feasible cuts = %10d. Per node = %.1f. ",
206 p->nNodes, p->nVarsMax, nCuts, ((float)nCuts)/p->nNodes );
207 ABC_PRT( "Time", Abc_Clock() - clk );
208 }
209
210 // print the cuts for the first primary output
211// Map_CutListPrint( p, Map_Regular(p->pOutputs[0]) );
212}
213
225Map_Cut_t * Map_CutCompute( Map_Man_t * p, Map_CutTable_t * pTable, Map_Node_t * pNode )
226{
227 Map_Node_t * pTemp;
228 Map_Cut_t * pList, * pList1, * pList2;
229 Map_Cut_t * pCut;
230
231 // if the cuts are computed return them
232 if ( pNode->pCuts )
233 return pNode->pCuts;
234
235 // compute the cuts for the children
236 pList1 = Map_Regular(pNode->p1)->pCuts;
237 pList2 = Map_Regular(pNode->p2)->pCuts;
238 // merge the lists
239 pList = Map_CutMergeLists( p, pTable, pList1, pList2,
240 Map_IsComplement(pNode->p1), Map_IsComplement(pNode->p2) );
241 // if there are functionally equivalent nodes, union them with this list
242 assert( pList );
243 // only add to the list of cuts if the node is a representative one
244 if ( pNode->pRepr == NULL )
245 {
246 for ( pTemp = pNode->pNextE; pTemp; pTemp = pTemp->pNextE )
247 {
248 assert( pTemp->pCuts );
249 pList = Map_CutUnionLists( pList, pTemp->pCuts );
250 assert( pTemp->pCuts );
251 pList = Map_CutSortCuts( p, pTable, pList );
252 }
253 }
254 // add the new cut
255 pCut = Map_CutAlloc( p );
256 pCut->nLeaves = 1;
257 pCut->ppLeaves[0] = pNode;
258 pCut->uTruth = 0xAAAAAAAA;
259 // append (it is important that the elementary cut is appended first)
260 pCut->pNext = pList;
261 // set at the node
262 pNode->pCuts = pCut;
263 // remove the dominated cuts
264 Map_CutFilter( p, pNode );
265 // set the phase correctly
266 if ( pNode->pRepr && Map_NodeComparePhase(pNode, pNode->pRepr) )
267 {
268 Map_ListForEachCut( pNode->pCuts, pCut )
269 pCut->Phase = 1;
270 }
271/*
272 {
273 int i, Counter = 0;;
274 for ( pCut = pNode->pCuts->pNext; pCut; pCut = pCut->pNext )
275 for ( i = 0; i < pCut->nLeaves; i++ )
276 Counter += (pCut->ppLeaves[i]->Level >= pNode->Level);
277// if ( Counter )
278// printf( " %d", Counter );
279 }
280*/
281 return pCut;
282}
283
295void Map_CutFilter( Map_Man_t * p, Map_Node_t * pNode )
296{
297 Map_Cut_t * pTemp, * pPrev, * pCut, * pCut2;
298 int i, k, Counter;
299
300 Counter = 0;
301 pPrev = pNode->pCuts;
302 Map_ListForEachCutSafe( pNode->pCuts->pNext, pCut, pCut2 )
303 {
304 // go through all the previous cuts up to pCut
305 for ( pTemp = pNode->pCuts->pNext; pTemp != pCut; pTemp = pTemp->pNext )
306 {
307 // check if every node in pTemp is contained in pCut
308 for ( i = 0; i < pTemp->nLeaves; i++ )
309 {
310 for ( k = 0; k < pCut->nLeaves; k++ )
311 if ( pTemp->ppLeaves[i] == pCut->ppLeaves[k] )
312 break;
313 if ( k == pCut->nLeaves ) // node i in pTemp is not contained in pCut
314 break;
315 }
316 if ( i == pTemp->nLeaves ) // every node in pTemp is contained in pCut
317 {
318 Counter++;
319 break;
320 }
321 }
322 if ( pTemp != pCut ) // pTemp contain pCut
323 {
324 pPrev->pNext = pCut->pNext; // skip pCut
325 // recycle pCut
326 Map_CutFree( p, pCut );
327 }
328 else
329 pPrev = pCut;
330 }
331// printf( "Dominated = %3d. \n", Counter );
332}
333
345Map_Cut_t * Map_CutMergeLists( Map_Man_t * p, Map_CutTable_t * pTable,
346 Map_Cut_t * pList1, Map_Cut_t * pList2, int fComp1, int fComp2 )
347{
348 Map_Node_t * ppNodes[6];
349 Map_Cut_t * pListNew, ** ppListNew, * pLists[7] = { NULL };
350 Map_Cut_t * pCut, * pPrev, * pTemp1, * pTemp2;
351 int nNodes, Counter, i;
352 Map_Cut_t ** ppArray1, ** ppArray2, ** ppArray3;
353 int nCuts1, nCuts2, nCuts3, k, fComp3;
354
355 ppArray1 = pTable->pCuts1;
356 ppArray2 = pTable->pCuts2;
357 nCuts1 = Map_CutList2Array( ppArray1, pList1 );
358 nCuts2 = Map_CutList2Array( ppArray2, pList2 );
359 // swap the lists based on their length
360 if ( nCuts1 > nCuts2 )
361 {
362 ppArray3 = ppArray1;
363 ppArray1 = ppArray2;
364 ppArray2 = ppArray3;
365
366 nCuts3 = nCuts1;
367 nCuts1 = nCuts2;
368 nCuts2 = nCuts3;
369
370 fComp3 = fComp1;
371 fComp1 = fComp2;
372 fComp2 = fComp3;
373 }
374 // pList1 is shorter or equal length compared to pList2
375
376 // prepare the manager for the cut computation
377 Map_CutTableRestart( pTable );
378 // go through the cut pairs
379 Counter = 0;
380// for ( pTemp1 = pList1; pTemp1; pTemp1 = fPivot1? NULL: pTemp1->pNext )
381// for ( pTemp2 = pList2; pTemp2; pTemp2 = fPivot2? NULL: pTemp2->pNext )
382 for ( i = 0; i < nCuts1; i++ )
383 {
384 for ( k = 0; k <= i; k++ )
385 {
386 pTemp1 = ppArray1[i];
387 pTemp2 = ppArray2[k];
388
389 if ( pTemp1->nLeaves == p->nVarsMax && pTemp2->nLeaves == p->nVarsMax )
390 {
391 if ( pTemp1->ppLeaves[0] != pTemp2->ppLeaves[0] )
392 continue;
393 if ( pTemp1->ppLeaves[1] != pTemp2->ppLeaves[1] )
394 continue;
395 }
396
397 // check if k-feasible cut exists
398 nNodes = Map_CutMergeTwo( pTemp1, pTemp2, ppNodes, p->nVarsMax );
399 if ( nNodes == 0 )
400 continue;
401 // consider the cut for possible addition to the set of new cuts
402 pCut = Map_CutTableConsider( p, pTable, ppNodes, nNodes );
403 if ( pCut == NULL )
404 continue;
405 // add data to the cut
406 pCut->pOne = Map_CutNotCond( pTemp1, fComp1 );
407 pCut->pTwo = Map_CutNotCond( pTemp2, fComp2 );
408// if ( p->nVarsMax == 5 )
409// pCut->uTruth = Map_CutComputeTruth( p, pCut, pTemp1, pTemp2, fComp1, fComp2 );
410 // add it to the corresponding list
411 pCut->pNext = pLists[(int)pCut->nLeaves];
412 pLists[(int)pCut->nLeaves] = pCut;
413 // count this cut and quit if limit is reached
414 Counter++;
415 if ( Counter == MAP_CUTS_MAX_COMPUTE )
416 goto QUITS;
417 }
418 for ( k = 0; k < i; k++ )
419 {
420 pTemp1 = ppArray1[k];
421 pTemp2 = ppArray2[i];
422
423 if ( pTemp1->nLeaves == p->nVarsMax && pTemp2->nLeaves == p->nVarsMax )
424 {
425 if ( pTemp1->ppLeaves[0] != pTemp2->ppLeaves[0] )
426 continue;
427 if ( pTemp1->ppLeaves[1] != pTemp2->ppLeaves[1] )
428 continue;
429 }
430
431 // check if k-feasible cut exists
432 nNodes = Map_CutMergeTwo( pTemp1, pTemp2, ppNodes, p->nVarsMax );
433 if ( nNodes == 0 )
434 continue;
435 // consider the cut for possible addition to the set of new cuts
436 pCut = Map_CutTableConsider( p, pTable, ppNodes, nNodes );
437 if ( pCut == NULL )
438 continue;
439 // add data to the cut
440 pCut->pOne = Map_CutNotCond( pTemp1, fComp1 );
441 pCut->pTwo = Map_CutNotCond( pTemp2, fComp2 );
442// if ( p->nVarsMax == 5 )
443// pCut->uTruth = Map_CutComputeTruth( p, pCut, pTemp1, pTemp2, fComp1, fComp2 );
444 // add it to the corresponding list
445 pCut->pNext = pLists[(int)pCut->nLeaves];
446 pLists[(int)pCut->nLeaves] = pCut;
447 // count this cut and quit if limit is reached
448 Counter++;
449 if ( Counter == MAP_CUTS_MAX_COMPUTE )
450 goto QUITS;
451 }
452 }
453 // consider the rest of them
454 for ( i = nCuts1; i < nCuts2; i++ )
455 for ( k = 0; k < nCuts1; k++ )
456 {
457 pTemp1 = ppArray1[k];
458 pTemp2 = ppArray2[i];
459
460 if ( pTemp1->nLeaves == p->nVarsMax && pTemp2->nLeaves == p->nVarsMax )
461 {
462 if ( pTemp1->ppLeaves[0] != pTemp2->ppLeaves[0] )
463 continue;
464 if ( pTemp1->ppLeaves[1] != pTemp2->ppLeaves[1] )
465 continue;
466 }
467
468 // check if k-feasible cut exists
469 nNodes = Map_CutMergeTwo( pTemp1, pTemp2, ppNodes, p->nVarsMax );
470 if ( nNodes == 0 )
471 continue;
472 // consider the cut for possible addition to the set of new cuts
473 pCut = Map_CutTableConsider( p, pTable, ppNodes, nNodes );
474 if ( pCut == NULL )
475 continue;
476 // add data to the cut
477 pCut->pOne = Map_CutNotCond( pTemp1, fComp1 );
478 pCut->pTwo = Map_CutNotCond( pTemp2, fComp2 );
479// if ( p->nVarsMax == 5 )
480// pCut->uTruth = Map_CutComputeTruth( p, pCut, pTemp1, pTemp2, fComp1, fComp2 );
481 // add it to the corresponding list
482 pCut->pNext = pLists[(int)pCut->nLeaves];
483 pLists[(int)pCut->nLeaves] = pCut;
484 // count this cut and quit if limit is reached
485 Counter++;
486 if ( Counter == MAP_CUTS_MAX_COMPUTE )
487 goto QUITS;
488 }
489QUITS :
490 // combine all the lists into one
491 pListNew = NULL;
492 ppListNew = &pListNew;
493 for ( i = 1; i <= p->nVarsMax; i++ )
494 {
495 if ( pLists[i] == NULL )
496 continue;
497 // find the last entry
498 for ( pPrev = pLists[i], pCut = pPrev->pNext; pCut;
499 pPrev = pCut, pCut = pCut->pNext );
500 // connect these lists
501 *ppListNew = pLists[i];
502 ppListNew = &pPrev->pNext;
503 }
504 *ppListNew = NULL;
505 // soft the cuts by arrival times and use only the first MAP_CUTS_MAX_USE
506 pListNew = Map_CutSortCuts( p, pTable, pListNew );
507 return pListNew;
508}
509
510
523 Map_Cut_t * pList1, Map_Cut_t * pList2, int fComp1, int fComp2 )
524{
525 Map_Node_t * ppNodes[6];
526 Map_Cut_t * pListNew, ** ppListNew, * pLists[7] = { NULL };
527 Map_Cut_t * pCut, * pPrev, * pTemp1, * pTemp2;
528 int nNodes, Counter, i;
529
530 // prepare the manager for the cut computation
531 Map_CutTableRestart( pTable );
532 // go through the cut pairs
533 Counter = 0;
534 for ( pTemp1 = pList1; pTemp1; pTemp1 = pTemp1->pNext )
535 for ( pTemp2 = pList2; pTemp2; pTemp2 = pTemp2->pNext )
536 {
537 // check if k-feasible cut exists
538 nNodes = Map_CutMergeTwo( pTemp1, pTemp2, ppNodes, p->nVarsMax );
539 if ( nNodes == 0 )
540 continue;
541 // consider the cut for possible addition to the set of new cuts
542 pCut = Map_CutTableConsider( p, pTable, ppNodes, nNodes );
543 if ( pCut == NULL )
544 continue;
545 // add data to the cut
546 pCut->pOne = Map_CutNotCond( pTemp1, fComp1 );
547 pCut->pTwo = Map_CutNotCond( pTemp2, fComp2 );
548 // add it to the corresponding list
549 pCut->pNext = pLists[(int)pCut->nLeaves];
550 pLists[(int)pCut->nLeaves] = pCut;
551 // count this cut and quit if limit is reached
552 Counter++;
553 if ( Counter == MAP_CUTS_MAX_COMPUTE )
554 goto QUITS;
555 }
556QUITS :
557 // combine all the lists into one
558 pListNew = NULL;
559 ppListNew = &pListNew;
560 for ( i = 1; i <= p->nVarsMax; i++ )
561 {
562 if ( pLists[i] == NULL )
563 continue;
564 // find the last entry
565 for ( pPrev = pLists[i], pCut = pPrev->pNext; pCut;
566 pPrev = pCut, pCut = pCut->pNext );
567 // connect these lists
568 *ppListNew = pLists[i];
569 ppListNew = &pPrev->pNext;
570 }
571 *ppListNew = NULL;
572 // soft the cuts by arrival times and use only the first MAP_CUTS_MAX_USE
573 pListNew = Map_CutSortCuts( p, pTable, pListNew );
574 return pListNew;
575}
576
589int Map_CutMergeTwo( Map_Cut_t * pCut1, Map_Cut_t * pCut2, Map_Node_t * ppNodes[], int nNodesMax )
590{
591 Map_Node_t * pNodeTemp;
592 int nTotal, i, k, min, fMismatch;
593
594 // check the special case when at least of the cuts is the largest
595 if ( pCut1->nLeaves == nNodesMax )
596 {
597 if ( pCut2->nLeaves == nNodesMax )
598 {
599 // return 0 if the cuts are different
600 for ( i = 0; i < nNodesMax; i++ )
601 if ( pCut1->ppLeaves[i] != pCut2->ppLeaves[i] )
602 return 0;
603 // return nNodesMax if they are the same
604 for ( i = 0; i < nNodesMax; i++ )
605 ppNodes[i] = pCut1->ppLeaves[i];
606 return nNodesMax;
607 }
608 else if ( pCut2->nLeaves == nNodesMax - 1 )
609 {
610 // return 0 if the cuts are different
611 fMismatch = 0;
612 for ( i = 0; i < nNodesMax; i++ )
613 if ( pCut1->ppLeaves[i] != pCut2->ppLeaves[i - fMismatch] )
614 {
615 if ( fMismatch == 1 )
616 return 0;
617 fMismatch = 1;
618 }
619 // return nNodesMax if they are the same
620 for ( i = 0; i < nNodesMax; i++ )
621 ppNodes[i] = pCut1->ppLeaves[i];
622 return nNodesMax;
623 }
624 }
625 else if ( pCut1->nLeaves == nNodesMax - 1 && pCut2->nLeaves == nNodesMax )
626 {
627 // return 0 if the cuts are different
628 fMismatch = 0;
629 for ( i = 0; i < nNodesMax; i++ )
630 if ( pCut1->ppLeaves[i - fMismatch] != pCut2->ppLeaves[i] )
631 {
632 if ( fMismatch == 1 )
633 return 0;
634 fMismatch = 1;
635 }
636 // return nNodesMax if they are the same
637 for ( i = 0; i < nNodesMax; i++ )
638 ppNodes[i] = pCut2->ppLeaves[i];
639 return nNodesMax;
640 }
641
642 // count the number of unique entries in pCut2
643 nTotal = pCut1->nLeaves;
644 for ( i = 0; i < pCut2->nLeaves; i++ )
645 {
646 // try to find this entry among the leaves of pCut1
647 for ( k = 0; k < pCut1->nLeaves; k++ )
648 if ( pCut2->ppLeaves[i] == pCut1->ppLeaves[k] )
649 break;
650 if ( k < pCut1->nLeaves ) // found
651 continue;
652 // we found a new entry to add
653 if ( nTotal == nNodesMax )
654 return 0;
655 ppNodes[nTotal++] = pCut2->ppLeaves[i];
656 }
657 // we know that the feasible cut exists
658
659 // add the starting entries
660 for ( k = 0; k < pCut1->nLeaves; k++ )
661 ppNodes[k] = pCut1->ppLeaves[k];
662
663 // selection-sort the entries
664 for ( i = 0; i < nTotal - 1; i++ )
665 {
666 min = i;
667 for ( k = i+1; k < nTotal; k++ )
668// if ( ppNodes[k] < ppNodes[min] ) // reported bug fix (non-determinism!)
669 if ( ppNodes[k]->Num < ppNodes[min]->Num )
670 min = k;
671 pNodeTemp = ppNodes[i];
672 ppNodes[i] = ppNodes[min];
673 ppNodes[min] = pNodeTemp;
674 }
675
676 return nTotal;
677}
678
690Map_Cut_t * Map_CutUnionLists( Map_Cut_t * pList1, Map_Cut_t * pList2 )
691{
692 Map_Cut_t * pTemp, * pRoot;
693 // find the last cut in the first list
694 pRoot = pList1;
695 Map_ListForEachCut( pList1, pTemp )
696 pRoot = pTemp;
697 // attach the non-trival part of the second cut to the end of the first
698 assert( pRoot->pNext == NULL );
699 pRoot->pNext = pList2->pNext;
700 pList2->pNext = NULL;
701 return pList1;
702}
703
704
717int Map_CutBelongsToList( Map_Cut_t * pList, Map_Node_t * ppNodes[], int nNodes )
718{
719 Map_Cut_t * pTemp;
720 int i;
721 for ( pTemp = pList; pTemp; pTemp = pTemp->pNext )
722 {
723 for ( i = 0; i < nNodes; i++ )
724 if ( pTemp->ppLeaves[i] != ppNodes[i] )
725 break;
726 if ( i == nNodes )
727 return 1;
728 }
729 return 0;
730}
731
732
744void Map_CutListPrint( Map_Man_t * pMan, Map_Node_t * pRoot )
745{
746 Map_Cut_t * pTemp;
747 int Counter;
748 for ( Counter = 0, pTemp = pRoot->pCuts; pTemp; pTemp = pTemp->pNext, Counter++ )
749 {
750 printf( "%2d : ", Counter + 1 );
751 Map_CutPrint_( pMan, pTemp, pRoot );
752 }
753}
754
766void Map_CutListPrint2( Map_Man_t * pMan, Map_Node_t * pRoot )
767{
768 Map_Cut_t * pTemp;
769 int Counter;
770 for ( Counter = 0, pTemp = pRoot->pCuts; pTemp; pTemp = pTemp->pNext, Counter++ )
771 {
772 printf( "%2d : ", Counter + 1 );
773 Map_CutPrint_( pMan, pTemp, pRoot );
774 }
775}
776
788void Map_CutPrint_( Map_Man_t * pMan, Map_Cut_t * pCut, Map_Node_t * pRoot )
789{
790 int i;
791 printf( "(%3d) {", pRoot->Num );
792 for ( i = 0; i < pMan->nVarsMax; i++ )
793 if ( pCut->ppLeaves[i] )
794 printf( " %3d", pCut->ppLeaves[i]->Num );
795 printf( " }\n" );
796}
797
798
799
800
801
802
803
804
816Map_CutTable_t * Map_CutTableStart( Map_Man_t * pMan )
817{
819 // allocate the table
820 p = ABC_ALLOC( Map_CutTable_t, 1 );
821 memset( p, 0, sizeof(Map_CutTable_t) );
822 p->nBins = Abc_PrimeCudd( 10 * MAP_CUTS_MAX_COMPUTE );
823 p->pBins = ABC_ALLOC( Map_Cut_t *, p->nBins );
824 memset( p->pBins, 0, sizeof(Map_Cut_t *) * p->nBins );
825 p->pCuts = ABC_ALLOC( int, 2 * MAP_CUTS_MAX_COMPUTE );
826 p->pArray = ABC_ALLOC( Map_Cut_t *, 2 * MAP_CUTS_MAX_COMPUTE );
827 p->pCuts1 = ABC_ALLOC( Map_Cut_t *, 2 * MAP_CUTS_MAX_COMPUTE );
828 p->pCuts2 = ABC_ALLOC( Map_Cut_t *, 2 * MAP_CUTS_MAX_COMPUTE );
829 return p;
830}
831
843void Map_CutTableStop( Map_CutTable_t * p )
844{
845 ABC_FREE( p->pCuts1 );
846 ABC_FREE( p->pCuts2 );
847 ABC_FREE( p->pArray );
848 ABC_FREE( p->pBins );
849 ABC_FREE( p->pCuts );
850 ABC_FREE( p );
851}
852
864unsigned Map_CutTableHash( Map_Node_t * ppNodes[], int nNodes )
865{
866 unsigned uRes;
867 int i;
868 uRes = 0;
869 for ( i = 0; i < nNodes; i++ )
870 uRes += s_HashPrimes[i] * ppNodes[i]->Num;
871 return uRes;
872}
873
886int Map_CutTableLookup( Map_CutTable_t * p, Map_Node_t * ppNodes[], int nNodes )
887{
888 Map_Cut_t * pCut;
889 unsigned Key;
890 int b, i;
891
892 Key = Map_CutTableHash(ppNodes, nNodes) % p->nBins;
893 for ( b = Key; p->pBins[b]; b = (b+1) % p->nBins )
894 {
895 pCut = p->pBins[b];
896 if ( pCut->nLeaves != nNodes )
897 continue;
898 for ( i = 0; i < nNodes; i++ )
899 if ( pCut->ppLeaves[i] != ppNodes[i] )
900 break;
901 if ( i == nNodes )
902 return -1;
903 }
904 return b;
905}
906
907
919Map_Cut_t * Map_CutTableConsider( Map_Man_t * pMan, Map_CutTable_t * p, Map_Node_t * ppNodes[], int nNodes )
920{
921 Map_Cut_t * pCut;
922 int Place, i;
923// abctime clk;
924 // check the cut
925 Place = Map_CutTableLookup( p, ppNodes, nNodes );
926 if ( Place == -1 )
927 return NULL;
928 assert( nNodes > 0 );
929 // create the new cut
930//clk = Abc_Clock();
931 pCut = Map_CutAlloc( pMan );
932//pMan->time1 += Abc_Clock() - clk;
933 pCut->nLeaves = nNodes;
934 for ( i = 0; i < nNodes; i++ )
935 pCut->ppLeaves[i] = ppNodes[i];
936 // add the cut to the table
937 assert( p->pBins[Place] == NULL );
938 p->pBins[Place] = pCut;
939 // add the cut to the new list
940 p->pCuts[ p->nCuts++ ] = Place;
941 return pCut;
942}
943
956void Map_CutTableRestart( Map_CutTable_t * p )
957{
958 int i;
959 for ( i = 0; i < p->nCuts; i++ )
960 {
961 assert( p->pBins[ p->pCuts[i] ] );
962 p->pBins[ p->pCuts[i] ] = NULL;
963 }
964 p->nCuts = 0;
965}
966
967
968
981{
982 if ( (*pC1)->nLeaves < (*pC2)->nLeaves )
983 return -1;
984 if ( (*pC1)->nLeaves > (*pC2)->nLeaves )
985 return 1;
986 return 0;
987}
988
1000Map_Cut_t * Map_CutSortCuts( Map_Man_t * pMan, Map_CutTable_t * p, Map_Cut_t * pList )
1001{
1002 Map_Cut_t * pListNew;
1003 int nCuts, i;
1004// abctime clk;
1005 // move the cuts from the list into the array
1006 nCuts = Map_CutList2Array( p->pCuts1, pList );
1007 assert( nCuts <= MAP_CUTS_MAX_COMPUTE );
1008 // sort the cuts
1009//clk = Abc_Clock();
1010 qsort( (void *)p->pCuts1, (size_t)nCuts, sizeof(Map_Cut_t *),
1011 (int (*)(const void *, const void *)) Map_CutSortCutsCompare );
1012//pMan->time2 += Abc_Clock() - clk;
1013 // move them back into the list
1014 if ( nCuts > MAP_CUTS_MAX_USE - 1 )
1015 {
1016 // free the remaining cuts
1017 for ( i = MAP_CUTS_MAX_USE - 1; i < nCuts; i++ )
1018 Extra_MmFixedEntryRecycle( pMan->mmCuts, (char *)p->pCuts1[i] );
1019 // update the number of cuts
1020 nCuts = MAP_CUTS_MAX_USE - 1;
1021 }
1022 pListNew = Map_CutArray2List( p->pCuts1, nCuts );
1023 return pListNew;
1024}
1025
1037int Map_CutList2Array( Map_Cut_t ** pArray, Map_Cut_t * pList )
1038{
1039 int i;
1040 for ( i = 0; pList; pList = pList->pNext, i++ )
1041 pArray[i] = pList;
1042 return i;
1043}
1044
1056Map_Cut_t * Map_CutArray2List( Map_Cut_t ** pArray, int nCuts )
1057{
1058 Map_Cut_t * pListNew, ** ppListNew;
1059 int i;
1060 pListNew = NULL;
1061 ppListNew = &pListNew;
1062 for ( i = 0; i < nCuts; i++ )
1063 {
1064 // connect these lists
1065 *ppListNew = pArray[i];
1066 ppListNew = &pArray[i]->pNext;
1067 }
1068//printf( "\n" );
1069
1070 *ppListNew = NULL;
1071 return pListNew;
1072}
1073
1074
1086unsigned Map_CutComputeTruth( Map_Man_t * p, Map_Cut_t * pCut, Map_Cut_t * pTemp0, Map_Cut_t * pTemp1, int fComp0, int fComp1 )
1087{
1088 static unsigned ** pPerms53 = NULL;
1089 static unsigned ** pPerms54 = NULL;
1090
1091 unsigned uPhase, uTruth, uTruth0, uTruth1;
1092 int i, k;
1093
1094 if ( pPerms53 == NULL )
1095 {
1096 pPerms53 = (unsigned **)Extra_TruthPerm53();
1097 pPerms54 = (unsigned **)Extra_TruthPerm54();
1098 }
1099
1100 // find the mapping from the old nodes to the new
1101 if ( pTemp0->nLeaves == pCut->nLeaves )
1102 uTruth0 = pTemp0->uTruth;
1103 else
1104 {
1105 assert( pTemp0->nLeaves < pCut->nLeaves );
1106 uPhase = 0;
1107 for ( i = 0; i < (int)pTemp0->nLeaves; i++ )
1108 {
1109 for ( k = 0; k < pCut->nLeaves; k++ )
1110 if ( pTemp0->ppLeaves[i] == pCut->ppLeaves[k] )
1111 break;
1112 uPhase |= (1 << k);
1113 }
1114 assert( uPhase < 32 );
1115 if ( pTemp0->nLeaves == 4 )
1116 {
1117 if ( uPhase == 31-16 ) // 01111
1118 uTruth0 = pTemp0->uTruth;
1119 else if ( uPhase == 31-8 ) // 10111
1120 uTruth0 = pPerms54[pTemp0->uTruth & 0xFFFF][0];
1121 else if ( uPhase == 31-4 ) // 11011
1122 uTruth0 = pPerms54[pTemp0->uTruth & 0xFFFF][1];
1123 else if ( uPhase == 31-2 ) // 11101
1124 uTruth0 = pPerms54[pTemp0->uTruth & 0xFFFF][2];
1125 else if ( uPhase == 31-1 ) // 11110
1126 uTruth0 = pPerms54[pTemp0->uTruth & 0xFFFF][3];
1127 else
1128 assert( 0 );
1129 }
1130 else
1131 uTruth0 = pPerms53[pTemp0->uTruth & 0xFF][uPhase];
1132 }
1133 uTruth0 = fComp0? ~uTruth0: uTruth0;
1134
1135 // find the mapping from the old nodes to the new
1136 if ( pTemp1->nLeaves == pCut->nLeaves )
1137 uTruth1 = pTemp1->uTruth;
1138 else
1139 {
1140 assert( pTemp1->nLeaves < pCut->nLeaves );
1141 uPhase = 0;
1142 for ( i = 0; i < (int)pTemp1->nLeaves; i++ )
1143 {
1144 for ( k = 0; k < pCut->nLeaves; k++ )
1145 if ( pTemp1->ppLeaves[i] == pCut->ppLeaves[k] )
1146 break;
1147 uPhase |= (1 << k);
1148 }
1149 assert( uPhase < 32 );
1150 if ( pTemp1->nLeaves == 4 )
1151 {
1152 if ( uPhase == 31-16 ) // 01111
1153 uTruth1 = pTemp1->uTruth;
1154 else if ( uPhase == 31-8 ) // 10111
1155 uTruth1 = pPerms54[pTemp1->uTruth & 0xFFFF][0];
1156 else if ( uPhase == 31-4 ) // 11011
1157 uTruth1 = pPerms54[pTemp1->uTruth & 0xFFFF][1];
1158 else if ( uPhase == 31-2 ) // 11101
1159 uTruth1 = pPerms54[pTemp1->uTruth & 0xFFFF][2];
1160 else if ( uPhase == 31-1 ) // 11110
1161 uTruth1 = pPerms54[pTemp1->uTruth & 0xFFFF][3];
1162 else
1163 assert( 0 );
1164 }
1165 else
1166 uTruth1 = pPerms53[pTemp1->uTruth & 0xFF][uPhase];
1167 }
1168 uTruth1 = fComp1? ~uTruth1: uTruth1;
1169 uTruth = uTruth0 & uTruth1;
1170 return uTruth;
1171}
1172
1176
1178
ABC_INT64_T abctime
Definition abc_global.h:332
#define ABC_PRT(a, t)
Definition abc_global.h:255
#define ABC_ALLOC(type, num)
Definition abc_global.h:264
#define ABC_FREE(obj)
Definition abc_global.h:267
#define ABC_NAMESPACE_IMPL_START
#define ABC_NAMESPACE_IMPL_END
int nTotal
DECLARATIONS ///.
Definition cutTruth.c:37
ABC_NAMESPACE_IMPL_START typedef char ProgressBar
Definition bbrNtbdd.c:27
Cube * p
Definition exorList.c:222
void Extra_ProgressBarStop(ProgressBar *p)
void Extra_MmFixedEntryRecycle(Extra_MmFixed_t *p, char *pEntry)
unsigned ** Extra_TruthPerm54()
ProgressBar * Extra_ProgressBarStart(FILE *pFile, int nItemsTotal)
FUNCTION DEFINITIONS ///.
unsigned ** Extra_TruthPerm53()
void Map_CutFree(Map_Man_t *p, Map_Cut_t *pCut)
int Map_MappingCountAllCuts(Map_Man_t *pMan)
FUNCTION DEFINITIONS ///.
Definition mapperCut.c:100
void Map_MappingCutsInput(Map_Man_t *p, Map_Node_t *pNode)
Definition mapperCut.c:158
#define Map_ListForEachCutSafe(pList, pCut, pCut2)
Definition mapperCut.c:78
struct Map_CutTableStrutct_t Map_CutTable_t
Definition mapperCut.c:34
Map_Cut_t * Map_CutMergeLists2(Map_Man_t *p, Map_CutTable_t *pTable, Map_Cut_t *pList1, Map_Cut_t *pList2, int fComp1, int fComp2)
Definition mapperCut.c:522
int Map_CutSortCutsCompare(Map_Cut_t **pC1, Map_Cut_t **pC2)
Definition mapperCut.c:980
#define Map_ListForEachCut(pList, pCut)
Definition mapperCut.c:74
void Map_MappingCuts(Map_Man_t *p)
GLOBAL VARIABLES ///.
Definition mapperCut.c:172
#define MAP_CUTS_MAX_COMPUTE
DECLARATIONS ///.
Definition mapperCut.c:29
#define MAP_CUTS_MAX_USE
Definition mapperCut.c:31
#define Map_CutNotCond(p, c)
Definition mapperInt.h:71
Map_Cut_t * Map_CutAlloc(Map_Man_t *p)
DECLARATIONS ///.
int Map_NodeComparePhase(Map_Node_t *p1, Map_Node_t *p2)
typedefABC_NAMESPACE_HEADER_START struct Map_ManStruct_t_ Map_Man_t
INCLUDES ///.
Definition mapper.h:40
int Map_NodeIsBuf(Map_Node_t *p)
struct Map_CutStruct_t_ Map_Cut_t
Definition mapper.h:43
int Map_NodeIsVar(Map_Node_t *p)
#define Map_Regular(p)
Definition mapper.h:68
int Map_NodeIsAnd(Map_Node_t *p)
#define Map_IsComplement(p)
GLOBAL VARIABLES ///.
Definition mapper.h:67
struct Map_NodeStruct_t_ Map_Node_t
Definition mapper.h:41
Map_Cut_t * pTwo
Definition mapperInt.h:268
Map_Match_t M[2]
Definition mapperInt.h:275
Map_Node_t * ppLeaves[6]
Definition mapperInt.h:269
Map_Cut_t * pOne
Definition mapperInt.h:267
unsigned uTruth
Definition mapperInt.h:270
Map_Cut_t * pNext
Definition mapperInt.h:266
Map_Cut_t ** pBins
Definition mapperCut.c:37
Map_Cut_t ** pCuts1
Definition mapperCut.c:42
Map_Cut_t ** pArray
Definition mapperCut.c:41
Map_Cut_t ** pCuts2
Definition mapperCut.c:43
Map_Cut_t * pCutBest[2]
Definition mapperInt.h:243
Map_Node_t * pNextE
Definition mapperInt.h:227
Map_Node_t * pRepr
Definition mapperInt.h:228
Map_Node_t * pNext
Definition mapperInt.h:209
Map_Node_t * p2
Definition mapperInt.h:226
Map_Cut_t * pCuts
Definition mapperInt.h:244
Map_Node_t * p1
Definition mapperInt.h:225
#define assert(ex)
Definition util_old.h:213
char * memset()