ABC: A System for Sequential Synthesis and Verification
 
Loading...
Searching...
No Matches
abcResub.c
Go to the documentation of this file.
1
20
21#include "base/abc/abc.h"
22#include "bool/dec/dec.h"
23
24ABC_NAMESPACE_IMPL_START
25
26
30
31#define ABC_RS_DIV1_MAX 150 // the max number of divisors to consider
32#define ABC_RS_DIV2_MAX 500 // the max number of pair-wise divisors to consider
33
34typedef struct Abc_ManRes_t_ Abc_ManRes_t;
35struct Abc_ManRes_t_
36{
37 // paramers
38 int nLeavesMax; // the max number of leaves in the cone
39 int nDivsMax; // the max number of divisors in the cone
40 // representation of the cone
41 Abc_Obj_t * pRoot; // the root of the cone
42 int nLeaves; // the number of leaves
43 int nDivs; // the number of all divisor (including leaves)
44 int nMffc; // the size of MFFC
45 int nLastGain; // the gain the number of nodes
46 Vec_Ptr_t * vDivs; // the divisors
47 // representation of the simulation info
48 int nBits; // the number of simulation bits
49 int nWords; // the number of unsigneds for siminfo
50 Vec_Ptr_t * vSims; // simulation info
51 unsigned * pInfo; // pointer to simulation info
52 // observability don't-cares
53 unsigned * pCareSet;
54 // internal divisor storage
55 Vec_Ptr_t * vDivs1UP; // the single-node unate divisors
56 Vec_Ptr_t * vDivs1UN; // the single-node unate divisors
57 Vec_Ptr_t * vDivs1B; // the single-node binate divisors
58 Vec_Ptr_t * vDivs2UP0; // the double-node unate divisors
59 Vec_Ptr_t * vDivs2UP1; // the double-node unate divisors
60 Vec_Ptr_t * vDivs2UN0; // the double-node unate divisors
61 Vec_Ptr_t * vDivs2UN1; // the double-node unate divisors
62 // other data
63 Vec_Ptr_t * vTemp; // temporary array of nodes
64 // runtime statistics
65 abctime timeCut;
66 abctime timeTruth;
67 abctime timeRes;
68 abctime timeDiv;
69 abctime timeMffc;
70 abctime timeSim;
71 abctime timeRes1;
72 abctime timeResD;
73 abctime timeRes2;
74 abctime timeRes3;
75 abctime timeNtk;
76 abctime timeTotal;
77 // improvement statistics
78 int nUsedNodeC;
79 int nUsedNode0;
80 int nUsedNode1Or;
81 int nUsedNode1And;
82 int nUsedNode2Or;
83 int nUsedNode2And;
84 int nUsedNode2OrAnd;
85 int nUsedNode2AndOr;
86 int nUsedNode3OrAnd;
87 int nUsedNode3AndOr;
88 int nUsedNodeTotal;
89 int nTotalDivs;
90 int nTotalLeaves;
91 int nTotalGain;
92 int nNodesBeg;
93 int nNodesEnd;
94};
95
96// external procedures
97static Abc_ManRes_t* Abc_ManResubStart( int nLeavesMax, int nDivsMax );
98static void Abc_ManResubStop( Abc_ManRes_t * p );
99static Dec_Graph_t * Abc_ManResubEval( Abc_ManRes_t * p, Abc_Obj_t * pRoot, Vec_Ptr_t * vLeaves, int nSteps, int fUpdateLevel, int fVerbose );
100static void Abc_ManResubCleanup( Abc_ManRes_t * p );
101static void Abc_ManResubPrint( Abc_ManRes_t * p );
102
103// other procedures
104static int Abc_ManResubCollectDivs( Abc_ManRes_t * p, Abc_Obj_t * pRoot, Vec_Ptr_t * vLeaves, int Required );
105static void Abc_ManResubSimulate( Vec_Ptr_t * vDivs, int nLeaves, Vec_Ptr_t * vSims, int nLeavesMax, int nWords );
106static void Abc_ManResubPrintDivs( Abc_ManRes_t * p, Abc_Obj_t * pRoot, Vec_Ptr_t * vLeaves );
107
108static void Abc_ManResubDivsS( Abc_ManRes_t * p, int Required );
109static void Abc_ManResubDivsD( Abc_ManRes_t * p, int Required );
110static Dec_Graph_t * Abc_ManResubQuit( Abc_ManRes_t * p );
111static Dec_Graph_t * Abc_ManResubDivs0( Abc_ManRes_t * p );
112static Dec_Graph_t * Abc_ManResubDivs1( Abc_ManRes_t * p, int Required );
113static Dec_Graph_t * Abc_ManResubDivs12( Abc_ManRes_t * p, int Required );
114static Dec_Graph_t * Abc_ManResubDivs2( Abc_ManRes_t * p, int Required );
115static Dec_Graph_t * Abc_ManResubDivs3( Abc_ManRes_t * p, int Required );
116
117static Vec_Ptr_t * Abc_CutFactorLarge( Abc_Obj_t * pNode, int nLeavesMax );
118static int Abc_CutVolumeCheck( Abc_Obj_t * pNode, Vec_Ptr_t * vLeaves );
119
120//extern abctime s_ResubTime;
121
125
137int Abc_NtkResubstitute( Abc_Ntk_t * pNtk, int nCutMax, int nStepsMax, int nMinSaved, int nLevelsOdc, int fUpdateLevel, int fVerbose, int fVeryVerbose )
138{
139 extern int Dec_GraphUpdateNetwork( Abc_Obj_t * pRoot, Dec_Graph_t * pGraph, int fUpdateLevel, int nGain );
140 ProgressBar * pProgress;
141 Abc_ManRes_t * pManRes;
142 Abc_ManCut_t * pManCut;
143 Odc_Man_t * pManOdc = NULL;
144 Dec_Graph_t * pFForm;
145 Vec_Ptr_t * vLeaves;
146 Abc_Obj_t * pNode;
147 abctime clk, clkStart = Abc_Clock();
148 int i, nNodes;
149
150 assert( Abc_NtkIsStrash(pNtk) );
151
152 // cleanup the AIG
153 Abc_AigCleanup((Abc_Aig_t *)pNtk->pManFunc);
154 // start the managers
155 pManCut = Abc_NtkManCutStart( nCutMax, 100000, 100000, 100000 );
156 pManRes = Abc_ManResubStart( nCutMax, ABC_RS_DIV1_MAX );
157 if ( nLevelsOdc > 0 )
158 pManOdc = Abc_NtkDontCareAlloc( nCutMax, nLevelsOdc, fVerbose, fVeryVerbose );
159
160 // compute the reverse levels if level update is requested
161 if ( fUpdateLevel )
162 Abc_NtkStartReverseLevels( pNtk, 0 );
163
164 if ( Abc_NtkLatchNum(pNtk) ) {
165 Abc_NtkForEachLatch(pNtk, pNode, i)
166 pNode->pNext = (Abc_Obj_t *)pNode->pData;
167 }
168
169 // resynthesize each node once
170 pManRes->nNodesBeg = Abc_NtkNodeNum(pNtk);
171 nNodes = Abc_NtkObjNumMax(pNtk);
172 pProgress = Extra_ProgressBarStart( stdout, nNodes );
173 //clear markAB at the beginning
174 Abc_NtkCleanMarkAB( pNtk );
175 Abc_NtkForEachNode( pNtk, pNode, i )
176 {
177 Extra_ProgressBarUpdate( pProgress, i, NULL );
178 // skip the constant node
179// if ( Abc_NodeIsConst(pNode) )
180// continue;
181 // skip persistant nodes
182 if ( Abc_NodeIsPersistant(pNode) )
183 continue;
184 // skip the nodes with many fanouts
185 if ( Abc_ObjFanoutNum(pNode) > 1000 )
186 continue;
187 // stop if all nodes have been tried once
188 if ( i >= nNodes )
189 break;
190
191 // compute a reconvergence-driven cut
192clk = Abc_Clock();
193 vLeaves = Abc_NodeFindCut( pManCut, pNode, 0 );
194// vLeaves = Abc_CutFactorLarge( pNode, nCutMax );
195pManRes->timeCut += Abc_Clock() - clk;
196/*
197 if ( fVerbose && vLeaves )
198 printf( "Node %6d : Leaves = %3d. Volume = %3d.\n", pNode->Id, Vec_PtrSize(vLeaves), Abc_CutVolumeCheck(pNode, vLeaves) );
199 if ( vLeaves == NULL )
200 continue;
201*/
202 // get the don't-cares
203 if ( pManOdc )
204 {
205clk = Abc_Clock();
206 Abc_NtkDontCareClear( pManOdc );
207 Abc_NtkDontCareCompute( pManOdc, pNode, vLeaves, pManRes->pCareSet );
208pManRes->timeTruth += Abc_Clock() - clk;
209 }
210
211 // evaluate this cut
212clk = Abc_Clock();
213 pFForm = Abc_ManResubEval( pManRes, pNode, vLeaves, nStepsMax, fUpdateLevel, fVerbose );
214// Vec_PtrFree( vLeaves );
215// Abc_ManResubCleanup( pManRes );
216pManRes->timeRes += Abc_Clock() - clk;
217 if ( pFForm == NULL )
218 continue;
219 if ( pManRes->nLastGain < nMinSaved )
220 {
221 Dec_GraphFree( pFForm );
222 continue;
223 }
224 pManRes->nTotalGain += pManRes->nLastGain;
225/*
226 if ( pManRes->nLeaves == 4 && pManRes->nMffc == 2 && pManRes->nLastGain == 1 )
227 {
228 printf( "%6d : L = %2d. V = %2d. Mffc = %2d. Divs = %3d. Up = %3d. Un = %3d. B = %3d.\n",
229 pNode->Id, pManRes->nLeaves, Abc_CutVolumeCheck(pNode, vLeaves), pManRes->nMffc, pManRes->nDivs,
230 pManRes->vDivs1UP->nSize, pManRes->vDivs1UN->nSize, pManRes->vDivs1B->nSize );
231 Abc_ManResubPrintDivs( pManRes, pNode, vLeaves );
232 }
233*/
234 // acceptable replacement found, update the graph
235clk = Abc_Clock();
236 Dec_GraphUpdateNetwork( pNode, pFForm, fUpdateLevel, pManRes->nLastGain );
237pManRes->timeNtk += Abc_Clock() - clk;
238 Dec_GraphFree( pFForm );
239 }
240 Extra_ProgressBarStop( pProgress );
241pManRes->timeTotal = Abc_Clock() - clkStart;
242 pManRes->nNodesEnd = Abc_NtkNodeNum(pNtk);
243
244 // print statistics
245 if ( fVerbose )
246 Abc_ManResubPrint( pManRes );
247
248 // delete the managers
249 Abc_ManResubStop( pManRes );
250 Abc_NtkManCutStop( pManCut );
251 if ( pManOdc ) Abc_NtkDontCareFree( pManOdc );
252
253 // clean the data field
254 Abc_NtkForEachObj( pNtk, pNode, i )
255 pNode->pData = NULL;
256
257 if ( Abc_NtkLatchNum(pNtk) ) {
258 Abc_NtkForEachLatch(pNtk, pNode, i)
259 pNode->pData = pNode->pNext, pNode->pNext = NULL;
260 }
261
262 // put the nodes into the DFS order and reassign their IDs
263 Abc_NtkReassignIds( pNtk );
264// Abc_AigCheckFaninOrder( pNtk->pManFunc );
265 // fix the levels
266 if ( fUpdateLevel )
267 Abc_NtkStopReverseLevels( pNtk );
268 else
269 Abc_NtkLevel( pNtk );
270 // check
271 if ( !Abc_NtkCheck( pNtk ) )
272 {
273 printf( "Abc_NtkRefactor: The network check has failed.\n" );
274 return 0;
275 }
276//s_ResubTime = Abc_Clock() - clkStart;
277 return 1;
278}
279
280
281
282
294Abc_ManRes_t * Abc_ManResubStart( int nLeavesMax, int nDivsMax )
295{
296 Abc_ManRes_t * p;
297 unsigned * pData;
298 int i, k;
299 assert( sizeof(unsigned) == 4 );
300 p = ABC_ALLOC( Abc_ManRes_t, 1 );
301 memset( p, 0, sizeof(Abc_ManRes_t) );
302 p->nLeavesMax = nLeavesMax;
303 p->nDivsMax = nDivsMax;
304 p->vDivs = Vec_PtrAlloc( p->nDivsMax );
305 // allocate simulation info
306 p->nBits = (1 << p->nLeavesMax);
307 p->nWords = (p->nBits <= 32)? 1 : (p->nBits / 32);
308 p->pInfo = ABC_ALLOC( unsigned, p->nWords * (p->nDivsMax + 1) );
309 memset( p->pInfo, 0, sizeof(unsigned) * p->nWords * p->nLeavesMax );
310 p->vSims = Vec_PtrAlloc( p->nDivsMax );
311 for ( i = 0; i < p->nDivsMax; i++ )
312 Vec_PtrPush( p->vSims, p->pInfo + i * p->nWords );
313 // assign the care set
314 p->pCareSet = p->pInfo + p->nDivsMax * p->nWords;
315 Abc_InfoFill( p->pCareSet, p->nWords );
316 // set elementary truth tables
317 for ( k = 0; k < p->nLeavesMax; k++ )
318 {
319 pData = (unsigned *)p->vSims->pArray[k];
320 for ( i = 0; i < p->nBits; i++ )
321 if ( i & (1 << k) )
322 pData[i>>5] |= (1 << (i&31));
323 }
324 // create the remaining divisors
325 p->vDivs1UP = Vec_PtrAlloc( p->nDivsMax );
326 p->vDivs1UN = Vec_PtrAlloc( p->nDivsMax );
327 p->vDivs1B = Vec_PtrAlloc( p->nDivsMax );
328 p->vDivs2UP0 = Vec_PtrAlloc( p->nDivsMax );
329 p->vDivs2UP1 = Vec_PtrAlloc( p->nDivsMax );
330 p->vDivs2UN0 = Vec_PtrAlloc( p->nDivsMax );
331 p->vDivs2UN1 = Vec_PtrAlloc( p->nDivsMax );
332 p->vTemp = Vec_PtrAlloc( p->nDivsMax );
333 return p;
334}
335
347void Abc_ManResubStop( Abc_ManRes_t * p )
348{
349 Vec_PtrFree( p->vDivs );
350 Vec_PtrFree( p->vSims );
351 Vec_PtrFree( p->vDivs1UP );
352 Vec_PtrFree( p->vDivs1UN );
353 Vec_PtrFree( p->vDivs1B );
354 Vec_PtrFree( p->vDivs2UP0 );
355 Vec_PtrFree( p->vDivs2UP1 );
356 Vec_PtrFree( p->vDivs2UN0 );
357 Vec_PtrFree( p->vDivs2UN1 );
358 Vec_PtrFree( p->vTemp );
359 ABC_FREE( p->pInfo );
360 ABC_FREE( p );
361}
362
374void Abc_ManResubPrint( Abc_ManRes_t * p )
375{
376 printf( "Used constants = %6d. ", p->nUsedNodeC ); ABC_PRT( "Cuts ", p->timeCut );
377 printf( "Used replacements = %6d. ", p->nUsedNode0 ); ABC_PRT( "Resub ", p->timeRes );
378 printf( "Used single ORs = %6d. ", p->nUsedNode1Or ); ABC_PRT( " Div ", p->timeDiv );
379 printf( "Used single ANDs = %6d. ", p->nUsedNode1And ); ABC_PRT( " Mffc ", p->timeMffc );
380 printf( "Used double ORs = %6d. ", p->nUsedNode2Or ); ABC_PRT( " Sim ", p->timeSim );
381 printf( "Used double ANDs = %6d. ", p->nUsedNode2And ); ABC_PRT( " 1 ", p->timeRes1 );
382 printf( "Used OR-AND = %6d. ", p->nUsedNode2OrAnd ); ABC_PRT( " D ", p->timeResD );
383 printf( "Used AND-OR = %6d. ", p->nUsedNode2AndOr ); ABC_PRT( " 2 ", p->timeRes2 );
384 printf( "Used OR-2ANDs = %6d. ", p->nUsedNode3OrAnd ); ABC_PRT( "Truth ", p->timeTruth ); //ABC_PRT( " 3 ", p->timeRes3 );
385 printf( "Used AND-2ORs = %6d. ", p->nUsedNode3AndOr ); ABC_PRT( "AIG ", p->timeNtk );
386 printf( "TOTAL = %6d. ", p->nUsedNodeC +
387 p->nUsedNode0 +
388 p->nUsedNode1Or +
389 p->nUsedNode1And +
390 p->nUsedNode2Or +
391 p->nUsedNode2And +
392 p->nUsedNode2OrAnd +
393 p->nUsedNode2AndOr +
394 p->nUsedNode3OrAnd +
395 p->nUsedNode3AndOr
396 ); ABC_PRT( "TOTAL ", p->timeTotal );
397 printf( "Total leaves = %8d.\n", p->nTotalLeaves );
398 printf( "Total divisors = %8d.\n", p->nTotalDivs );
399// printf( "Total gain = %8d.\n", p->nTotalGain );
400 printf( "Gain = %8d. (%6.2f %%).\n", p->nNodesBeg-p->nNodesEnd, 100.0*(p->nNodesBeg-p->nNodesEnd)/p->nNodesBeg );
401}
402
403
415void Abc_ManResubCollectDivs_rec( Abc_Obj_t * pNode, Vec_Ptr_t * vInternal )
416{
417 // skip visited nodes
418 if ( Abc_NodeIsTravIdCurrent(pNode) )
419 return;
420 Abc_NodeSetTravIdCurrent(pNode);
421 // collect the fanins
422 Abc_ManResubCollectDivs_rec( Abc_ObjFanin0(pNode), vInternal );
423 Abc_ManResubCollectDivs_rec( Abc_ObjFanin1(pNode), vInternal );
424 // collect the internal node
425 if ( pNode->fMarkA == 0 )
426 Vec_PtrPush( vInternal, pNode );
427}
428
440int Abc_ManResubCollectDivs( Abc_ManRes_t * p, Abc_Obj_t * pRoot, Vec_Ptr_t * vLeaves, int Required )
441{
442 Abc_Obj_t * pNode, * pFanout;
443 int i, k, Limit, Counter;
444
445 Vec_PtrClear( p->vDivs1UP );
446 Vec_PtrClear( p->vDivs1UN );
447 Vec_PtrClear( p->vDivs1B );
448
449 // add the leaves of the cuts to the divisors
450 Vec_PtrClear( p->vDivs );
451 Abc_NtkIncrementTravId( pRoot->pNtk );
452 Vec_PtrForEachEntry( Abc_Obj_t *, vLeaves, pNode, i )
453 {
454 Vec_PtrPush( p->vDivs, pNode );
455 Abc_NodeSetTravIdCurrent( pNode );
456 }
457
458 // mark nodes in the MFFC
459 Vec_PtrForEachEntry( Abc_Obj_t *, p->vTemp, pNode, i )
460 pNode->fMarkA = 1;
461 // collect the cone (without MFFC)
462 Abc_ManResubCollectDivs_rec( pRoot, p->vDivs );
463 // unmark the current MFFC
464 Vec_PtrForEachEntry( Abc_Obj_t *, p->vTemp, pNode, i )
465 pNode->fMarkA = 0;
466
467 // check if the number of divisors is not exceeded
468 if ( Vec_PtrSize(p->vDivs) - Vec_PtrSize(vLeaves) + Vec_PtrSize(p->vTemp) >= Vec_PtrSize(p->vSims) - p->nLeavesMax )
469 return 0;
470
471 // get the number of divisors to collect
472 Limit = Vec_PtrSize(p->vSims) - p->nLeavesMax - (Vec_PtrSize(p->vDivs) - Vec_PtrSize(vLeaves) + Vec_PtrSize(p->vTemp));
473
474 // explore the fanouts, which are not in the MFFC
475 Counter = 0;
476 Vec_PtrForEachEntry( Abc_Obj_t *, p->vDivs, pNode, i )
477 {
478 if ( Abc_ObjFanoutNum(pNode) > 100 )
479 {
480// printf( "%d ", Abc_ObjFanoutNum(pNode) );
481 continue;
482 }
483 // if the fanout has both fanins in the set, add it
484 Abc_ObjForEachFanout( pNode, pFanout, k )
485 {
486 if ( Abc_NodeIsTravIdCurrent(pFanout) || Abc_ObjIsCo(pFanout) || (int)pFanout->Level > Required )
487 continue;
488 if ( Abc_NodeIsTravIdCurrent(Abc_ObjFanin0(pFanout)) && Abc_NodeIsTravIdCurrent(Abc_ObjFanin1(pFanout)) )
489 {
490 if ( Abc_ObjFanin0(pFanout) == pRoot || Abc_ObjFanin1(pFanout) == pRoot )
491 continue;
492 Vec_PtrPush( p->vDivs, pFanout );
493 Abc_NodeSetTravIdCurrent( pFanout );
494 // quit computing divisors if there is too many of them
495 if ( ++Counter == Limit )
496 goto Quits;
497 }
498 }
499 }
500
501Quits :
502 // get the number of divisors
503 p->nDivs = Vec_PtrSize(p->vDivs);
504
505 // add the nodes in the MFFC
506 Vec_PtrForEachEntry( Abc_Obj_t *, p->vTemp, pNode, i )
507 Vec_PtrPush( p->vDivs, pNode );
508 assert( pRoot == Vec_PtrEntryLast(p->vDivs) );
509
510 assert( Vec_PtrSize(p->vDivs) - Vec_PtrSize(vLeaves) <= Vec_PtrSize(p->vSims) - p->nLeavesMax );
511 return 1;
512}
513
525void Abc_ManResubPrintDivs( Abc_ManRes_t * p, Abc_Obj_t * pRoot, Vec_Ptr_t * vLeaves )
526{
527 Abc_Obj_t * pFanin, * pNode;
528 int i, k;
529 // print the nodes
530 Vec_PtrForEachEntry( Abc_Obj_t *, p->vDivs, pNode, i )
531 {
532 if ( i < Vec_PtrSize(vLeaves) )
533 {
534 printf( "%6d : %c\n", pNode->Id, 'a'+i );
535 continue;
536 }
537 printf( "%6d : %2d = ", pNode->Id, i );
538 // find the first fanin
539 Vec_PtrForEachEntry( Abc_Obj_t *, p->vDivs, pFanin, k )
540 if ( Abc_ObjFanin0(pNode) == pFanin )
541 break;
542 if ( k < Vec_PtrSize(vLeaves) )
543 printf( "%c", 'a' + k );
544 else
545 printf( "%d", k );
546 printf( "%s ", Abc_ObjFaninC0(pNode)? "\'" : "" );
547 // find the second fanin
548 Vec_PtrForEachEntry( Abc_Obj_t *, p->vDivs, pFanin, k )
549 if ( Abc_ObjFanin1(pNode) == pFanin )
550 break;
551 if ( k < Vec_PtrSize(vLeaves) )
552 printf( "%c", 'a' + k );
553 else
554 printf( "%d", k );
555 printf( "%s ", Abc_ObjFaninC1(pNode)? "\'" : "" );
556 if ( pNode == pRoot )
557 printf( " root" );
558 printf( "\n" );
559 }
560 printf( "\n" );
561}
562
574void Abc_ManResubDumpInstance( Vec_Ptr_t * vDivs, int nLeaves, int nDivs, int nWords )
575{
576 Abc_Obj_t * pRoot = (Abc_Obj_t *)Vec_PtrEntryLast(vDivs);
577 char pFileName[1000];
578 sprintf( pFileName, "%s_%05d.pla", pRoot->pNtk->pName, pRoot->Id );
579 FILE * pFile = fopen( pFileName, "wb" );
580 if ( pFile == NULL ) {
581 printf( "Cannot open file \"%s\" for writing.\n", pFileName );
582 return;
583 }
584 fprintf( pFile, "// Resub instance generated for node %d in network \"%s\" on %s\n", pRoot->Id, pRoot->pNtk->pName, Extra_TimeStamp() );
585 fprintf( pFile, ".i %d\n", nDivs );
586 fprintf( pFile, ".o %d\n", 1 );
587 fprintf( pFile, ".p %d\n", 1 << nLeaves );
588 Abc_Obj_t * pObj; int i, n;
589 for ( n = 0; n < (1 << nLeaves); n++ ) {
590 Vec_PtrForEachEntryStop( Abc_Obj_t *, vDivs, pObj, i, nDivs ) {
591 fprintf( pFile, "%d", Abc_InfoHasBit((unsigned *)pObj->pData, n) );
592 if ( i == nLeaves-1 )
593 fprintf( pFile, " " );
594 }
595 fprintf( pFile, " %d\n", Abc_InfoHasBit((unsigned *)pRoot->pData, n) );
596 }
597 fprintf( pFile, ".e\n" );
598 fclose( pFile );
599 printf( "Finished dumping file \"%s\" with %d divisors and %d patterns.\n", pFileName, nDivs, (1 << nLeaves) );
600}
601
613void Abc_ManResubSimulate( Vec_Ptr_t * vDivs, int nLeaves, Vec_Ptr_t * vSims, int nLeavesMax, int nWords )
614{
615 Abc_Obj_t * pObj;
616 unsigned * puData0, * puData1, * puData;
617 int i, k;
618 assert( Vec_PtrSize(vDivs) - nLeaves <= Vec_PtrSize(vSims) - nLeavesMax );
619 // simulate
620 Vec_PtrForEachEntry( Abc_Obj_t *, vDivs, pObj, i )
621 {
622 if ( i < nLeaves )
623 { // initialize the leaf
624 pObj->pData = Vec_PtrEntry( vSims, i );
625 continue;
626 }
627 // set storage for the node's simulation info
628 pObj->pData = Vec_PtrEntry( vSims, i - nLeaves + nLeavesMax );
629 // get pointer to the simulation info
630 puData = (unsigned *)pObj->pData;
631 puData0 = (unsigned *)Abc_ObjFanin0(pObj)->pData;
632 puData1 = (unsigned *)Abc_ObjFanin1(pObj)->pData;
633 // simulate
634 if ( Abc_ObjFaninC0(pObj) && Abc_ObjFaninC1(pObj) )
635 for ( k = 0; k < nWords; k++ )
636 puData[k] = ~puData0[k] & ~puData1[k];
637 else if ( Abc_ObjFaninC0(pObj) )
638 for ( k = 0; k < nWords; k++ )
639 puData[k] = ~puData0[k] & puData1[k];
640 else if ( Abc_ObjFaninC1(pObj) )
641 for ( k = 0; k < nWords; k++ )
642 puData[k] = puData0[k] & ~puData1[k];
643 else
644 for ( k = 0; k < nWords; k++ )
645 puData[k] = puData0[k] & puData1[k];
646 }
647 // normalize
648 Vec_PtrForEachEntry( Abc_Obj_t *, vDivs, pObj, i )
649 {
650 puData = (unsigned *)pObj->pData;
651 pObj->fPhase = (puData[0] & 1);
652 if ( pObj->fPhase )
653 for ( k = 0; k < nWords; k++ )
654 puData[k] = ~puData[k];
655 }
656}
657
658
670Dec_Graph_t * Abc_ManResubQuit0( Abc_Obj_t * pRoot, Abc_Obj_t * pObj )
671{
672 Dec_Graph_t * pGraph;
673 Dec_Edge_t eRoot;
674 pGraph = Dec_GraphCreate( 1 );
675 Dec_GraphNode( pGraph, 0 )->pFunc = pObj;
676 eRoot = Dec_EdgeCreate( 0, pObj->fPhase );
677 Dec_GraphSetRoot( pGraph, eRoot );
678 if ( pRoot->fPhase )
679 Dec_GraphComplement( pGraph );
680 return pGraph;
681}
682
694Dec_Graph_t * Abc_ManResubQuit1( Abc_Obj_t * pRoot, Abc_Obj_t * pObj0, Abc_Obj_t * pObj1, int fOrGate )
695{
696 Dec_Graph_t * pGraph;
697 Dec_Edge_t eRoot, eNode0, eNode1;
698 assert( Abc_ObjRegular(pObj0) != Abc_ObjRegular(pObj1) );
699 pGraph = Dec_GraphCreate( 2 );
700 Dec_GraphNode( pGraph, 0 )->pFunc = Abc_ObjRegular(pObj0);
701 Dec_GraphNode( pGraph, 1 )->pFunc = Abc_ObjRegular(pObj1);
702 eNode0 = Dec_EdgeCreate( 0, Abc_ObjRegular(pObj0)->fPhase ^ Abc_ObjIsComplement(pObj0) );
703 eNode1 = Dec_EdgeCreate( 1, Abc_ObjRegular(pObj1)->fPhase ^ Abc_ObjIsComplement(pObj1) );
704 if ( fOrGate )
705 eRoot = Dec_GraphAddNodeOr( pGraph, eNode0, eNode1 );
706 else
707 eRoot = Dec_GraphAddNodeAnd( pGraph, eNode0, eNode1 );
708 Dec_GraphSetRoot( pGraph, eRoot );
709 if ( pRoot->fPhase )
710 Dec_GraphComplement( pGraph );
711 return pGraph;
712}
713
725Dec_Graph_t * Abc_ManResubQuit21( Abc_Obj_t * pRoot, Abc_Obj_t * pObj0, Abc_Obj_t * pObj1, Abc_Obj_t * pObj2, int fOrGate )
726{
727 Dec_Graph_t * pGraph;
728 Dec_Edge_t eRoot, eNode0, eNode1, eNode2;
729 assert( Abc_ObjRegular(pObj0) != Abc_ObjRegular(pObj1) );
730 assert( Abc_ObjRegular(pObj0) != Abc_ObjRegular(pObj2) );
731 assert( Abc_ObjRegular(pObj1) != Abc_ObjRegular(pObj2) );
732 pGraph = Dec_GraphCreate( 3 );
733 Dec_GraphNode( pGraph, 0 )->pFunc = Abc_ObjRegular(pObj0);
734 Dec_GraphNode( pGraph, 1 )->pFunc = Abc_ObjRegular(pObj1);
735 Dec_GraphNode( pGraph, 2 )->pFunc = Abc_ObjRegular(pObj2);
736 eNode0 = Dec_EdgeCreate( 0, Abc_ObjRegular(pObj0)->fPhase ^ Abc_ObjIsComplement(pObj0) );
737 eNode1 = Dec_EdgeCreate( 1, Abc_ObjRegular(pObj1)->fPhase ^ Abc_ObjIsComplement(pObj1) );
738 eNode2 = Dec_EdgeCreate( 2, Abc_ObjRegular(pObj2)->fPhase ^ Abc_ObjIsComplement(pObj2) );
739 if ( fOrGate )
740 {
741 eRoot = Dec_GraphAddNodeOr( pGraph, eNode0, eNode1 );
742 eRoot = Dec_GraphAddNodeOr( pGraph, eNode2, eRoot );
743 }
744 else
745 {
746 eRoot = Dec_GraphAddNodeAnd( pGraph, eNode0, eNode1 );
747 eRoot = Dec_GraphAddNodeAnd( pGraph, eNode2, eRoot );
748 }
749 Dec_GraphSetRoot( pGraph, eRoot );
750 if ( pRoot->fPhase )
751 Dec_GraphComplement( pGraph );
752 return pGraph;
753}
754
766Dec_Graph_t * Abc_ManResubQuit2( Abc_Obj_t * pRoot, Abc_Obj_t * pObj0, Abc_Obj_t * pObj1, Abc_Obj_t * pObj2, int fOrGate )
767{
768 Dec_Graph_t * pGraph;
769 Dec_Edge_t eRoot, ePrev, eNode0, eNode1, eNode2;
770 assert( Abc_ObjRegular(pObj0) != Abc_ObjRegular(pObj1) );
771 assert( Abc_ObjRegular(pObj0) != Abc_ObjRegular(pObj2) );
772 assert( Abc_ObjRegular(pObj1) != Abc_ObjRegular(pObj2) );
773 pGraph = Dec_GraphCreate( 3 );
774 Dec_GraphNode( pGraph, 0 )->pFunc = Abc_ObjRegular(pObj0);
775 Dec_GraphNode( pGraph, 1 )->pFunc = Abc_ObjRegular(pObj1);
776 Dec_GraphNode( pGraph, 2 )->pFunc = Abc_ObjRegular(pObj2);
777 eNode0 = Dec_EdgeCreate( 0, Abc_ObjRegular(pObj0)->fPhase ^ Abc_ObjIsComplement(pObj0) );
778 if ( Abc_ObjIsComplement(pObj1) && Abc_ObjIsComplement(pObj2) )
779 {
780 eNode1 = Dec_EdgeCreate( 1, Abc_ObjRegular(pObj1)->fPhase );
781 eNode2 = Dec_EdgeCreate( 2, Abc_ObjRegular(pObj2)->fPhase );
782 ePrev = Dec_GraphAddNodeOr( pGraph, eNode1, eNode2 );
783 }
784 else
785 {
786 eNode1 = Dec_EdgeCreate( 1, Abc_ObjRegular(pObj1)->fPhase ^ Abc_ObjIsComplement(pObj1) );
787 eNode2 = Dec_EdgeCreate( 2, Abc_ObjRegular(pObj2)->fPhase ^ Abc_ObjIsComplement(pObj2) );
788 ePrev = Dec_GraphAddNodeAnd( pGraph, eNode1, eNode2 );
789 }
790 if ( fOrGate )
791 eRoot = Dec_GraphAddNodeOr( pGraph, eNode0, ePrev );
792 else
793 eRoot = Dec_GraphAddNodeAnd( pGraph, eNode0, ePrev );
794 Dec_GraphSetRoot( pGraph, eRoot );
795 if ( pRoot->fPhase )
796 Dec_GraphComplement( pGraph );
797 return pGraph;
798}
799
811Dec_Graph_t * Abc_ManResubQuit3( Abc_Obj_t * pRoot, Abc_Obj_t * pObj0, Abc_Obj_t * pObj1, Abc_Obj_t * pObj2, Abc_Obj_t * pObj3, int fOrGate )
812{
813 Dec_Graph_t * pGraph;
814 Dec_Edge_t eRoot, ePrev0, ePrev1, eNode0, eNode1, eNode2, eNode3;
815 assert( Abc_ObjRegular(pObj0) != Abc_ObjRegular(pObj1) );
816 assert( Abc_ObjRegular(pObj2) != Abc_ObjRegular(pObj3) );
817 pGraph = Dec_GraphCreate( 4 );
818 Dec_GraphNode( pGraph, 0 )->pFunc = Abc_ObjRegular(pObj0);
819 Dec_GraphNode( pGraph, 1 )->pFunc = Abc_ObjRegular(pObj1);
820 Dec_GraphNode( pGraph, 2 )->pFunc = Abc_ObjRegular(pObj2);
821 Dec_GraphNode( pGraph, 3 )->pFunc = Abc_ObjRegular(pObj3);
822 if ( Abc_ObjIsComplement(pObj0) && Abc_ObjIsComplement(pObj1) )
823 {
824 eNode0 = Dec_EdgeCreate( 0, Abc_ObjRegular(pObj0)->fPhase );
825 eNode1 = Dec_EdgeCreate( 1, Abc_ObjRegular(pObj1)->fPhase );
826 ePrev0 = Dec_GraphAddNodeOr( pGraph, eNode0, eNode1 );
827 if ( Abc_ObjIsComplement(pObj2) && Abc_ObjIsComplement(pObj3) )
828 {
829 eNode2 = Dec_EdgeCreate( 2, Abc_ObjRegular(pObj2)->fPhase );
830 eNode3 = Dec_EdgeCreate( 3, Abc_ObjRegular(pObj3)->fPhase );
831 ePrev1 = Dec_GraphAddNodeOr( pGraph, eNode2, eNode3 );
832 }
833 else
834 {
835 eNode2 = Dec_EdgeCreate( 2, Abc_ObjRegular(pObj2)->fPhase ^ Abc_ObjIsComplement(pObj2) );
836 eNode3 = Dec_EdgeCreate( 3, Abc_ObjRegular(pObj3)->fPhase ^ Abc_ObjIsComplement(pObj3) );
837 ePrev1 = Dec_GraphAddNodeAnd( pGraph, eNode2, eNode3 );
838 }
839 }
840 else
841 {
842 eNode0 = Dec_EdgeCreate( 0, Abc_ObjRegular(pObj0)->fPhase ^ Abc_ObjIsComplement(pObj0) );
843 eNode1 = Dec_EdgeCreate( 1, Abc_ObjRegular(pObj1)->fPhase ^ Abc_ObjIsComplement(pObj1) );
844 ePrev0 = Dec_GraphAddNodeAnd( pGraph, eNode0, eNode1 );
845 if ( Abc_ObjIsComplement(pObj2) && Abc_ObjIsComplement(pObj3) )
846 {
847 eNode2 = Dec_EdgeCreate( 2, Abc_ObjRegular(pObj2)->fPhase );
848 eNode3 = Dec_EdgeCreate( 3, Abc_ObjRegular(pObj3)->fPhase );
849 ePrev1 = Dec_GraphAddNodeOr( pGraph, eNode2, eNode3 );
850 }
851 else
852 {
853 eNode2 = Dec_EdgeCreate( 2, Abc_ObjRegular(pObj2)->fPhase ^ Abc_ObjIsComplement(pObj2) );
854 eNode3 = Dec_EdgeCreate( 3, Abc_ObjRegular(pObj3)->fPhase ^ Abc_ObjIsComplement(pObj3) );
855 ePrev1 = Dec_GraphAddNodeAnd( pGraph, eNode2, eNode3 );
856 }
857 }
858 if ( fOrGate )
859 eRoot = Dec_GraphAddNodeOr( pGraph, ePrev0, ePrev1 );
860 else
861 eRoot = Dec_GraphAddNodeAnd( pGraph, ePrev0, ePrev1 );
862 Dec_GraphSetRoot( pGraph, eRoot );
863 if ( pRoot->fPhase )
864 Dec_GraphComplement( pGraph );
865 return pGraph;
866}
867
868
869
870
882void Abc_ManResubDivsS( Abc_ManRes_t * p, int Required )
883{
884 int fMoreDivs = 1; // bug fix by Siang-Yun Lee
885 Abc_Obj_t * pObj;
886 unsigned * puData, * puDataR;
887 int i, w;
888 Vec_PtrClear( p->vDivs1UP );
889 Vec_PtrClear( p->vDivs1UN );
890 Vec_PtrClear( p->vDivs1B );
891 puDataR = (unsigned *)p->pRoot->pData;
892 Vec_PtrForEachEntryStop( Abc_Obj_t *, p->vDivs, pObj, i, p->nDivs )
893 {
894 if ( (int)pObj->Level > Required - 1 )
895 continue;
896
897 puData = (unsigned *)pObj->pData;
898 // check positive containment
899 for ( w = 0; w < p->nWords; w++ )
900// if ( puData[w] & ~puDataR[w] )
901 if ( puData[w] & ~puDataR[w] & p->pCareSet[w] ) // care set
902 break;
903 if ( w == p->nWords )
904 {
905 Vec_PtrPush( p->vDivs1UP, pObj );
906 continue;
907 }
908 if ( fMoreDivs )
909 {
910 for ( w = 0; w < p->nWords; w++ )
911 // if ( ~puData[w] & ~puDataR[w] )
912 if ( ~puData[w] & ~puDataR[w] & p->pCareSet[w] ) // care set
913 break;
914 if ( w == p->nWords )
915 {
916 Vec_PtrPush( p->vDivs1UP, Abc_ObjNot(pObj) );
917 continue;
918 }
919 }
920 // check negative containment
921 for ( w = 0; w < p->nWords; w++ )
922// if ( ~puData[w] & puDataR[w] )
923 if ( ~puData[w] & puDataR[w] & p->pCareSet[w] ) // care set
924 break;
925 if ( w == p->nWords )
926 {
927 Vec_PtrPush( p->vDivs1UN, pObj );
928 continue;
929 }
930 if ( fMoreDivs )
931 {
932 for ( w = 0; w < p->nWords; w++ )
933 // if ( puData[w] & puDataR[w] )
934 if ( puData[w] & puDataR[w] & p->pCareSet[w] ) // care set
935 break;
936 if ( w == p->nWords )
937 {
938 Vec_PtrPush( p->vDivs1UN, Abc_ObjNot(pObj) );
939 continue;
940 }
941 }
942 // add the node to binates
943 Vec_PtrPush( p->vDivs1B, pObj );
944 }
945}
946
958void Abc_ManResubDivsD( Abc_ManRes_t * p, int Required )
959{
960 Abc_Obj_t * pObj0, * pObj1;
961 unsigned * puData0, * puData1, * puDataR;
962 int i, k, w;
963 Vec_PtrClear( p->vDivs2UP0 );
964 Vec_PtrClear( p->vDivs2UP1 );
965 Vec_PtrClear( p->vDivs2UN0 );
966 Vec_PtrClear( p->vDivs2UN1 );
967 puDataR = (unsigned *)p->pRoot->pData;
968 Vec_PtrForEachEntry( Abc_Obj_t *, p->vDivs1B, pObj0, i )
969 {
970 if ( (int)pObj0->Level > Required - 2 )
971 continue;
972
973 puData0 = (unsigned *)pObj0->pData;
974 Vec_PtrForEachEntryStart( Abc_Obj_t *, p->vDivs1B, pObj1, k, i + 1 )
975 {
976 if ( (int)pObj1->Level > Required - 2 )
977 continue;
978
979 puData1 = (unsigned *)pObj1->pData;
980
981 if ( Vec_PtrSize(p->vDivs2UP0) < ABC_RS_DIV2_MAX )
982 {
983 // get positive unate divisors
984 for ( w = 0; w < p->nWords; w++ )
985// if ( (puData0[w] & puData1[w]) & ~puDataR[w] )
986 if ( (puData0[w] & puData1[w]) & ~puDataR[w] & p->pCareSet[w] ) // care set
987 break;
988 if ( w == p->nWords )
989 {
990 Vec_PtrPush( p->vDivs2UP0, pObj0 );
991 Vec_PtrPush( p->vDivs2UP1, pObj1 );
992 }
993 for ( w = 0; w < p->nWords; w++ )
994// if ( (~puData0[w] & puData1[w]) & ~puDataR[w] )
995 if ( (~puData0[w] & puData1[w]) & ~puDataR[w] & p->pCareSet[w] ) // care set
996 break;
997 if ( w == p->nWords )
998 {
999 Vec_PtrPush( p->vDivs2UP0, Abc_ObjNot(pObj0) );
1000 Vec_PtrPush( p->vDivs2UP1, pObj1 );
1001 }
1002 for ( w = 0; w < p->nWords; w++ )
1003// if ( (puData0[w] & ~puData1[w]) & ~puDataR[w] )
1004 if ( (puData0[w] & ~puData1[w]) & ~puDataR[w] & p->pCareSet[w] ) // care set
1005 break;
1006 if ( w == p->nWords )
1007 {
1008 Vec_PtrPush( p->vDivs2UP0, pObj0 );
1009 Vec_PtrPush( p->vDivs2UP1, Abc_ObjNot(pObj1) );
1010 }
1011 for ( w = 0; w < p->nWords; w++ )
1012// if ( (puData0[w] | puData1[w]) & ~puDataR[w] )
1013 if ( (puData0[w] | puData1[w]) & ~puDataR[w] & p->pCareSet[w] ) // care set
1014 break;
1015 if ( w == p->nWords )
1016 {
1017 Vec_PtrPush( p->vDivs2UP0, Abc_ObjNot(pObj0) );
1018 Vec_PtrPush( p->vDivs2UP1, Abc_ObjNot(pObj1) );
1019 }
1020 }
1021
1022 if ( Vec_PtrSize(p->vDivs2UN0) < ABC_RS_DIV2_MAX )
1023 {
1024 // get negative unate divisors
1025 for ( w = 0; w < p->nWords; w++ )
1026// if ( ~(puData0[w] & puData1[w]) & puDataR[w] )
1027 if ( ~(puData0[w] & puData1[w]) & puDataR[w] & p->pCareSet[w] ) // care set
1028 break;
1029 if ( w == p->nWords )
1030 {
1031 Vec_PtrPush( p->vDivs2UN0, pObj0 );
1032 Vec_PtrPush( p->vDivs2UN1, pObj1 );
1033 }
1034 for ( w = 0; w < p->nWords; w++ )
1035// if ( ~(~puData0[w] & puData1[w]) & puDataR[w] )
1036 if ( ~(~puData0[w] & puData1[w]) & puDataR[w] & p->pCareSet[w] ) // care set
1037 break;
1038 if ( w == p->nWords )
1039 {
1040 Vec_PtrPush( p->vDivs2UN0, Abc_ObjNot(pObj0) );
1041 Vec_PtrPush( p->vDivs2UN1, pObj1 );
1042 }
1043 for ( w = 0; w < p->nWords; w++ )
1044// if ( ~(puData0[w] & ~puData1[w]) & puDataR[w] )
1045 if ( ~(puData0[w] & ~puData1[w]) & puDataR[w] & p->pCareSet[w] ) // care set
1046 break;
1047 if ( w == p->nWords )
1048 {
1049 Vec_PtrPush( p->vDivs2UN0, pObj0 );
1050 Vec_PtrPush( p->vDivs2UN1, Abc_ObjNot(pObj1) );
1051 }
1052 for ( w = 0; w < p->nWords; w++ )
1053// if ( ~(puData0[w] | puData1[w]) & puDataR[w] )
1054 if ( ~(puData0[w] | puData1[w]) & puDataR[w] & p->pCareSet[w] ) // care set
1055 break;
1056 if ( w == p->nWords )
1057 {
1058 Vec_PtrPush( p->vDivs2UN0, Abc_ObjNot(pObj0) );
1059 Vec_PtrPush( p->vDivs2UN1, Abc_ObjNot(pObj1) );
1060 }
1061 }
1062 }
1063 }
1064// printf( "%d %d ", Vec_PtrSize(p->vDivs2UP0), Vec_PtrSize(p->vDivs2UN0) );
1065}
1066
1067
1068
1080Dec_Graph_t * Abc_ManResubQuit( Abc_ManRes_t * p )
1081{
1082 Dec_Graph_t * pGraph;
1083 unsigned * upData;
1084 int w;
1085 upData = (unsigned *)p->pRoot->pData;
1086 for ( w = 0; w < p->nWords; w++ )
1087// if ( upData[w] )
1088 if ( upData[w] & p->pCareSet[w] ) // care set
1089 break;
1090 if ( w != p->nWords )
1091 return NULL;
1092 // get constant node graph
1093 if ( p->pRoot->fPhase )
1094 pGraph = Dec_GraphCreateConst1();
1095 else
1096 pGraph = Dec_GraphCreateConst0();
1097 return pGraph;
1098}
1099
1111Dec_Graph_t * Abc_ManResubDivs0( Abc_ManRes_t * p )
1112{
1113 Abc_Obj_t * pObj;
1114 unsigned * puData, * puDataR;
1115 int i, w;
1116 puDataR = (unsigned *)p->pRoot->pData;
1117 Vec_PtrForEachEntryStop( Abc_Obj_t *, p->vDivs, pObj, i, p->nDivs )
1118 {
1119 puData = (unsigned *)pObj->pData;
1120 for ( w = 0; w < p->nWords; w++ )
1121// if ( puData[w] != puDataR[w] )
1122 if ( (puData[w] ^ puDataR[w]) & p->pCareSet[w] ) // care set
1123 break;
1124 if ( w == p->nWords )
1125 return Abc_ManResubQuit0( p->pRoot, pObj );
1126 }
1127 return NULL;
1128}
1129
1141Dec_Graph_t * Abc_ManResubDivs1( Abc_ManRes_t * p, int Required )
1142{
1143 Abc_Obj_t * pObj0, * pObj1;
1144 unsigned * puData0, * puData1, * puDataR;
1145 int i, k, w;
1146 puDataR = (unsigned *)p->pRoot->pData;
1147 // check positive unate divisors
1148 Vec_PtrForEachEntry( Abc_Obj_t *, p->vDivs1UP, pObj0, i )
1149 {
1150 puData0 = (unsigned *)Abc_ObjRegular(pObj0)->pData;
1151 Vec_PtrForEachEntryStart( Abc_Obj_t *, p->vDivs1UP, pObj1, k, i + 1 )
1152 {
1153 puData1 = (unsigned *)Abc_ObjRegular(pObj1)->pData;
1154 if ( Abc_ObjIsComplement(pObj0) && Abc_ObjIsComplement(pObj1) )
1155 {
1156 for ( w = 0; w < p->nWords; w++ )
1157 // if ( (puData0[w] | puData1[w]) != puDataR[w] )
1158 if ( ((~puData0[w] | ~puData1[w]) ^ puDataR[w]) & p->pCareSet[w] ) // care set
1159 break;
1160 }
1161 else if ( Abc_ObjIsComplement(pObj0) )
1162 {
1163 for ( w = 0; w < p->nWords; w++ )
1164 // if ( (puData0[w] | puData1[w]) != puDataR[w] )
1165 if ( ((~puData0[w] | puData1[w]) ^ puDataR[w]) & p->pCareSet[w] ) // care set
1166 break;
1167 }
1168 else if ( Abc_ObjIsComplement(pObj1) )
1169 {
1170 for ( w = 0; w < p->nWords; w++ )
1171 // if ( (puData0[w] | puData1[w]) != puDataR[w] )
1172 if ( ((puData0[w] | ~puData1[w]) ^ puDataR[w]) & p->pCareSet[w] ) // care set
1173 break;
1174 }
1175 else
1176 {
1177 for ( w = 0; w < p->nWords; w++ )
1178 // if ( (puData0[w] | puData1[w]) != puDataR[w] )
1179 if ( ((puData0[w] | puData1[w]) ^ puDataR[w]) & p->pCareSet[w] ) // care set
1180 break;
1181 }
1182 if ( w == p->nWords )
1183 {
1184 p->nUsedNode1Or++;
1185 return Abc_ManResubQuit1( p->pRoot, pObj0, pObj1, 1 );
1186 }
1187 }
1188 }
1189 // check negative unate divisors
1190 Vec_PtrForEachEntry( Abc_Obj_t *, p->vDivs1UN, pObj0, i )
1191 {
1192 puData0 = (unsigned *)Abc_ObjRegular(pObj0)->pData;
1193 Vec_PtrForEachEntryStart( Abc_Obj_t *, p->vDivs1UN, pObj1, k, i + 1 )
1194 {
1195 puData1 = (unsigned *)Abc_ObjRegular(pObj1)->pData;
1196 if ( Abc_ObjIsComplement(pObj0) && Abc_ObjIsComplement(pObj1) )
1197 {
1198 for ( w = 0; w < p->nWords; w++ )
1199 // if ( (puData0[w] & puData1[w]) != puDataR[w] )
1200 if ( ((~puData0[w] & ~puData1[w]) ^ puDataR[w]) & p->pCareSet[w] ) // care set
1201 break;
1202 }
1203 if ( Abc_ObjIsComplement(pObj0) )
1204 {
1205 for ( w = 0; w < p->nWords; w++ )
1206 // if ( (puData0[w] & puData1[w]) != puDataR[w] )
1207 if ( ((~puData0[w] & puData1[w]) ^ puDataR[w]) & p->pCareSet[w] ) // care set
1208 break;
1209 }
1210 if ( Abc_ObjIsComplement(pObj1) )
1211 {
1212 for ( w = 0; w < p->nWords; w++ )
1213 // if ( (puData0[w] & puData1[w]) != puDataR[w] )
1214 if ( ((puData0[w] & ~puData1[w]) ^ puDataR[w]) & p->pCareSet[w] ) // care set
1215 break;
1216 }
1217 else
1218 {
1219 for ( w = 0; w < p->nWords; w++ )
1220 // if ( (puData0[w] & puData1[w]) != puDataR[w] )
1221 if ( ((puData0[w] & puData1[w]) ^ puDataR[w]) & p->pCareSet[w] ) // care set
1222 break;
1223 }
1224 if ( w == p->nWords )
1225 {
1226 p->nUsedNode1And++;
1227 return Abc_ManResubQuit1( p->pRoot, pObj0, pObj1, 0 );
1228 }
1229 }
1230 }
1231 return NULL;
1232}
1233
1245Dec_Graph_t * Abc_ManResubDivs12( Abc_ManRes_t * p, int Required )
1246{
1247 Abc_Obj_t * pObj0, * pObj1, * pObj2, * pObjMax, * pObjMin0 = NULL, * pObjMin1 = NULL;
1248 unsigned * puData0, * puData1, * puData2, * puDataR;
1249 int i, k, j, w, LevelMax;
1250 puDataR = (unsigned *)p->pRoot->pData;
1251 // check positive unate divisors
1252 Vec_PtrForEachEntry( Abc_Obj_t *, p->vDivs1UP, pObj0, i )
1253 {
1254 puData0 = (unsigned *)Abc_ObjRegular(pObj0)->pData;
1255 Vec_PtrForEachEntryStart( Abc_Obj_t *, p->vDivs1UP, pObj1, k, i + 1 )
1256 {
1257 puData1 = (unsigned *)Abc_ObjRegular(pObj1)->pData;
1258 Vec_PtrForEachEntryStart( Abc_Obj_t *, p->vDivs1UP, pObj2, j, k + 1 )
1259 {
1260 puData2 = (unsigned *)Abc_ObjRegular(pObj2)->pData;
1261 if ( Abc_ObjIsComplement(pObj0) && Abc_ObjIsComplement(pObj1) && Abc_ObjIsComplement(pObj2) )
1262 {
1263 for ( w = 0; w < p->nWords; w++ )
1264 // if ( (puData0[w] | puData1[w] | puData2[w]) != puDataR[w] )
1265 if ( ((~puData0[w] | ~puData1[w] | ~puData2[w]) ^ puDataR[w]) & p->pCareSet[w] ) // care set
1266 break;
1267 }
1268 else if ( Abc_ObjIsComplement(pObj0) && Abc_ObjIsComplement(pObj1) && !Abc_ObjIsComplement(pObj2) )
1269 {
1270 for ( w = 0; w < p->nWords; w++ )
1271 // if ( (puData0[w] | puData1[w] | puData2[w]) != puDataR[w] )
1272 if ( ((~puData0[w] | ~puData1[w] | puData2[w]) ^ puDataR[w]) & p->pCareSet[w] ) // care set
1273 break;
1274 }
1275 else if ( Abc_ObjIsComplement(pObj0) && !Abc_ObjIsComplement(pObj1) && Abc_ObjIsComplement(pObj2) )
1276 {
1277 for ( w = 0; w < p->nWords; w++ )
1278 // if ( (puData0[w] | puData1[w] | puData2[w]) != puDataR[w] )
1279 if ( ((~puData0[w] | puData1[w] | ~puData2[w]) ^ puDataR[w]) & p->pCareSet[w] ) // care set
1280 break;
1281 }
1282 else if ( Abc_ObjIsComplement(pObj0) && !Abc_ObjIsComplement(pObj1) && !Abc_ObjIsComplement(pObj2) )
1283 {
1284 for ( w = 0; w < p->nWords; w++ )
1285 // if ( (puData0[w] | puData1[w] | puData2[w]) != puDataR[w] )
1286 if ( ((~puData0[w] | puData1[w] | puData2[w]) ^ puDataR[w]) & p->pCareSet[w] ) // care set
1287 break;
1288 }
1289 else if ( !Abc_ObjIsComplement(pObj0) && Abc_ObjIsComplement(pObj1) && Abc_ObjIsComplement(pObj2) )
1290 {
1291 for ( w = 0; w < p->nWords; w++ )
1292 // if ( (puData0[w] | puData1[w] | puData2[w]) != puDataR[w] )
1293 if ( ((puData0[w] | ~puData1[w] | ~puData2[w]) ^ puDataR[w]) & p->pCareSet[w] ) // care set
1294 break;
1295 }
1296 else if ( !Abc_ObjIsComplement(pObj0) && Abc_ObjIsComplement(pObj1) && !Abc_ObjIsComplement(pObj2) )
1297 {
1298 for ( w = 0; w < p->nWords; w++ )
1299 // if ( (puData0[w] | puData1[w] | puData2[w]) != puDataR[w] )
1300 if ( ((puData0[w] | ~puData1[w] | puData2[w]) ^ puDataR[w]) & p->pCareSet[w] ) // care set
1301 break;
1302 }
1303 else if ( !Abc_ObjIsComplement(pObj0) && !Abc_ObjIsComplement(pObj1) && Abc_ObjIsComplement(pObj2) )
1304 {
1305 for ( w = 0; w < p->nWords; w++ )
1306 // if ( (puData0[w] | puData1[w] | puData2[w]) != puDataR[w] )
1307 if ( ((puData0[w] | puData1[w] | ~puData2[w]) ^ puDataR[w]) & p->pCareSet[w] ) // care set
1308 break;
1309 }
1310 else if ( !Abc_ObjIsComplement(pObj0) && !Abc_ObjIsComplement(pObj1) && !Abc_ObjIsComplement(pObj2) )
1311 {
1312 for ( w = 0; w < p->nWords; w++ )
1313 // if ( (puData0[w] | puData1[w] | puData2[w]) != puDataR[w] )
1314 if ( ((puData0[w] | puData1[w] | puData2[w]) ^ puDataR[w]) & p->pCareSet[w] ) // care set
1315 break;
1316 }
1317 else assert( 0 );
1318 if ( w == p->nWords )
1319 {
1320 LevelMax = Abc_MaxInt( Abc_ObjRegular(pObj0)->Level, Abc_MaxInt(Abc_ObjRegular(pObj1)->Level, Abc_ObjRegular(pObj2)->Level) );
1321 assert( LevelMax <= Required - 1 );
1322
1323 pObjMax = NULL;
1324 if ( (int)Abc_ObjRegular(pObj0)->Level == LevelMax )
1325 pObjMax = pObj0, pObjMin0 = pObj1, pObjMin1 = pObj2;
1326 if ( (int)Abc_ObjRegular(pObj1)->Level == LevelMax )
1327 {
1328 if ( pObjMax ) continue;
1329 pObjMax = pObj1, pObjMin0 = pObj0, pObjMin1 = pObj2;
1330 }
1331 if ( (int)Abc_ObjRegular(pObj2)->Level == LevelMax )
1332 {
1333 if ( pObjMax ) continue;
1334 pObjMax = pObj2, pObjMin0 = pObj0, pObjMin1 = pObj1;
1335 }
1336
1337 p->nUsedNode2Or++;
1338 assert(pObjMin0);
1339 assert(pObjMin1);
1340 return Abc_ManResubQuit21( p->pRoot, pObjMin0, pObjMin1, pObjMax, 1 );
1341 }
1342 }
1343 }
1344 }
1345 // check negative unate divisors
1346 Vec_PtrForEachEntry( Abc_Obj_t *, p->vDivs1UN, pObj0, i )
1347 {
1348 puData0 = (unsigned *)Abc_ObjRegular(pObj0)->pData;
1349 Vec_PtrForEachEntryStart( Abc_Obj_t *, p->vDivs1UN, pObj1, k, i + 1 )
1350 {
1351 puData1 = (unsigned *)Abc_ObjRegular(pObj1)->pData;
1352 Vec_PtrForEachEntryStart( Abc_Obj_t *, p->vDivs1UN, pObj2, j, k + 1 )
1353 {
1354 puData2 = (unsigned *)Abc_ObjRegular(pObj2)->pData;
1355 if ( Abc_ObjIsComplement(pObj0) && Abc_ObjIsComplement(pObj1) && Abc_ObjIsComplement(pObj2) )
1356 {
1357 for ( w = 0; w < p->nWords; w++ )
1358 // if ( (puData0[w] & puData1[w] & puData2[w]) != puDataR[w] )
1359 if ( ((~puData0[w] & ~puData1[w] & ~puData2[w]) ^ puDataR[w]) & p->pCareSet[w] ) // care set
1360 break;
1361 }
1362 else if ( Abc_ObjIsComplement(pObj0) && Abc_ObjIsComplement(pObj1) && !Abc_ObjIsComplement(pObj2) )
1363 {
1364 for ( w = 0; w < p->nWords; w++ )
1365 // if ( (puData0[w] & puData1[w] & puData2[w]) != puDataR[w] )
1366 if ( ((~puData0[w] & ~puData1[w] & puData2[w]) ^ puDataR[w]) & p->pCareSet[w] ) // care set
1367 break;
1368 }
1369 else if ( Abc_ObjIsComplement(pObj0) && !Abc_ObjIsComplement(pObj1) && Abc_ObjIsComplement(pObj2) )
1370 {
1371 for ( w = 0; w < p->nWords; w++ )
1372 // if ( (puData0[w] & puData1[w] & puData2[w]) != puDataR[w] )
1373 if ( ((~puData0[w] & puData1[w] & ~puData2[w]) ^ puDataR[w]) & p->pCareSet[w] ) // care set
1374 break;
1375 }
1376 else if ( Abc_ObjIsComplement(pObj0) && !Abc_ObjIsComplement(pObj1) && !Abc_ObjIsComplement(pObj2) )
1377 {
1378 for ( w = 0; w < p->nWords; w++ )
1379 // if ( (puData0[w] & puData1[w] & puData2[w]) != puDataR[w] )
1380 if ( ((~puData0[w] & puData1[w] & puData2[w]) ^ puDataR[w]) & p->pCareSet[w] ) // care set
1381 break;
1382 }
1383 else if ( !Abc_ObjIsComplement(pObj0) && Abc_ObjIsComplement(pObj1) && Abc_ObjIsComplement(pObj2) )
1384 {
1385 for ( w = 0; w < p->nWords; w++ )
1386 // if ( (puData0[w] & puData1[w] & puData2[w]) != puDataR[w] )
1387 if ( ((puData0[w] & ~puData1[w] & ~puData2[w]) ^ puDataR[w]) & p->pCareSet[w] ) // care set
1388 break;
1389 }
1390 else if ( !Abc_ObjIsComplement(pObj0) && Abc_ObjIsComplement(pObj1) && !Abc_ObjIsComplement(pObj2) )
1391 {
1392 for ( w = 0; w < p->nWords; w++ )
1393 // if ( (puData0[w] & puData1[w] & puData2[w]) != puDataR[w] )
1394 if ( ((puData0[w] & ~puData1[w] & puData2[w]) ^ puDataR[w]) & p->pCareSet[w] ) // care set
1395 break;
1396 }
1397 else if ( !Abc_ObjIsComplement(pObj0) && !Abc_ObjIsComplement(pObj1) && Abc_ObjIsComplement(pObj2) )
1398 {
1399 for ( w = 0; w < p->nWords; w++ )
1400 // if ( (puData0[w] & puData1[w] & puData2[w]) != puDataR[w] )
1401 if ( ((puData0[w] & puData1[w] & ~puData2[w]) ^ puDataR[w]) & p->pCareSet[w] ) // care set
1402 break;
1403 }
1404 else if ( !Abc_ObjIsComplement(pObj0) && !Abc_ObjIsComplement(pObj1) && !Abc_ObjIsComplement(pObj2) )
1405 {
1406 for ( w = 0; w < p->nWords; w++ )
1407 // if ( (puData0[w] & puData1[w] & puData2[w]) != puDataR[w] )
1408 if ( ((puData0[w] & puData1[w] & puData2[w]) ^ puDataR[w]) & p->pCareSet[w] ) // care set
1409 break;
1410 }
1411 else assert( 0 );
1412 if ( w == p->nWords )
1413 {
1414 LevelMax = Abc_MaxInt( Abc_ObjRegular(pObj0)->Level, Abc_MaxInt(Abc_ObjRegular(pObj1)->Level, Abc_ObjRegular(pObj2)->Level) );
1415 assert( LevelMax <= Required - 1 );
1416
1417 pObjMax = NULL;
1418 if ( (int)Abc_ObjRegular(pObj0)->Level == LevelMax )
1419 pObjMax = pObj0, pObjMin0 = pObj1, pObjMin1 = pObj2;
1420 if ( (int)Abc_ObjRegular(pObj1)->Level == LevelMax )
1421 {
1422 if ( pObjMax ) continue;
1423 pObjMax = pObj1, pObjMin0 = pObj0, pObjMin1 = pObj2;
1424 }
1425 if ( (int)Abc_ObjRegular(pObj2)->Level == LevelMax )
1426 {
1427 if ( pObjMax ) continue;
1428 pObjMax = pObj2, pObjMin0 = pObj0, pObjMin1 = pObj1;
1429 }
1430
1431 p->nUsedNode2And++;
1432 assert(pObjMin0);
1433 assert(pObjMin1);
1434 return Abc_ManResubQuit21( p->pRoot, pObjMin0, pObjMin1, pObjMax, 0 );
1435 }
1436 }
1437 }
1438 }
1439 return NULL;
1440}
1441
1453Dec_Graph_t * Abc_ManResubDivs2( Abc_ManRes_t * p, int Required )
1454{
1455 Abc_Obj_t * pObj0, * pObj1, * pObj2;
1456 unsigned * puData0, * puData1, * puData2, * puDataR;
1457 int i, k, w;
1458 puDataR = (unsigned *)p->pRoot->pData;
1459 // check positive unate divisors
1460 Vec_PtrForEachEntry( Abc_Obj_t *, p->vDivs1UP, pObj0, i )
1461 {
1462 puData0 = (unsigned *)Abc_ObjRegular(pObj0)->pData;
1463 Vec_PtrForEachEntry( Abc_Obj_t *, p->vDivs2UP0, pObj1, k )
1464 {
1465 pObj2 = (Abc_Obj_t *)Vec_PtrEntry( p->vDivs2UP1, k );
1466
1467 puData1 = (unsigned *)Abc_ObjRegular(pObj1)->pData;
1468 puData2 = (unsigned *)Abc_ObjRegular(pObj2)->pData;
1469 if ( Abc_ObjIsComplement(pObj0) )
1470 {
1471 if ( Abc_ObjIsComplement(pObj1) && Abc_ObjIsComplement(pObj2) )
1472 {
1473 for ( w = 0; w < p->nWords; w++ )
1474 // if ( (puData0[w] | (puData1[w] | puData2[w])) != puDataR[w] )
1475 if ( ((~puData0[w] | (puData1[w] | puData2[w])) ^ puDataR[w]) & p->pCareSet[w] ) // care set
1476 break;
1477 }
1478 else if ( Abc_ObjIsComplement(pObj1) )
1479 {
1480 for ( w = 0; w < p->nWords; w++ )
1481 // if ( (puData0[w] | (~puData1[w] & puData2[w])) != puDataR[w] )
1482 if ( ((~puData0[w] | (~puData1[w] & puData2[w])) ^ puDataR[w]) & p->pCareSet[w] ) // care set
1483 break;
1484 }
1485 else if ( Abc_ObjIsComplement(pObj2) )
1486 {
1487 for ( w = 0; w < p->nWords; w++ )
1488 // if ( (puData0[w] | (puData1[w] & ~puData2[w])) != puDataR[w] )
1489 if ( ((~puData0[w] | (puData1[w] & ~puData2[w])) ^ puDataR[w]) & p->pCareSet[w] ) // care set
1490 break;
1491 }
1492 else
1493 {
1494 for ( w = 0; w < p->nWords; w++ )
1495 // if ( (puData0[w] | (puData1[w] & puData2[w])) != puDataR[w] )
1496 if ( ((~puData0[w] | (puData1[w] & puData2[w])) ^ puDataR[w]) & p->pCareSet[w] ) // care set
1497 break;
1498 }
1499 }
1500 else
1501 {
1502 if ( Abc_ObjIsComplement(pObj1) && Abc_ObjIsComplement(pObj2) )
1503 {
1504 for ( w = 0; w < p->nWords; w++ )
1505 // if ( (puData0[w] | (puData1[w] | puData2[w])) != puDataR[w] )
1506 if ( ((puData0[w] | (puData1[w] | puData2[w])) ^ puDataR[w]) & p->pCareSet[w] ) // care set
1507 break;
1508 }
1509 else if ( Abc_ObjIsComplement(pObj1) )
1510 {
1511 for ( w = 0; w < p->nWords; w++ )
1512 // if ( (puData0[w] | (~puData1[w] & puData2[w])) != puDataR[w] )
1513 if ( ((puData0[w] | (~puData1[w] & puData2[w])) ^ puDataR[w]) & p->pCareSet[w] ) // care set
1514 break;
1515 }
1516 else if ( Abc_ObjIsComplement(pObj2) )
1517 {
1518 for ( w = 0; w < p->nWords; w++ )
1519 // if ( (puData0[w] | (puData1[w] & ~puData2[w])) != puDataR[w] )
1520 if ( ((puData0[w] | (puData1[w] & ~puData2[w])) ^ puDataR[w]) & p->pCareSet[w] ) // care set
1521 break;
1522 }
1523 else
1524 {
1525 for ( w = 0; w < p->nWords; w++ )
1526 // if ( (puData0[w] | (puData1[w] & puData2[w])) != puDataR[w] )
1527 if ( ((puData0[w] | (puData1[w] & puData2[w])) ^ puDataR[w]) & p->pCareSet[w] ) // care set
1528 break;
1529 }
1530 }
1531 if ( w == p->nWords )
1532 {
1533 p->nUsedNode2OrAnd++;
1534 return Abc_ManResubQuit2( p->pRoot, pObj0, pObj1, pObj2, 1 );
1535 }
1536 }
1537 }
1538 // check negative unate divisors
1539 Vec_PtrForEachEntry( Abc_Obj_t *, p->vDivs1UN, pObj0, i )
1540 {
1541 puData0 = (unsigned *)Abc_ObjRegular(pObj0)->pData;
1542 Vec_PtrForEachEntry( Abc_Obj_t *, p->vDivs2UN0, pObj1, k )
1543 {
1544 pObj2 = (Abc_Obj_t *)Vec_PtrEntry( p->vDivs2UN1, k );
1545
1546 puData1 = (unsigned *)Abc_ObjRegular(pObj1)->pData;
1547 puData2 = (unsigned *)Abc_ObjRegular(pObj2)->pData;
1548 if ( Abc_ObjIsComplement(pObj0) )
1549 {
1550 if ( Abc_ObjIsComplement(pObj1) && Abc_ObjIsComplement(pObj2) )
1551 {
1552 for ( w = 0; w < p->nWords; w++ )
1553 // if ( (puData0[w] & (puData1[w] | puData2[w])) != puDataR[w] )
1554 if ( ((~puData0[w] & (puData1[w] | puData2[w])) ^ puDataR[w]) & p->pCareSet[w] ) // care set
1555 break;
1556 }
1557 else if ( Abc_ObjIsComplement(pObj1) )
1558 {
1559 for ( w = 0; w < p->nWords; w++ )
1560 // if ( (puData0[w] & (~puData1[w] & puData2[w])) != puDataR[w] )
1561 if ( ((~puData0[w] & (~puData1[w] & puData2[w])) ^ puDataR[w]) & p->pCareSet[w] ) // care set
1562 break;
1563 }
1564 else if ( Abc_ObjIsComplement(pObj2) )
1565 {
1566 for ( w = 0; w < p->nWords; w++ )
1567 // if ( (puData0[w] & (puData1[w] & ~puData2[w])) != puDataR[w] )
1568 if ( ((~puData0[w] & (puData1[w] & ~puData2[w])) ^ puDataR[w]) & p->pCareSet[w] ) // care set
1569 break;
1570 }
1571 else
1572 {
1573 for ( w = 0; w < p->nWords; w++ )
1574 // if ( (puData0[w] & (puData1[w] & puData2[w])) != puDataR[w] )
1575 if ( ((~puData0[w] & (puData1[w] & puData2[w])) ^ puDataR[w]) & p->pCareSet[w] ) // care set
1576 break;
1577 }
1578 }
1579 else
1580 {
1581 if ( Abc_ObjIsComplement(pObj1) && Abc_ObjIsComplement(pObj2) )
1582 {
1583 for ( w = 0; w < p->nWords; w++ )
1584 // if ( (puData0[w] & (puData1[w] | puData2[w])) != puDataR[w] )
1585 if ( ((puData0[w] & (puData1[w] | puData2[w])) ^ puDataR[w]) & p->pCareSet[w] ) // care set
1586 break;
1587 }
1588 else if ( Abc_ObjIsComplement(pObj1) )
1589 {
1590 for ( w = 0; w < p->nWords; w++ )
1591 // if ( (puData0[w] & (~puData1[w] & puData2[w])) != puDataR[w] )
1592 if ( ((puData0[w] & (~puData1[w] & puData2[w])) ^ puDataR[w]) & p->pCareSet[w] ) // care set
1593 break;
1594 }
1595 else if ( Abc_ObjIsComplement(pObj2) )
1596 {
1597 for ( w = 0; w < p->nWords; w++ )
1598 // if ( (puData0[w] & (puData1[w] & ~puData2[w])) != puDataR[w] )
1599 if ( ((puData0[w] & (puData1[w] & ~puData2[w])) ^ puDataR[w]) & p->pCareSet[w] ) // care set
1600 break;
1601 }
1602 else
1603 {
1604 for ( w = 0; w < p->nWords; w++ )
1605 // if ( (puData0[w] & (puData1[w] & puData2[w])) != puDataR[w] )
1606 if ( ((puData0[w] & (puData1[w] & puData2[w])) ^ puDataR[w]) & p->pCareSet[w] ) // care set
1607 break;
1608 }
1609 }
1610 if ( w == p->nWords )
1611 {
1612 p->nUsedNode2AndOr++;
1613 return Abc_ManResubQuit2( p->pRoot, pObj0, pObj1, pObj2, 0 );
1614 }
1615 }
1616 }
1617 return NULL;
1618}
1619
1631Dec_Graph_t * Abc_ManResubDivs3( Abc_ManRes_t * p, int Required )
1632{
1633 Abc_Obj_t * pObj0, * pObj1, * pObj2, * pObj3;
1634 unsigned * puData0, * puData1, * puData2, * puData3, * puDataR;
1635 int i, k, w = 0, Flag;
1636 puDataR = (unsigned *)p->pRoot->pData;
1637 // check positive unate divisors
1638 Vec_PtrForEachEntry( Abc_Obj_t *, p->vDivs2UP0, pObj0, i )
1639 {
1640 pObj1 = (Abc_Obj_t *)Vec_PtrEntry( p->vDivs2UP1, i );
1641 puData0 = (unsigned *)Abc_ObjRegular(pObj0)->pData;
1642 puData1 = (unsigned *)Abc_ObjRegular(pObj1)->pData;
1643 Flag = (Abc_ObjIsComplement(pObj0) << 3) | (Abc_ObjIsComplement(pObj1) << 2);
1644
1645 Vec_PtrForEachEntryStart( Abc_Obj_t *, p->vDivs2UP0, pObj2, k, i + 1 )
1646 {
1647 pObj3 = (Abc_Obj_t *)Vec_PtrEntry( p->vDivs2UP1, k );
1648 puData2 = (unsigned *)Abc_ObjRegular(pObj2)->pData;
1649 puData3 = (unsigned *)Abc_ObjRegular(pObj3)->pData;
1650
1651 Flag = (Flag & 12) | ((int)Abc_ObjIsComplement(pObj2) << 1) | (int)Abc_ObjIsComplement(pObj3);
1652 assert( Flag < 16 );
1653 switch( Flag )
1654 {
1655 case 0: // 0000
1656 for ( w = 0; w < p->nWords; w++ )
1657// if ( ((puData0[w] & puData1[w]) | (puData2[w] & puData3[w])) != puDataR[w] )
1658 if ( (((puData0[w] & puData1[w]) | (puData2[w] & puData3[w])) ^ puDataR[w]) & p->pCareSet[w] ) // care set
1659 break;
1660 break;
1661 case 1: // 0001
1662 for ( w = 0; w < p->nWords; w++ )
1663// if ( ((puData0[w] & puData1[w]) | (puData2[w] & ~puData3[w])) != puDataR[w] )
1664 if ( (((puData0[w] & puData1[w]) | (puData2[w] & ~puData3[w])) ^ puDataR[w]) & p->pCareSet[w] ) // care set
1665 break;
1666 break;
1667 case 2: // 0010
1668 for ( w = 0; w < p->nWords; w++ )
1669// if ( ((puData0[w] & puData1[w]) | (~puData2[w] & puData3[w])) != puDataR[w] )
1670 if ( (((puData0[w] & puData1[w]) | (~puData2[w] & puData3[w])) ^ puDataR[w]) & p->pCareSet[w] ) // care set
1671 break;
1672 break;
1673 case 3: // 0011
1674 for ( w = 0; w < p->nWords; w++ )
1675// if ( ((puData0[w] & puData1[w]) | (puData2[w] | puData3[w])) != puDataR[w] )
1676 if ( (((puData0[w] & puData1[w]) | (puData2[w] | puData3[w])) ^ puDataR[w]) & p->pCareSet[w] ) // care set
1677 break;
1678 break;
1679
1680 case 4: // 0100
1681 for ( w = 0; w < p->nWords; w++ )
1682// if ( ((puData0[w] & ~puData1[w]) | (puData2[w] & puData3[w])) != puDataR[w] )
1683 if ( (((puData0[w] & ~puData1[w]) | (puData2[w] & puData3[w])) ^ puDataR[w]) & p->pCareSet[w] ) // care set
1684 break;
1685 break;
1686 case 5: // 0101
1687 for ( w = 0; w < p->nWords; w++ )
1688// if ( ((puData0[w] & ~puData1[w]) | (puData2[w] & ~puData3[w])) != puDataR[w] )
1689 if ( (((puData0[w] & ~puData1[w]) | (puData2[w] & ~puData3[w])) ^ puDataR[w]) & p->pCareSet[w] ) // care set
1690 break;
1691 break;
1692 case 6: // 0110
1693 for ( w = 0; w < p->nWords; w++ )
1694// if ( ((puData0[w] & ~puData1[w]) | (~puData2[w] & puData3[w])) != puDataR[w] )
1695 if ( (((puData0[w] & ~puData1[w]) | (~puData2[w] & puData3[w])) ^ puDataR[w]) & p->pCareSet[w] ) // care set
1696 break;
1697 break;
1698 case 7: // 0111
1699 for ( w = 0; w < p->nWords; w++ )
1700// if ( ((puData0[w] & ~puData1[w]) | (puData2[w] | puData3[w])) != puDataR[w] )
1701 if ( (((puData0[w] & ~puData1[w]) | (puData2[w] | puData3[w])) ^ puDataR[w]) & p->pCareSet[w] ) // care set
1702 break;
1703 break;
1704
1705 case 8: // 1000
1706 for ( w = 0; w < p->nWords; w++ )
1707// if ( ((~puData0[w] & puData1[w]) | (puData2[w] & puData3[w])) != puDataR[w] )
1708 if ( (((~puData0[w] & puData1[w]) | (puData2[w] & puData3[w])) ^ puDataR[w]) & p->pCareSet[w] ) // care set
1709 break;
1710 break;
1711 case 9: // 1001
1712 for ( w = 0; w < p->nWords; w++ )
1713// if ( ((~puData0[w] & puData1[w]) | (puData2[w] & ~puData3[w])) != puDataR[w] )
1714 if ( (((~puData0[w] & puData1[w]) | (puData2[w] & ~puData3[w])) ^ puDataR[w]) & p->pCareSet[w] ) // care set
1715 break;
1716 break;
1717 case 10: // 1010
1718 for ( w = 0; w < p->nWords; w++ )
1719// if ( ((~puData0[w] & puData1[w]) | (~puData2[w] & puData3[w])) != puDataR[w] )
1720 if ( (((~puData0[w] & puData1[w]) | (~puData2[w] & puData3[w])) ^ puDataR[w]) & p->pCareSet[w] ) // care set
1721 break;
1722 break;
1723 case 11: // 1011
1724 for ( w = 0; w < p->nWords; w++ )
1725// if ( ((~puData0[w] & puData1[w]) | (puData2[w] | puData3[w])) != puDataR[w] )
1726 if ( (((~puData0[w] & puData1[w]) | (puData2[w] | puData3[w])) ^ puDataR[w]) & p->pCareSet[w] ) // care set
1727 break;
1728 break;
1729
1730 case 12: // 1100
1731 for ( w = 0; w < p->nWords; w++ )
1732// if ( ((puData0[w] | puData1[w]) | (puData2[w] & puData3[w])) != puDataR[w] )
1733 if ( (((puData0[w] | puData1[w]) | (puData2[w] & puData3[w])) ^ puDataR[w]) & p->pCareSet[w] ) // care set
1734 break;
1735 break;
1736 case 13: // 1101
1737 for ( w = 0; w < p->nWords; w++ )
1738// if ( ((puData0[w] | puData1[w]) | (puData2[w] & ~puData3[w])) != puDataR[w] )
1739 if ( (((puData0[w] | puData1[w]) | (puData2[w] & ~puData3[w])) ^ puDataR[w]) & p->pCareSet[w] )
1740 break;
1741 break;
1742 case 14: // 1110
1743 for ( w = 0; w < p->nWords; w++ )
1744// if ( ((puData0[w] | puData1[w]) | (~puData2[w] & puData3[w])) != puDataR[w] )
1745 if ( (((puData0[w] | puData1[w]) | (~puData2[w] & puData3[w])) ^ puDataR[w]) & p->pCareSet[w] )
1746 break;
1747 break;
1748 case 15: // 1111
1749 for ( w = 0; w < p->nWords; w++ )
1750// if ( ((puData0[w] | puData1[w]) | (puData2[w] | puData3[w])) != puDataR[w] )
1751 if ( (((puData0[w] | puData1[w]) | (puData2[w] | puData3[w])) ^ puDataR[w]) & p->pCareSet[w] )
1752 break;
1753 break;
1754
1755 }
1756 if ( w == p->nWords )
1757 {
1758 p->nUsedNode3OrAnd++;
1759 return Abc_ManResubQuit3( p->pRoot, pObj0, pObj1, pObj2, pObj3, 1 );
1760 }
1761 }
1762 }
1763
1764/*
1765 // check negative unate divisors
1766 Vec_PtrForEachEntry( Abc_Obj_t *, p->vDivs2UN0, pObj0, i )
1767 {
1768 pObj1 = Vec_PtrEntry( p->vDivs2UN1, i );
1769 puData0 = Abc_ObjRegular(pObj0)->pData;
1770 puData1 = Abc_ObjRegular(pObj1)->pData;
1771 Flag = (Abc_ObjIsComplement(pObj0) << 3) | (Abc_ObjIsComplement(pObj1) << 2);
1772
1773 Vec_PtrForEachEntryStart( Abc_Obj_t *, p->vDivs2UN0, pObj2, k, i + 1 )
1774 {
1775 pObj3 = Vec_PtrEntry( p->vDivs2UN1, k );
1776 puData2 = Abc_ObjRegular(pObj2)->pData;
1777 puData3 = Abc_ObjRegular(pObj3)->pData;
1778
1779 Flag = (Flag & 12) | (Abc_ObjIsComplement(pObj2) << 1) | Abc_ObjIsComplement(pObj3);
1780 assert( Flag < 16 );
1781 switch( Flag )
1782 {
1783 case 0: // 0000
1784 for ( w = 0; w < p->nWords; w++ )
1785 if ( (((puData0[w] & puData1[w]) & (puData2[w] & puData3[w])) ^ puDataR[w]) & p->pCareSet[w] )
1786 break;
1787 break;
1788 case 1: // 0001
1789 for ( w = 0; w < p->nWords; w++ )
1790 if ( (((puData0[w] & puData1[w]) & (puData2[w] & ~puData3[w])) ^ puDataR[w]) & p->pCareSet[w] )
1791 break;
1792 break;
1793 case 2: // 0010
1794 for ( w = 0; w < p->nWords; w++ )
1795 if ( (((puData0[w] & puData1[w]) & (~puData2[w] & puData3[w])) ^ puDataR[w]) & p->pCareSet[w] )
1796 break;
1797 break;
1798 case 3: // 0011
1799 for ( w = 0; w < p->nWords; w++ )
1800 if ( (((puData0[w] & puData1[w]) & (puData2[w] | puData3[w])) ^ puDataR[w]) & p->pCareSet[w] )
1801 break;
1802 break;
1803
1804 case 4: // 0100
1805 for ( w = 0; w < p->nWords; w++ )
1806 if ( (((puData0[w] & ~puData1[w]) & (puData2[w] & puData3[w])) ^ puDataR[w]) & p->pCareSet[w] )
1807 break;
1808 break;
1809 case 5: // 0101
1810 for ( w = 0; w < p->nWords; w++ )
1811 if ( (((puData0[w] & ~puData1[w]) & (puData2[w] & ~puData3[w])) ^ puDataR[w]) & p->pCareSet[w] )
1812 break;
1813 break;
1814 case 6: // 0110
1815 for ( w = 0; w < p->nWords; w++ )
1816 if ( (((puData0[w] & ~puData1[w]) & (~puData2[w] & puData3[w])) ^ puDataR[w]) & p->pCareSet[w] )
1817 break;
1818 break;
1819 case 7: // 0111
1820 for ( w = 0; w < p->nWords; w++ )
1821 if ( (((puData0[w] & ~puData1[w]) & (puData2[w] | puData3[w])) ^ puDataR[w]) & p->pCareSet[w] )
1822 break;
1823 break;
1824
1825 case 8: // 1000
1826 for ( w = 0; w < p->nWords; w++ )
1827 if ( (((~puData0[w] & puData1[w]) & (puData2[w] & puData3[w])) ^ puDataR[w]) & p->pCareSet[w] )
1828 break;
1829 break;
1830 case 9: // 1001
1831 for ( w = 0; w < p->nWords; w++ )
1832 if ( (((~puData0[w] & puData1[w]) & (puData2[w] & ~puData3[w])) ^ puDataR[w]) & p->pCareSet[w] )
1833 break;
1834 break;
1835 case 10: // 1010
1836 for ( w = 0; w < p->nWords; w++ )
1837 if ( (((~puData0[w] & puData1[w]) & (~puData2[w] & puData3[w])) ^ puDataR[w]) & p->pCareSet[w] )
1838 break;
1839 break;
1840 case 11: // 1011
1841 for ( w = 0; w < p->nWords; w++ )
1842 if ( (((~puData0[w] & puData1[w]) & (puData2[w] | puData3[w])) ^ puDataR[w]) & p->pCareSet[w] )
1843 break;
1844 break;
1845
1846 case 12: // 1100
1847 for ( w = 0; w < p->nWords; w++ )
1848 if ( (((puData0[w] | puData1[w]) & (puData2[w] & puData3[w])) ^ puDataR[w]) & p->pCareSet[w] )
1849 break;
1850 break;
1851 case 13: // 1101
1852 for ( w = 0; w < p->nWords; w++ )
1853 if ( (((puData0[w] | puData1[w]) & (puData2[w] & ~puData3[w])) ^ puDataR[w]) & p->pCareSet[w] )
1854 break;
1855 break;
1856 case 14: // 1110
1857 for ( w = 0; w < p->nWords; w++ )
1858 if ( (((puData0[w] | puData1[w]) & (~puData2[w] & puData3[w])) ^ puDataR[w]) & p->pCareSet[w] )
1859 break;
1860 break;
1861 case 15: // 1111
1862 for ( w = 0; w < p->nWords; w++ )
1863 if ( (((puData0[w] | puData1[w]) & (puData2[w] | puData3[w])) ^ puDataR[w]) & p->pCareSet[w] )
1864 break;
1865 break;
1866
1867 }
1868 if ( w == p->nWords )
1869 {
1870 p->nUsedNode3AndOr++;
1871 return Abc_ManResubQuit3( p->pRoot, pObj0, pObj1, pObj2, pObj3, 0 );
1872 }
1873 }
1874 }
1875*/
1876 return NULL;
1877}
1878
1890void Abc_ManResubCleanup( Abc_ManRes_t * p )
1891{
1892 Abc_Obj_t * pObj;
1893 int i;
1894 Vec_PtrForEachEntry( Abc_Obj_t *, p->vDivs, pObj, i )
1895 pObj->pData = NULL;
1896 Vec_PtrClear( p->vDivs );
1897 p->pRoot = NULL;
1898}
1899
1911Dec_Graph_t * Abc_ManResubEval( Abc_ManRes_t * p, Abc_Obj_t * pRoot, Vec_Ptr_t * vLeaves, int nSteps, int fUpdateLevel, int fVerbose )
1912{
1913 extern int Abc_NodeMffcInside( Abc_Obj_t * pNode, Vec_Ptr_t * vLeaves, Vec_Ptr_t * vInside );
1914 Dec_Graph_t * pGraph;
1915 int Required;
1916 abctime clk;
1917
1918 Required = fUpdateLevel? Abc_ObjRequiredLevel(pRoot) : ABC_INFINITY;
1919
1920 assert( nSteps >= 0 );
1921 assert( nSteps <= 3 );
1922 p->pRoot = pRoot;
1923 p->nLeaves = Vec_PtrSize(vLeaves);
1924 p->nLastGain = -1;
1925
1926 // collect the MFFC
1927clk = Abc_Clock();
1928 p->nMffc = Abc_NodeMffcInside( pRoot, vLeaves, p->vTemp );
1929p->timeMffc += Abc_Clock() - clk;
1930 assert( p->nMffc > 0 );
1931
1932 // collect the divisor nodes
1933clk = Abc_Clock();
1934 if ( !Abc_ManResubCollectDivs( p, pRoot, vLeaves, Required ) )
1935 return NULL;
1936 p->timeDiv += Abc_Clock() - clk;
1937
1938 p->nTotalDivs += p->nDivs;
1939 p->nTotalLeaves += p->nLeaves;
1940
1941 // simulate the nodes
1942clk = Abc_Clock();
1943 Abc_ManResubSimulate( p->vDivs, p->nLeaves, p->vSims, p->nLeavesMax, p->nWords );
1944p->timeSim += Abc_Clock() - clk;
1945
1946clk = Abc_Clock();
1947 // consider constants
1948 if ( (pGraph = Abc_ManResubQuit( p )) )
1949 {
1950 p->nUsedNodeC++;
1951 p->nLastGain = p->nMffc;
1952 return pGraph;
1953 }
1954
1955 // consider equal nodes
1956 if ( (pGraph = Abc_ManResubDivs0( p )) )
1957 {
1958p->timeRes1 += Abc_Clock() - clk;
1959 p->nUsedNode0++;
1960 p->nLastGain = p->nMffc;
1961 return pGraph;
1962 }
1963 if ( nSteps == 0 || p->nMffc == 1 )
1964 {
1965p->timeRes1 += Abc_Clock() - clk;
1966 return NULL;
1967 }
1968
1969 // get the one level divisors
1970 Abc_ManResubDivsS( p, Required );
1971
1972// if ( Vec_PtrSize(vLeaves) >= 6 )
1973// Abc_ManResubDumpInstance( p->vDivs, Vec_PtrSize(vLeaves), p->nDivs, p->nWords );
1974
1975 // consider one node
1976 if ( (pGraph = Abc_ManResubDivs1( p, Required )) )
1977 {
1978p->timeRes1 += Abc_Clock() - clk;
1979 p->nLastGain = p->nMffc - 1;
1980 return pGraph;
1981 }
1982p->timeRes1 += Abc_Clock() - clk;
1983 if ( nSteps == 1 || p->nMffc == 2 )
1984 return NULL;
1985
1986clk = Abc_Clock();
1987 // consider triples
1988 if ( (pGraph = Abc_ManResubDivs12( p, Required )) )
1989 {
1990p->timeRes2 += Abc_Clock() - clk;
1991 p->nLastGain = p->nMffc - 2;
1992 return pGraph;
1993 }
1994p->timeRes2 += Abc_Clock() - clk;
1995
1996 // get the two level divisors
1997clk = Abc_Clock();
1998 Abc_ManResubDivsD( p, Required );
1999p->timeResD += Abc_Clock() - clk;
2000
2001 // consider two nodes
2002clk = Abc_Clock();
2003 if ( (pGraph = Abc_ManResubDivs2( p, Required )) )
2004 {
2005p->timeRes2 += Abc_Clock() - clk;
2006 p->nLastGain = p->nMffc - 2;
2007 return pGraph;
2008 }
2009p->timeRes2 += Abc_Clock() - clk;
2010 if ( nSteps == 2 || p->nMffc == 3 )
2011 return NULL;
2012
2013 // consider two nodes
2014clk = Abc_Clock();
2015 if ( (pGraph = Abc_ManResubDivs3( p, Required )) )
2016 {
2017p->timeRes3 += Abc_Clock() - clk;
2018 p->nLastGain = p->nMffc - 3;
2019 return pGraph;
2020 }
2021p->timeRes3 += Abc_Clock() - clk;
2022 if ( nSteps == 3 || p->nLeavesMax == 4 )
2023 return NULL;
2024 return NULL;
2025}
2026
2027
2028
2029
2041int Abc_CutVolumeCheck_rec( Abc_Obj_t * pObj )
2042{
2043 // quit if the node is visited (or if it is a leaf)
2044 if ( Abc_NodeIsTravIdCurrent(pObj) )
2045 return 0;
2046 Abc_NodeSetTravIdCurrent(pObj);
2047 // report the error
2048 if ( Abc_ObjIsCi(pObj) )
2049 printf( "Abc_CutVolumeCheck() ERROR: The set of nodes is not a cut!\n" );
2050 // count the number of nodes in the leaves
2051 return 1 + Abc_CutVolumeCheck_rec( Abc_ObjFanin0(pObj) ) +
2052 Abc_CutVolumeCheck_rec( Abc_ObjFanin1(pObj) );
2053}
2054
2066int Abc_CutVolumeCheck( Abc_Obj_t * pNode, Vec_Ptr_t * vLeaves )
2067{
2068 Abc_Obj_t * pObj;
2069 int i;
2070 // mark the leaves
2071 Abc_NtkIncrementTravId( pNode->pNtk );
2072 Vec_PtrForEachEntry( Abc_Obj_t *, vLeaves, pObj, i )
2073 Abc_NodeSetTravIdCurrent( pObj );
2074 // traverse the nodes starting from the given one and count them
2075 return Abc_CutVolumeCheck_rec( pNode );
2076}
2077
2089void Abc_CutFactor_rec( Abc_Obj_t * pObj, Vec_Ptr_t * vLeaves )
2090{
2091 if ( pObj->fMarkA )
2092 return;
2093 if ( Abc_ObjIsCi(pObj) || (Abc_ObjFanoutNum(pObj) > 1 && !Abc_NodeIsMuxControlType(pObj)) )
2094 {
2095 Vec_PtrPush( vLeaves, pObj );
2096 pObj->fMarkA = 1;
2097 return;
2098 }
2099 Abc_CutFactor_rec( Abc_ObjFanin0(pObj), vLeaves );
2100 Abc_CutFactor_rec( Abc_ObjFanin1(pObj), vLeaves );
2101}
2102
2116Vec_Ptr_t * Abc_CutFactor( Abc_Obj_t * pNode )
2117{
2118 Vec_Ptr_t * vLeaves;
2119 Abc_Obj_t * pObj;
2120 int i;
2121 assert( !Abc_ObjIsCi(pNode) );
2122 vLeaves = Vec_PtrAlloc( 10 );
2123 Abc_CutFactor_rec( Abc_ObjFanin0(pNode), vLeaves );
2124 Abc_CutFactor_rec( Abc_ObjFanin1(pNode), vLeaves );
2125 Vec_PtrForEachEntry( Abc_Obj_t *, vLeaves, pObj, i )
2126 pObj->fMarkA = 0;
2127 return vLeaves;
2128}
2129
2146Vec_Ptr_t * Abc_CutFactorLarge( Abc_Obj_t * pNode, int nLeavesMax )
2147{
2148 Vec_Ptr_t * vLeaves, * vFactors, * vFact, * vNext;
2149 Vec_Int_t * vFeasible;
2150 Abc_Obj_t * pLeaf, * pTemp;
2151 int i, k, Counter, RandLeaf;
2152 int BestCut, BestShare;
2153 assert( Abc_ObjIsNode(pNode) );
2154 // get one factor-cut
2155 vLeaves = Abc_CutFactor( pNode );
2156 if ( Vec_PtrSize(vLeaves) > nLeavesMax )
2157 {
2158 Vec_PtrFree(vLeaves);
2159 return NULL;
2160 }
2161 if ( Vec_PtrSize(vLeaves) == nLeavesMax )
2162 return vLeaves;
2163 // initialize the factor cuts for the leaves
2164 vFactors = Vec_PtrAlloc( nLeavesMax );
2165 Abc_NtkIncrementTravId( pNode->pNtk );
2166 Vec_PtrForEachEntry( Abc_Obj_t *, vLeaves, pLeaf, i )
2167 {
2168 Abc_NodeSetTravIdCurrent( pLeaf );
2169 if ( Abc_ObjIsCi(pLeaf) )
2170 Vec_PtrPush( vFactors, NULL );
2171 else
2172 Vec_PtrPush( vFactors, Abc_CutFactor(pLeaf) );
2173 }
2174 // construct larger factor cuts
2175 vFeasible = Vec_IntAlloc( nLeavesMax );
2176 while ( 1 )
2177 {
2178 BestCut = -1, BestShare = -1;
2179 // find the next feasible cut to add
2180 Vec_IntClear( vFeasible );
2181 Vec_PtrForEachEntry( Vec_Ptr_t *, vFactors, vFact, i )
2182 {
2183 if ( vFact == NULL )
2184 continue;
2185 // count the number of unmarked leaves of this factor cut
2186 Counter = 0;
2187 Vec_PtrForEachEntry( Abc_Obj_t *, vFact, pTemp, k )
2188 Counter += !Abc_NodeIsTravIdCurrent(pTemp);
2189 // if the number of new leaves is smaller than the diff, it is feasible
2190 if ( Counter <= nLeavesMax - Vec_PtrSize(vLeaves) + 1 )
2191 {
2192 Vec_IntPush( vFeasible, i );
2193 if ( BestCut == -1 || BestShare < Vec_PtrSize(vFact) - Counter )
2194 BestCut = i, BestShare = Vec_PtrSize(vFact) - Counter;
2195 }
2196 }
2197 // quit if there is no feasible factor cuts
2198 if ( Vec_IntSize(vFeasible) == 0 )
2199 break;
2200 // randomly choose one leaf and get its factor cut
2201// RandLeaf = Vec_IntEntry( vFeasible, rand() % Vec_IntSize(vFeasible) );
2202 // choose the cut that has most sharing with the other cuts
2203 RandLeaf = BestCut;
2204
2205 pLeaf = (Abc_Obj_t *)Vec_PtrEntry( vLeaves, RandLeaf );
2206 vNext = (Vec_Ptr_t *)Vec_PtrEntry( vFactors, RandLeaf );
2207 // unmark this leaf
2208 Abc_NodeSetTravIdPrevious( pLeaf );
2209 // remove this cut from the leaves and factor cuts
2210 for ( i = RandLeaf; i < Vec_PtrSize(vLeaves)-1; i++ )
2211 {
2212 Vec_PtrWriteEntry( vLeaves, i, Vec_PtrEntry(vLeaves, i+1) );
2213 Vec_PtrWriteEntry( vFactors, i, Vec_PtrEntry(vFactors,i+1) );
2214 }
2215 Vec_PtrShrink( vLeaves, Vec_PtrSize(vLeaves) -1 );
2216 Vec_PtrShrink( vFactors, Vec_PtrSize(vFactors)-1 );
2217 // add new leaves, compute their factor cuts
2218 Vec_PtrForEachEntry( Abc_Obj_t *, vNext, pLeaf, i )
2219 {
2220 if ( Abc_NodeIsTravIdCurrent(pLeaf) )
2221 continue;
2222 Abc_NodeSetTravIdCurrent( pLeaf );
2223 Vec_PtrPush( vLeaves, pLeaf );
2224 if ( Abc_ObjIsCi(pLeaf) )
2225 Vec_PtrPush( vFactors, NULL );
2226 else
2227 Vec_PtrPush( vFactors, Abc_CutFactor(pLeaf) );
2228 }
2229 Vec_PtrFree( vNext );
2230 assert( Vec_PtrSize(vLeaves) <= nLeavesMax );
2231 if ( Vec_PtrSize(vLeaves) == nLeavesMax )
2232 break;
2233 }
2234
2235 // remove temporary storage
2236 Vec_PtrForEachEntry( Vec_Ptr_t *, vFactors, vFact, i )
2237 if ( vFact ) Vec_PtrFree( vFact );
2238 Vec_PtrFree( vFactors );
2239 Vec_IntFree( vFeasible );
2240 return vLeaves;
2241}
2242
2246
2247
2248ABC_NAMESPACE_IMPL_END
2249
nWords
int nWords
Definition abcNpn.c:127
Dec_GraphUpdateNetwork
int Dec_GraphUpdateNetwork(Abc_Obj_t *pRoot, Dec_Graph_t *pGraph, int fUpdateLevel, int nGain)
Definition decAbc.c:240
ABC_RS_DIV2_MAX
#define ABC_RS_DIV2_MAX
Definition abcOrchestration.c:45
Abc_ManRes_t
struct Abc_ManRes_t_ Abc_ManRes_t
Definition abcOrchestration.c:47
ABC_RS_DIV1_MAX
#define ABC_RS_DIV1_MAX
Definition abcOrchestration.c:44
Abc_NodeMffcInside
int Abc_NodeMffcInside(Abc_Obj_t *pNode, Vec_Ptr_t *vLeaves, Vec_Ptr_t *vInside)
Definition abcRefs.c:351
Abc_ManResubQuit3
Dec_Graph_t * Abc_ManResubQuit3(Abc_Obj_t *pRoot, Abc_Obj_t *pObj0, Abc_Obj_t *pObj1, Abc_Obj_t *pObj2, Abc_Obj_t *pObj3, int fOrGate)
Definition abcResub.c:811
Abc_CutFactor
Vec_Ptr_t * Abc_CutFactor(Abc_Obj_t *pNode)
Definition abcResub.c:2116
Abc_NtkResubstitute
int Abc_NtkResubstitute(Abc_Ntk_t *pNtk, int nCutMax, int nStepsMax, int nMinSaved, int nLevelsOdc, int fUpdateLevel, int fVerbose, int fVeryVerbose)
FUNCTION DEFINITIONS ///.
Definition abcResub.c:137
Abc_CutVolumeCheck_rec
int Abc_CutVolumeCheck_rec(Abc_Obj_t *pObj)
Definition abcResub.c:2041
Abc_ManResubQuit2
Dec_Graph_t * Abc_ManResubQuit2(Abc_Obj_t *pRoot, Abc_Obj_t *pObj0, Abc_Obj_t *pObj1, Abc_Obj_t *pObj2, int fOrGate)
Definition abcResub.c:766
Abc_ManResubQuit1
Dec_Graph_t * Abc_ManResubQuit1(Abc_Obj_t *pRoot, Abc_Obj_t *pObj0, Abc_Obj_t *pObj1, int fOrGate)
Definition abcResub.c:694
Abc_ManResubQuit21
Dec_Graph_t * Abc_ManResubQuit21(Abc_Obj_t *pRoot, Abc_Obj_t *pObj0, Abc_Obj_t *pObj1, Abc_Obj_t *pObj2, int fOrGate)
Definition abcResub.c:725
Abc_ManResubDumpInstance
void Abc_ManResubDumpInstance(Vec_Ptr_t *vDivs, int nLeaves, int nDivs, int nWords)
Definition abcResub.c:574
Abc_ManResubQuit0
Dec_Graph_t * Abc_ManResubQuit0(Abc_Obj_t *pRoot, Abc_Obj_t *pObj)
Definition abcResub.c:670
Abc_ManResubCollectDivs_rec
void Abc_ManResubCollectDivs_rec(Abc_Obj_t *pNode, Vec_Ptr_t *vInternal)
Definition abcResub.c:415
Abc_CutFactor_rec
void Abc_CutFactor_rec(Abc_Obj_t *pObj, Vec_Ptr_t *vLeaves)
Definition abcResub.c:2089
Abc_Obj_t
struct Abc_Obj_t_ Abc_Obj_t
Definition abc.h:116
Abc_NtkDontCareAlloc
ABC_DLL Odc_Man_t * Abc_NtkDontCareAlloc(int nVarsMax, int nLevels, int fVerbose, int fVeryVerbose)
FUNCTION DEFINITIONS ///.
Definition abcOdc.c:163
Abc_NtkForEachLatch
#define Abc_NtkForEachLatch(pNtk, pObj, i)
Definition abc.h:500
Abc_ObjRequiredLevel
ABC_DLL int Abc_ObjRequiredLevel(Abc_Obj_t *pObj)
Definition abcTiming.c:1214
Abc_NtkCheck
ABC_DLL int Abc_NtkCheck(Abc_Ntk_t *pNtk)
FUNCTION DEFINITIONS ///.
Definition abcCheck.c:64
Abc_NtkForEachObj
#define Abc_NtkForEachObj(pNtk, pObj, i)
ITERATORS ///.
Definition abc.h:449
Abc_NtkDontCareCompute
ABC_DLL int Abc_NtkDontCareCompute(Odc_Man_t *p, Abc_Obj_t *pNode, Vec_Ptr_t *vLeaves, unsigned *puTruth)
Definition abcOdc.c:1042
Abc_ObjForEachFanout
#define Abc_ObjForEachFanout(pObj, pFanout, i)
Definition abc.h:529
Abc_ManCut_t
struct Abc_ManCut_t_ Abc_ManCut_t
Definition abc.h:119
Odc_Man_t
struct Odc_Man_t_ Odc_Man_t
Definition abc.h:832
Abc_NtkDontCareClear
ABC_DLL void Abc_NtkDontCareClear(Odc_Man_t *p)
Definition abcOdc.c:244
Abc_Aig_t
struct Abc_Aig_t_ Abc_Aig_t
Definition abc.h:117
Abc_NtkManCutStop
ABC_DLL void Abc_NtkManCutStop(Abc_ManCut_t *p)
Definition abcReconv.c:623
Abc_Ntk_t
struct Abc_Ntk_t_ Abc_Ntk_t
Definition abc.h:115
Abc_NtkStopReverseLevels
ABC_DLL void Abc_NtkStopReverseLevels(Abc_Ntk_t *pNtk)
Definition abcTiming.c:1302
Abc_NodeIsMuxControlType
ABC_DLL int Abc_NodeIsMuxControlType(Abc_Obj_t *pNode)
Definition abcUtil.c:1398
Abc_NtkLevel
ABC_DLL int Abc_NtkLevel(Abc_Ntk_t *pNtk)
Definition abcDfs.c:1449
Abc_NodeFindCut
ABC_DLL Vec_Ptr_t * Abc_NodeFindCut(Abc_ManCut_t *p, Abc_Obj_t *pRoot, int fContain)
Definition abcReconv.c:256
Abc_AigCleanup
ABC_DLL int Abc_AigCleanup(Abc_Aig_t *pMan)
Definition abcAig.c:194
Abc_NtkStartReverseLevels
ABC_DLL void Abc_NtkStartReverseLevels(Abc_Ntk_t *pNtk, int nMaxLevelIncrease)
Definition abcTiming.c:1274
Abc_NtkDontCareFree
ABC_DLL void Abc_NtkDontCareFree(Odc_Man_t *p)
Definition abcOdc.c:276
Abc_NtkReassignIds
ABC_DLL void Abc_NtkReassignIds(Abc_Ntk_t *pNtk)
Definition abcUtil.c:1809
Abc_NtkCleanMarkAB
ABC_DLL void Abc_NtkCleanMarkAB(Abc_Ntk_t *pNtk)
Definition abcUtil.c:753
Abc_NtkManCutStart
ABC_DLL Abc_ManCut_t * Abc_NtkManCutStart(int nNodeSizeMax, int nConeSizeMax, int nNodeFanStop, int nConeFanStop)
Definition abcReconv.c:595
Abc_NtkForEachNode
#define Abc_NtkForEachNode(pNtk, pNode, i)
Definition abc.h:464
abctime
ABC_INT64_T abctime
Definition abc_global.h:332
ABC_PRT
#define ABC_PRT(a, t)
Definition abc_global.h:255
ABC_ALLOC
#define ABC_ALLOC(type, num)
Definition abc_global.h:264
ABC_INFINITY
#define ABC_INFINITY
MACRO DEFINITIONS ///.
Definition abc_global.h:250
ABC_FREE
#define ABC_FREE(obj)
Definition abc_global.h:267
ABC_NAMESPACE_IMPL_START
#define ABC_NAMESPACE_IMPL_START
Definition abc_namespaces.h:54
ABC_NAMESPACE_IMPL_END
#define ABC_NAMESPACE_IMPL_END
Definition abc_namespaces.h:55
Vec_Int_t
typedefABC_NAMESPACE_IMPL_START struct Vec_Int_t_ Vec_Int_t
DECLARATIONS ///.
Definition bblif.c:37
ProgressBar
ABC_NAMESPACE_IMPL_START typedef char ProgressBar
Definition bbrNtbdd.c:27
Dec_Edge_t
typedefABC_NAMESPACE_HEADER_START struct Dec_Edge_t_ Dec_Edge_t
INCLUDES ///.
Definition dec.h:42
Dec_Graph_t
struct Dec_Graph_t_ Dec_Graph_t
Definition dec.h:68
p
Cube * p
Definition exorList.c:222
Extra_ProgressBarStop
void Extra_ProgressBarStop(ProgressBar *p)
Definition extraUtilProgress.c:118
Extra_TimeStamp
char * Extra_TimeStamp()
Definition extraUtilFile.c:465
Extra_ProgressBarStart
ProgressBar * Extra_ProgressBarStart(FILE *pFile, int nItemsTotal)
FUNCTION DEFINITIONS ///.
Definition extraUtilProgress.c:62
Abc_ManRes_t_
Definition abcOrchestration.c:49
Abc_ManRes_t_::nUsedNode2Or
int nUsedNode2Or
Definition abcOrchestration.c:95
Abc_ManRes_t_::vDivs2UP1
Vec_Ptr_t * vDivs2UP1
Definition abcOrchestration.c:72
Abc_ManRes_t_::vDivs2UN0
Vec_Ptr_t * vDivs2UN0
Definition abcOrchestration.c:73
Abc_ManRes_t_::timeSim
abctime timeSim
Definition abcOrchestration.c:83
Abc_ManRes_t_::nUsedNode0
int nUsedNode0
Definition abcOrchestration.c:92
Abc_ManRes_t_::pInfo
unsigned * pInfo
Definition abcOrchestration.c:64
Abc_ManRes_t_::vDivs
Vec_Ptr_t * vDivs
Definition abcOrchestration.c:59
Abc_ManRes_t_::nNodesEnd
int nNodesEnd
Definition abcOrchestration.c:106
Abc_ManRes_t_::timeRes2
abctime timeRes2
Definition abcOrchestration.c:86
Abc_ManRes_t_::vDivs2UP0
Vec_Ptr_t * vDivs2UP0
Definition abcOrchestration.c:71
Abc_ManRes_t_::nMffc
int nMffc
Definition abcOrchestration.c:57
Abc_ManRes_t_::timeTruth
abctime timeTruth
Definition abcOrchestration.c:79
Abc_ManRes_t_::timeRes
abctime timeRes
Definition abcOrchestration.c:80
Abc_ManRes_t_::timeRes1
abctime timeRes1
Definition abcOrchestration.c:84
Abc_ManRes_t_::nLastGain
int nLastGain
Definition abcOrchestration.c:58
Abc_ManRes_t_::timeRes3
abctime timeRes3
Definition abcOrchestration.c:87
Abc_ManRes_t_::nTotalLeaves
int nTotalLeaves
Definition abcOrchestration.c:103
Abc_ManRes_t_::nNodesBeg
int nNodesBeg
Definition abcOrchestration.c:105
Abc_ManRes_t_::nLeavesMax
int nLeavesMax
Definition abcOrchestration.c:51
Abc_ManRes_t_::nDivsMax
int nDivsMax
Definition abcOrchestration.c:52
Abc_ManRes_t_::nDivs
int nDivs
Definition abcOrchestration.c:56
Abc_ManRes_t_::nUsedNode3AndOr
int nUsedNode3AndOr
Definition abcOrchestration.c:100
Abc_ManRes_t_::nUsedNode3OrAnd
int nUsedNode3OrAnd
Definition abcOrchestration.c:99
Abc_ManRes_t_::vDivs1UN
Vec_Ptr_t * vDivs1UN
Definition abcOrchestration.c:69
Abc_ManRes_t_::timeCut
abctime timeCut
Definition abcOrchestration.c:78
Abc_ManRes_t_::nUsedNode2AndOr
int nUsedNode2AndOr
Definition abcOrchestration.c:98
Abc_ManRes_t_::timeMffc
abctime timeMffc
Definition abcOrchestration.c:82
Abc_ManRes_t_::nTotalDivs
int nTotalDivs
Definition abcOrchestration.c:102
Abc_ManRes_t_::vSims
Vec_Ptr_t * vSims
Definition abcOrchestration.c:63
Abc_ManRes_t_::timeTotal
abctime timeTotal
Definition abcOrchestration.c:89
Abc_ManRes_t_::nUsedNode2OrAnd
int nUsedNode2OrAnd
Definition abcOrchestration.c:97
Abc_ManRes_t_::nUsedNode1And
int nUsedNode1And
Definition abcOrchestration.c:94
Abc_ManRes_t_::timeResD
abctime timeResD
Definition abcOrchestration.c:85
Abc_ManRes_t_::vDivs2UN1
Vec_Ptr_t * vDivs2UN1
Definition abcOrchestration.c:74
Abc_ManRes_t_::pRoot
Abc_Obj_t * pRoot
Definition abcOrchestration.c:54
Abc_ManRes_t_::nUsedNode2And
int nUsedNode2And
Definition abcOrchestration.c:96
Abc_ManRes_t_::timeNtk
abctime timeNtk
Definition abcOrchestration.c:88
Abc_ManRes_t_::nUsedNode1Or
int nUsedNode1Or
Definition abcOrchestration.c:93
Abc_ManRes_t_::nTotalGain
int nTotalGain
Definition abcOrchestration.c:104
Abc_ManRes_t_::nUsedNodeTotal
int nUsedNodeTotal
Definition abcOrchestration.c:101
Abc_ManRes_t_::pCareSet
unsigned * pCareSet
Definition abcOrchestration.c:66
Abc_ManRes_t_::nLeaves
int nLeaves
Definition abcOrchestration.c:55
Abc_ManRes_t_::nUsedNodeC
int nUsedNodeC
Definition abcOrchestration.c:91
Abc_ManRes_t_::vDivs1UP
Vec_Ptr_t * vDivs1UP
Definition abcOrchestration.c:68
Abc_ManRes_t_::timeDiv
abctime timeDiv
Definition abcOrchestration.c:81
Abc_ManRes_t_::vTemp
Vec_Ptr_t * vTemp
Definition abcOrchestration.c:76
Abc_ManRes_t_::vDivs1B
Vec_Ptr_t * vDivs1B
Definition abcOrchestration.c:70
Abc_ManRes_t_::nBits
int nBits
Definition abcOrchestration.c:61
Abc_Ntk_t_::pName
char * pName
Definition abc.h:158
Abc_Ntk_t_::pManFunc
void * pManFunc
Definition abc.h:191
Abc_Obj_t_::pData
void * pData
Definition abc.h:145
Abc_Obj_t_::pNtk
Abc_Ntk_t * pNtk
Definition abc.h:130
Abc_Obj_t_::Id
int Id
Definition abc.h:132
Abc_Obj_t_::fMarkA
unsigned fMarkA
Definition abc.h:134
Abc_Obj_t_::fPhase
unsigned fPhase
Definition abc.h:137
Abc_Obj_t_::pNext
Abc_Obj_t * pNext
Definition abc.h:131
Abc_Obj_t_::Level
unsigned Level
Definition abc.h:142
assert
#define assert(ex)
Definition util_old.h:213
memset
char * memset()
sprintf
char * sprintf()
Vec_PtrForEachEntryStart
#define Vec_PtrForEachEntryStart(Type, vVec, pEntry, i, Start)
Definition vecPtr.h:57
Vec_PtrForEachEntryStop
#define Vec_PtrForEachEntryStop(Type, vVec, pEntry, i, Stop)
Definition vecPtr.h:59
Vec_Ptr_t
typedefABC_NAMESPACE_HEADER_START struct Vec_Ptr_t_ Vec_Ptr_t
INCLUDES ///.
Definition vecPtr.h:42
Vec_PtrForEachEntry
#define Vec_PtrForEachEntry(Type, vVec, pEntry, i)
MACRO DEFINITIONS ///.
Definition vecPtr.h:55