abc-master
 All Data Structures Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros
abcResub.c
Go to the documentation of this file.
1 /**CFile****************************************************************
2 
3  FileName [abcResub.c]
4 
5  SystemName [ABC: Logic synthesis and verification system.]
6 
7  PackageName [Network and node package.]
8 
9  Synopsis [Resubstitution manager.]
10 
11  Author [Alan Mishchenko]
12 
13  Affiliation [UC Berkeley]
14 
15  Date [Ver. 1.0. Started - June 20, 2005.]
16 
17  Revision [$Id: abcResub.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
18 
19 ***********************************************************************/
20 
21 #include "base/abc/abc.h"
22 #include "bool/dec/dec.h"
23 
24 ABC_NAMESPACE_IMPL_START
25 
26 
27 ////////////////////////////////////////////////////////////////////////
28 /// DECLARATIONS ///
29 ////////////////////////////////////////////////////////////////////////
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 
34 typedef struct Abc_ManRes_t_ Abc_ManRes_t;
35 struct 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
97 static Abc_ManRes_t* Abc_ManResubStart( int nLeavesMax, int nDivsMax );
98 static void Abc_ManResubStop( Abc_ManRes_t * p );
99 static Dec_Graph_t * Abc_ManResubEval( Abc_ManRes_t * p, Abc_Obj_t * pRoot, Vec_Ptr_t * vLeaves, int nSteps, int fUpdateLevel, int fVerbose );
100 static void Abc_ManResubCleanup( Abc_ManRes_t * p );
101 static void Abc_ManResubPrint( Abc_ManRes_t * p );
102 
103 // other procedures
104 static int Abc_ManResubCollectDivs( Abc_ManRes_t * p, Abc_Obj_t * pRoot, Vec_Ptr_t * vLeaves, int Required );
105 static void Abc_ManResubSimulate( Vec_Ptr_t * vDivs, int nLeaves, Vec_Ptr_t * vSims, int nLeavesMax, int nWords );
106 static void Abc_ManResubPrintDivs( Abc_ManRes_t * p, Abc_Obj_t * pRoot, Vec_Ptr_t * vLeaves );
107 
108 static void Abc_ManResubDivsS( Abc_ManRes_t * p, int Required );
109 static void Abc_ManResubDivsD( Abc_ManRes_t * p, int Required );
110 static Dec_Graph_t * Abc_ManResubQuit( Abc_ManRes_t * p );
111 static Dec_Graph_t * Abc_ManResubDivs0( Abc_ManRes_t * p );
112 static Dec_Graph_t * Abc_ManResubDivs1( Abc_ManRes_t * p, int Required );
113 static Dec_Graph_t * Abc_ManResubDivs12( Abc_ManRes_t * p, int Required );
114 static Dec_Graph_t * Abc_ManResubDivs2( Abc_ManRes_t * p, int Required );
115 static Dec_Graph_t * Abc_ManResubDivs3( Abc_ManRes_t * p, int Required );
116 
117 static Vec_Ptr_t * Abc_CutFactorLarge( Abc_Obj_t * pNode, int nLeavesMax );
118 static int Abc_CutVolumeCheck( Abc_Obj_t * pNode, Vec_Ptr_t * vLeaves );
119 
120 extern abctime s_ResubTime;
121 
122 ////////////////////////////////////////////////////////////////////////
123 /// FUNCTION DEFINITIONS ///
124 ////////////////////////////////////////////////////////////////////////
125 
126 /**Function*************************************************************
127 
128  Synopsis [Performs incremental resynthesis of the AIG.]
129 
130  Description []
131 
132  SideEffects []
133 
134  SeeAlso []
135 
136 ***********************************************************************/
137 int Abc_NtkResubstitute( Abc_Ntk_t * pNtk, int nCutMax, int nStepsMax, int nLevelsOdc, int fUpdateLevel, int fVerbose, int fVeryVerbose )
138 {
139  extern void 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  Abc_NtkForEachNode( pNtk, pNode, i )
174  {
175  Extra_ProgressBarUpdate( pProgress, i, NULL );
176  // skip the constant node
177 // if ( Abc_NodeIsConst(pNode) )
178 // continue;
179  // skip persistant nodes
180  if ( Abc_NodeIsPersistant(pNode) )
181  continue;
182  // skip the nodes with many fanouts
183  if ( Abc_ObjFanoutNum(pNode) > 1000 )
184  continue;
185  // stop if all nodes have been tried once
186  if ( i >= nNodes )
187  break;
188 
189  // compute a reconvergence-driven cut
190 clk = Abc_Clock();
191  vLeaves = Abc_NodeFindCut( pManCut, pNode, 0 );
192 // vLeaves = Abc_CutFactorLarge( pNode, nCutMax );
193 pManRes->timeCut += Abc_Clock() - clk;
194 /*
195  if ( fVerbose && vLeaves )
196  printf( "Node %6d : Leaves = %3d. Volume = %3d.\n", pNode->Id, Vec_PtrSize(vLeaves), Abc_CutVolumeCheck(pNode, vLeaves) );
197  if ( vLeaves == NULL )
198  continue;
199 */
200  // get the don't-cares
201  if ( pManOdc )
202  {
203 clk = Abc_Clock();
204  Abc_NtkDontCareClear( pManOdc );
205  Abc_NtkDontCareCompute( pManOdc, pNode, vLeaves, pManRes->pCareSet );
206 pManRes->timeTruth += Abc_Clock() - clk;
207  }
208 
209  // evaluate this cut
210 clk = Abc_Clock();
211  pFForm = Abc_ManResubEval( pManRes, pNode, vLeaves, nStepsMax, fUpdateLevel, fVerbose );
212 // Vec_PtrFree( vLeaves );
213 // Abc_ManResubCleanup( pManRes );
214 pManRes->timeRes += Abc_Clock() - clk;
215  if ( pFForm == NULL )
216  continue;
217  pManRes->nTotalGain += pManRes->nLastGain;
218 /*
219  if ( pManRes->nLeaves == 4 && pManRes->nMffc == 2 && pManRes->nLastGain == 1 )
220  {
221  printf( "%6d : L = %2d. V = %2d. Mffc = %2d. Divs = %3d. Up = %3d. Un = %3d. B = %3d.\n",
222  pNode->Id, pManRes->nLeaves, Abc_CutVolumeCheck(pNode, vLeaves), pManRes->nMffc, pManRes->nDivs,
223  pManRes->vDivs1UP->nSize, pManRes->vDivs1UN->nSize, pManRes->vDivs1B->nSize );
224  Abc_ManResubPrintDivs( pManRes, pNode, vLeaves );
225  }
226 */
227  // acceptable replacement found, update the graph
228 clk = Abc_Clock();
229  Dec_GraphUpdateNetwork( pNode, pFForm, fUpdateLevel, pManRes->nLastGain );
230 pManRes->timeNtk += Abc_Clock() - clk;
231  Dec_GraphFree( pFForm );
232  }
233  Extra_ProgressBarStop( pProgress );
234 pManRes->timeTotal = Abc_Clock() - clkStart;
235  pManRes->nNodesEnd = Abc_NtkNodeNum(pNtk);
236 
237  // print statistics
238  if ( fVerbose )
239  Abc_ManResubPrint( pManRes );
240 
241  // delete the managers
242  Abc_ManResubStop( pManRes );
243  Abc_NtkManCutStop( pManCut );
244  if ( pManOdc ) Abc_NtkDontCareFree( pManOdc );
245 
246  // clean the data field
247  Abc_NtkForEachObj( pNtk, pNode, i )
248  pNode->pData = NULL;
249 
250  if ( Abc_NtkLatchNum(pNtk) ) {
251  Abc_NtkForEachLatch(pNtk, pNode, i)
252  pNode->pData = pNode->pNext, pNode->pNext = NULL;
253  }
254 
255  // put the nodes into the DFS order and reassign their IDs
256  Abc_NtkReassignIds( pNtk );
257 // Abc_AigCheckFaninOrder( pNtk->pManFunc );
258  // fix the levels
259  if ( fUpdateLevel )
260  Abc_NtkStopReverseLevels( pNtk );
261  else
262  Abc_NtkLevel( pNtk );
263  // check
264  if ( !Abc_NtkCheck( pNtk ) )
265  {
266  printf( "Abc_NtkRefactor: The network check has failed.\n" );
267  return 0;
268  }
269 s_ResubTime = Abc_Clock() - clkStart;
270  return 1;
271 }
272 
273 
274 
275 
276 /**Function*************************************************************
277 
278  Synopsis []
279 
280  Description []
281 
282  SideEffects []
283 
284  SeeAlso []
285 
286 ***********************************************************************/
287 Abc_ManRes_t * Abc_ManResubStart( int nLeavesMax, int nDivsMax )
288 {
289  Abc_ManRes_t * p;
290  unsigned * pData;
291  int i, k;
292  assert( sizeof(unsigned) == 4 );
293  p = ABC_ALLOC( Abc_ManRes_t, 1 );
294  memset( p, 0, sizeof(Abc_ManRes_t) );
295  p->nLeavesMax = nLeavesMax;
296  p->nDivsMax = nDivsMax;
297  p->vDivs = Vec_PtrAlloc( p->nDivsMax );
298  // allocate simulation info
299  p->nBits = (1 << p->nLeavesMax);
300  p->nWords = (p->nBits <= 32)? 1 : (p->nBits / 32);
301  p->pInfo = ABC_ALLOC( unsigned, p->nWords * (p->nDivsMax + 1) );
302  memset( p->pInfo, 0, sizeof(unsigned) * p->nWords * p->nLeavesMax );
303  p->vSims = Vec_PtrAlloc( p->nDivsMax );
304  for ( i = 0; i < p->nDivsMax; i++ )
305  Vec_PtrPush( p->vSims, p->pInfo + i * p->nWords );
306  // assign the care set
307  p->pCareSet = p->pInfo + p->nDivsMax * p->nWords;
308  Abc_InfoFill( p->pCareSet, p->nWords );
309  // set elementary truth tables
310  for ( k = 0; k < p->nLeavesMax; k++ )
311  {
312  pData = (unsigned *)p->vSims->pArray[k];
313  for ( i = 0; i < p->nBits; i++ )
314  if ( i & (1 << k) )
315  pData[i>>5] |= (1 << (i&31));
316  }
317  // create the remaining divisors
318  p->vDivs1UP = Vec_PtrAlloc( p->nDivsMax );
319  p->vDivs1UN = Vec_PtrAlloc( p->nDivsMax );
320  p->vDivs1B = Vec_PtrAlloc( p->nDivsMax );
321  p->vDivs2UP0 = Vec_PtrAlloc( p->nDivsMax );
322  p->vDivs2UP1 = Vec_PtrAlloc( p->nDivsMax );
323  p->vDivs2UN0 = Vec_PtrAlloc( p->nDivsMax );
324  p->vDivs2UN1 = Vec_PtrAlloc( p->nDivsMax );
325  p->vTemp = Vec_PtrAlloc( p->nDivsMax );
326  return p;
327 }
328 
329 /**Function*************************************************************
330 
331  Synopsis []
332 
333  Description []
334 
335  SideEffects []
336 
337  SeeAlso []
338 
339 ***********************************************************************/
340 void Abc_ManResubStop( Abc_ManRes_t * p )
341 {
342  Vec_PtrFree( p->vDivs );
343  Vec_PtrFree( p->vSims );
344  Vec_PtrFree( p->vDivs1UP );
345  Vec_PtrFree( p->vDivs1UN );
346  Vec_PtrFree( p->vDivs1B );
347  Vec_PtrFree( p->vDivs2UP0 );
348  Vec_PtrFree( p->vDivs2UP1 );
349  Vec_PtrFree( p->vDivs2UN0 );
350  Vec_PtrFree( p->vDivs2UN1 );
351  Vec_PtrFree( p->vTemp );
352  ABC_FREE( p->pInfo );
353  ABC_FREE( p );
354 }
355 
356 /**Function*************************************************************
357 
358  Synopsis []
359 
360  Description []
361 
362  SideEffects []
363 
364  SeeAlso []
365 
366 ***********************************************************************/
367 void Abc_ManResubPrint( Abc_ManRes_t * p )
368 {
369  printf( "Used constants = %6d. ", p->nUsedNodeC ); ABC_PRT( "Cuts ", p->timeCut );
370  printf( "Used replacements = %6d. ", p->nUsedNode0 ); ABC_PRT( "Resub ", p->timeRes );
371  printf( "Used single ORs = %6d. ", p->nUsedNode1Or ); ABC_PRT( " Div ", p->timeDiv );
372  printf( "Used single ANDs = %6d. ", p->nUsedNode1And ); ABC_PRT( " Mffc ", p->timeMffc );
373  printf( "Used double ORs = %6d. ", p->nUsedNode2Or ); ABC_PRT( " Sim ", p->timeSim );
374  printf( "Used double ANDs = %6d. ", p->nUsedNode2And ); ABC_PRT( " 1 ", p->timeRes1 );
375  printf( "Used OR-AND = %6d. ", p->nUsedNode2OrAnd ); ABC_PRT( " D ", p->timeResD );
376  printf( "Used AND-OR = %6d. ", p->nUsedNode2AndOr ); ABC_PRT( " 2 ", p->timeRes2 );
377  printf( "Used OR-2ANDs = %6d. ", p->nUsedNode3OrAnd ); ABC_PRT( "Truth ", p->timeTruth ); //ABC_PRT( " 3 ", p->timeRes3 );
378  printf( "Used AND-2ORs = %6d. ", p->nUsedNode3AndOr ); ABC_PRT( "AIG ", p->timeNtk );
379  printf( "TOTAL = %6d. ", p->nUsedNodeC +
380  p->nUsedNode0 +
381  p->nUsedNode1Or +
382  p->nUsedNode1And +
383  p->nUsedNode2Or +
384  p->nUsedNode2And +
385  p->nUsedNode2OrAnd +
386  p->nUsedNode2AndOr +
387  p->nUsedNode3OrAnd +
388  p->nUsedNode3AndOr
389  ); ABC_PRT( "TOTAL ", p->timeTotal );
390  printf( "Total leaves = %8d.\n", p->nTotalLeaves );
391  printf( "Total divisors = %8d.\n", p->nTotalDivs );
392 // printf( "Total gain = %8d.\n", p->nTotalGain );
393  printf( "Gain = %8d. (%6.2f %%).\n", p->nNodesBeg-p->nNodesEnd, 100.0*(p->nNodesBeg-p->nNodesEnd)/p->nNodesBeg );
394 }
395 
396 
397 /**Function*************************************************************
398 
399  Synopsis []
400 
401  Description []
402 
403  SideEffects []
404 
405  SeeAlso []
406 
407 ***********************************************************************/
408 void Abc_ManResubCollectDivs_rec( Abc_Obj_t * pNode, Vec_Ptr_t * vInternal )
409 {
410  // skip visited nodes
411  if ( Abc_NodeIsTravIdCurrent(pNode) )
412  return;
413  Abc_NodeSetTravIdCurrent(pNode);
414  // collect the fanins
415  Abc_ManResubCollectDivs_rec( Abc_ObjFanin0(pNode), vInternal );
416  Abc_ManResubCollectDivs_rec( Abc_ObjFanin1(pNode), vInternal );
417  // collect the internal node
418  if ( pNode->fMarkA == 0 )
419  Vec_PtrPush( vInternal, pNode );
420 }
421 
422 /**Function*************************************************************
423 
424  Synopsis []
425 
426  Description []
427 
428  SideEffects []
429 
430  SeeAlso []
431 
432 ***********************************************************************/
433 int Abc_ManResubCollectDivs( Abc_ManRes_t * p, Abc_Obj_t * pRoot, Vec_Ptr_t * vLeaves, int Required )
434 {
435  Abc_Obj_t * pNode, * pFanout;
436  int i, k, Limit, Counter;
437 
438  Vec_PtrClear( p->vDivs1UP );
439  Vec_PtrClear( p->vDivs1UN );
440  Vec_PtrClear( p->vDivs1B );
441 
442  // add the leaves of the cuts to the divisors
443  Vec_PtrClear( p->vDivs );
444  Abc_NtkIncrementTravId( pRoot->pNtk );
445  Vec_PtrForEachEntry( Abc_Obj_t *, vLeaves, pNode, i )
446  {
447  Vec_PtrPush( p->vDivs, pNode );
448  Abc_NodeSetTravIdCurrent( pNode );
449  }
450 
451  // mark nodes in the MFFC
452  Vec_PtrForEachEntry( Abc_Obj_t *, p->vTemp, pNode, i )
453  pNode->fMarkA = 1;
454  // collect the cone (without MFFC)
455  Abc_ManResubCollectDivs_rec( pRoot, p->vDivs );
456  // unmark the current MFFC
457  Vec_PtrForEachEntry( Abc_Obj_t *, p->vTemp, pNode, i )
458  pNode->fMarkA = 0;
459 
460  // check if the number of divisors is not exceeded
461  if ( Vec_PtrSize(p->vDivs) - Vec_PtrSize(vLeaves) + Vec_PtrSize(p->vTemp) >= Vec_PtrSize(p->vSims) - p->nLeavesMax )
462  return 0;
463 
464  // get the number of divisors to collect
465  Limit = Vec_PtrSize(p->vSims) - p->nLeavesMax - (Vec_PtrSize(p->vDivs) - Vec_PtrSize(vLeaves) + Vec_PtrSize(p->vTemp));
466 
467  // explore the fanouts, which are not in the MFFC
468  Counter = 0;
469  Vec_PtrForEachEntry( Abc_Obj_t *, p->vDivs, pNode, i )
470  {
471  if ( Abc_ObjFanoutNum(pNode) > 100 )
472  {
473 // printf( "%d ", Abc_ObjFanoutNum(pNode) );
474  continue;
475  }
476  // if the fanout has both fanins in the set, add it
477  Abc_ObjForEachFanout( pNode, pFanout, k )
478  {
479  if ( Abc_NodeIsTravIdCurrent(pFanout) || Abc_ObjIsCo(pFanout) || (int)pFanout->Level > Required )
480  continue;
481  if ( Abc_NodeIsTravIdCurrent(Abc_ObjFanin0(pFanout)) && Abc_NodeIsTravIdCurrent(Abc_ObjFanin1(pFanout)) )
482  {
483  if ( Abc_ObjFanin0(pFanout) == pRoot || Abc_ObjFanin1(pFanout) == pRoot )
484  continue;
485  Vec_PtrPush( p->vDivs, pFanout );
486  Abc_NodeSetTravIdCurrent( pFanout );
487  // quit computing divisors if there is too many of them
488  if ( ++Counter == Limit )
489  goto Quits;
490  }
491  }
492  }
493 
494 Quits :
495  // get the number of divisors
496  p->nDivs = Vec_PtrSize(p->vDivs);
497 
498  // add the nodes in the MFFC
499  Vec_PtrForEachEntry( Abc_Obj_t *, p->vTemp, pNode, i )
500  Vec_PtrPush( p->vDivs, pNode );
501  assert( pRoot == Vec_PtrEntryLast(p->vDivs) );
502 
503  assert( Vec_PtrSize(p->vDivs) - Vec_PtrSize(vLeaves) <= Vec_PtrSize(p->vSims) - p->nLeavesMax );
504  return 1;
505 }
506 
507 /**Function*************************************************************
508 
509  Synopsis []
510 
511  Description []
512 
513  SideEffects []
514 
515  SeeAlso []
516 
517 ***********************************************************************/
518 void Abc_ManResubPrintDivs( Abc_ManRes_t * p, Abc_Obj_t * pRoot, Vec_Ptr_t * vLeaves )
519 {
520  Abc_Obj_t * pFanin, * pNode;
521  int i, k;
522  // print the nodes
523  Vec_PtrForEachEntry( Abc_Obj_t *, p->vDivs, pNode, i )
524  {
525  if ( i < Vec_PtrSize(vLeaves) )
526  {
527  printf( "%6d : %c\n", pNode->Id, 'a'+i );
528  continue;
529  }
530  printf( "%6d : %2d = ", pNode->Id, i );
531  // find the first fanin
532  Vec_PtrForEachEntry( Abc_Obj_t *, p->vDivs, pFanin, k )
533  if ( Abc_ObjFanin0(pNode) == pFanin )
534  break;
535  if ( k < Vec_PtrSize(vLeaves) )
536  printf( "%c", 'a' + k );
537  else
538  printf( "%d", k );
539  printf( "%s ", Abc_ObjFaninC0(pNode)? "\'" : "" );
540  // find the second fanin
541  Vec_PtrForEachEntry( Abc_Obj_t *, p->vDivs, pFanin, k )
542  if ( Abc_ObjFanin1(pNode) == pFanin )
543  break;
544  if ( k < Vec_PtrSize(vLeaves) )
545  printf( "%c", 'a' + k );
546  else
547  printf( "%d", k );
548  printf( "%s ", Abc_ObjFaninC1(pNode)? "\'" : "" );
549  if ( pNode == pRoot )
550  printf( " root" );
551  printf( "\n" );
552  }
553  printf( "\n" );
554 }
555 
556 
557 /**Function*************************************************************
558 
559  Synopsis [Performs simulation.]
560 
561  Description []
562 
563  SideEffects []
564 
565  SeeAlso []
566 
567 ***********************************************************************/
568 void Abc_ManResubSimulate( Vec_Ptr_t * vDivs, int nLeaves, Vec_Ptr_t * vSims, int nLeavesMax, int nWords )
569 {
570  Abc_Obj_t * pObj;
571  unsigned * puData0, * puData1, * puData;
572  int i, k;
573  assert( Vec_PtrSize(vDivs) - nLeaves <= Vec_PtrSize(vSims) - nLeavesMax );
574  // simulate
575  Vec_PtrForEachEntry( Abc_Obj_t *, vDivs, pObj, i )
576  {
577  if ( i < nLeaves )
578  { // initialize the leaf
579  pObj->pData = Vec_PtrEntry( vSims, i );
580  continue;
581  }
582  // set storage for the node's simulation info
583  pObj->pData = Vec_PtrEntry( vSims, i - nLeaves + nLeavesMax );
584  // get pointer to the simulation info
585  puData = (unsigned *)pObj->pData;
586  puData0 = (unsigned *)Abc_ObjFanin0(pObj)->pData;
587  puData1 = (unsigned *)Abc_ObjFanin1(pObj)->pData;
588  // simulate
589  if ( Abc_ObjFaninC0(pObj) && Abc_ObjFaninC1(pObj) )
590  for ( k = 0; k < nWords; k++ )
591  puData[k] = ~puData0[k] & ~puData1[k];
592  else if ( Abc_ObjFaninC0(pObj) )
593  for ( k = 0; k < nWords; k++ )
594  puData[k] = ~puData0[k] & puData1[k];
595  else if ( Abc_ObjFaninC1(pObj) )
596  for ( k = 0; k < nWords; k++ )
597  puData[k] = puData0[k] & ~puData1[k];
598  else
599  for ( k = 0; k < nWords; k++ )
600  puData[k] = puData0[k] & puData1[k];
601  }
602  // normalize
603  Vec_PtrForEachEntry( Abc_Obj_t *, vDivs, pObj, i )
604  {
605  puData = (unsigned *)pObj->pData;
606  pObj->fPhase = (puData[0] & 1);
607  if ( pObj->fPhase )
608  for ( k = 0; k < nWords; k++ )
609  puData[k] = ~puData[k];
610  }
611 }
612 
613 
614 /**Function*************************************************************
615 
616  Synopsis []
617 
618  Description []
619 
620  SideEffects []
621 
622  SeeAlso []
623 
624 ***********************************************************************/
625 Dec_Graph_t * Abc_ManResubQuit0( Abc_Obj_t * pRoot, Abc_Obj_t * pObj )
626 {
627  Dec_Graph_t * pGraph;
628  Dec_Edge_t eRoot;
629  pGraph = Dec_GraphCreate( 1 );
630  Dec_GraphNode( pGraph, 0 )->pFunc = pObj;
631  eRoot = Dec_EdgeCreate( 0, pObj->fPhase );
632  Dec_GraphSetRoot( pGraph, eRoot );
633  if ( pRoot->fPhase )
634  Dec_GraphComplement( pGraph );
635  return pGraph;
636 }
637 
638 /**Function*************************************************************
639 
640  Synopsis []
641 
642  Description []
643 
644  SideEffects []
645 
646  SeeAlso []
647 
648 ***********************************************************************/
649 Dec_Graph_t * Abc_ManResubQuit1( Abc_Obj_t * pRoot, Abc_Obj_t * pObj0, Abc_Obj_t * pObj1, int fOrGate )
650 {
651  Dec_Graph_t * pGraph;
652  Dec_Edge_t eRoot, eNode0, eNode1;
653  assert( pObj0 != pObj1 );
654  assert( !Abc_ObjIsComplement(pObj0) );
655  assert( !Abc_ObjIsComplement(pObj1) );
656  pGraph = Dec_GraphCreate( 2 );
657  Dec_GraphNode( pGraph, 0 )->pFunc = pObj0;
658  Dec_GraphNode( pGraph, 1 )->pFunc = pObj1;
659  eNode0 = Dec_EdgeCreate( 0, pObj0->fPhase );
660  eNode1 = Dec_EdgeCreate( 1, pObj1->fPhase );
661  if ( fOrGate )
662  eRoot = Dec_GraphAddNodeOr( pGraph, eNode0, eNode1 );
663  else
664  eRoot = Dec_GraphAddNodeAnd( pGraph, eNode0, eNode1 );
665  Dec_GraphSetRoot( pGraph, eRoot );
666  if ( pRoot->fPhase )
667  Dec_GraphComplement( pGraph );
668  return pGraph;
669 }
670 
671 /**Function*************************************************************
672 
673  Synopsis []
674 
675  Description []
676 
677  SideEffects []
678 
679  SeeAlso []
680 
681 ***********************************************************************/
682 Dec_Graph_t * Abc_ManResubQuit21( Abc_Obj_t * pRoot, Abc_Obj_t * pObj0, Abc_Obj_t * pObj1, Abc_Obj_t * pObj2, int fOrGate )
683 {
684  Dec_Graph_t * pGraph;
685  Dec_Edge_t eRoot, eNode0, eNode1, eNode2;
686  assert( pObj0 != pObj1 );
687  assert( !Abc_ObjIsComplement(pObj0) );
688  assert( !Abc_ObjIsComplement(pObj1) );
689  assert( !Abc_ObjIsComplement(pObj2) );
690  pGraph = Dec_GraphCreate( 3 );
691  Dec_GraphNode( pGraph, 0 )->pFunc = pObj0;
692  Dec_GraphNode( pGraph, 1 )->pFunc = pObj1;
693  Dec_GraphNode( pGraph, 2 )->pFunc = pObj2;
694  eNode0 = Dec_EdgeCreate( 0, pObj0->fPhase );
695  eNode1 = Dec_EdgeCreate( 1, pObj1->fPhase );
696  eNode2 = Dec_EdgeCreate( 2, pObj2->fPhase );
697  if ( fOrGate )
698  {
699  eRoot = Dec_GraphAddNodeOr( pGraph, eNode0, eNode1 );
700  eRoot = Dec_GraphAddNodeOr( pGraph, eNode2, eRoot );
701  }
702  else
703  {
704  eRoot = Dec_GraphAddNodeAnd( pGraph, eNode0, eNode1 );
705  eRoot = Dec_GraphAddNodeAnd( pGraph, eNode2, eRoot );
706  }
707  Dec_GraphSetRoot( pGraph, eRoot );
708  if ( pRoot->fPhase )
709  Dec_GraphComplement( pGraph );
710  return pGraph;
711 }
712 
713 /**Function*************************************************************
714 
715  Synopsis []
716 
717  Description []
718 
719  SideEffects []
720 
721  SeeAlso []
722 
723 ***********************************************************************/
724 Dec_Graph_t * Abc_ManResubQuit2( Abc_Obj_t * pRoot, Abc_Obj_t * pObj0, Abc_Obj_t * pObj1, Abc_Obj_t * pObj2, int fOrGate )
725 {
726  Dec_Graph_t * pGraph;
727  Dec_Edge_t eRoot, ePrev, eNode0, eNode1, eNode2;
728  assert( pObj0 != pObj1 );
729  assert( pObj0 != pObj2 );
730  assert( pObj1 != pObj2 );
731  assert( !Abc_ObjIsComplement(pObj0) );
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 );
737  if ( Abc_ObjIsComplement(pObj1) && Abc_ObjIsComplement(pObj2) )
738  {
739  eNode1 = Dec_EdgeCreate( 1, Abc_ObjRegular(pObj1)->fPhase );
740  eNode2 = Dec_EdgeCreate( 2, Abc_ObjRegular(pObj2)->fPhase );
741  ePrev = Dec_GraphAddNodeOr( pGraph, eNode1, eNode2 );
742  }
743  else
744  {
745  eNode1 = Dec_EdgeCreate( 1, Abc_ObjRegular(pObj1)->fPhase ^ Abc_ObjIsComplement(pObj1) );
746  eNode2 = Dec_EdgeCreate( 2, Abc_ObjRegular(pObj2)->fPhase ^ Abc_ObjIsComplement(pObj2) );
747  ePrev = Dec_GraphAddNodeAnd( pGraph, eNode1, eNode2 );
748  }
749  if ( fOrGate )
750  eRoot = Dec_GraphAddNodeOr( pGraph, eNode0, ePrev );
751  else
752  eRoot = Dec_GraphAddNodeAnd( pGraph, eNode0, ePrev );
753  Dec_GraphSetRoot( pGraph, eRoot );
754  if ( pRoot->fPhase )
755  Dec_GraphComplement( pGraph );
756  return pGraph;
757 }
758 
759 /**Function*************************************************************
760 
761  Synopsis []
762 
763  Description []
764 
765  SideEffects []
766 
767  SeeAlso []
768 
769 ***********************************************************************/
770 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 )
771 {
772  Dec_Graph_t * pGraph;
773  Dec_Edge_t eRoot, ePrev0, ePrev1, eNode0, eNode1, eNode2, eNode3;
774  assert( pObj0 != pObj1 );
775  assert( pObj2 != pObj3 );
776  pGraph = Dec_GraphCreate( 4 );
777  Dec_GraphNode( pGraph, 0 )->pFunc = Abc_ObjRegular(pObj0);
778  Dec_GraphNode( pGraph, 1 )->pFunc = Abc_ObjRegular(pObj1);
779  Dec_GraphNode( pGraph, 2 )->pFunc = Abc_ObjRegular(pObj2);
780  Dec_GraphNode( pGraph, 3 )->pFunc = Abc_ObjRegular(pObj3);
781  if ( Abc_ObjIsComplement(pObj0) && Abc_ObjIsComplement(pObj1) )
782  {
783  eNode0 = Dec_EdgeCreate( 0, Abc_ObjRegular(pObj0)->fPhase );
784  eNode1 = Dec_EdgeCreate( 1, Abc_ObjRegular(pObj1)->fPhase );
785  ePrev0 = Dec_GraphAddNodeOr( pGraph, eNode0, eNode1 );
786  if ( Abc_ObjIsComplement(pObj2) && Abc_ObjIsComplement(pObj3) )
787  {
788  eNode2 = Dec_EdgeCreate( 2, Abc_ObjRegular(pObj2)->fPhase );
789  eNode3 = Dec_EdgeCreate( 3, Abc_ObjRegular(pObj3)->fPhase );
790  ePrev1 = Dec_GraphAddNodeOr( pGraph, eNode2, eNode3 );
791  }
792  else
793  {
794  eNode2 = Dec_EdgeCreate( 2, Abc_ObjRegular(pObj2)->fPhase ^ Abc_ObjIsComplement(pObj2) );
795  eNode3 = Dec_EdgeCreate( 3, Abc_ObjRegular(pObj3)->fPhase ^ Abc_ObjIsComplement(pObj3) );
796  ePrev1 = Dec_GraphAddNodeAnd( pGraph, eNode2, eNode3 );
797  }
798  }
799  else
800  {
801  eNode0 = Dec_EdgeCreate( 0, Abc_ObjRegular(pObj0)->fPhase ^ Abc_ObjIsComplement(pObj0) );
802  eNode1 = Dec_EdgeCreate( 1, Abc_ObjRegular(pObj1)->fPhase ^ Abc_ObjIsComplement(pObj1) );
803  ePrev0 = Dec_GraphAddNodeAnd( pGraph, eNode0, eNode1 );
804  if ( Abc_ObjIsComplement(pObj2) && Abc_ObjIsComplement(pObj3) )
805  {
806  eNode2 = Dec_EdgeCreate( 2, Abc_ObjRegular(pObj2)->fPhase );
807  eNode3 = Dec_EdgeCreate( 3, Abc_ObjRegular(pObj3)->fPhase );
808  ePrev1 = Dec_GraphAddNodeOr( pGraph, eNode2, eNode3 );
809  }
810  else
811  {
812  eNode2 = Dec_EdgeCreate( 2, Abc_ObjRegular(pObj2)->fPhase ^ Abc_ObjIsComplement(pObj2) );
813  eNode3 = Dec_EdgeCreate( 3, Abc_ObjRegular(pObj3)->fPhase ^ Abc_ObjIsComplement(pObj3) );
814  ePrev1 = Dec_GraphAddNodeAnd( pGraph, eNode2, eNode3 );
815  }
816  }
817  if ( fOrGate )
818  eRoot = Dec_GraphAddNodeOr( pGraph, ePrev0, ePrev1 );
819  else
820  eRoot = Dec_GraphAddNodeAnd( pGraph, ePrev0, ePrev1 );
821  Dec_GraphSetRoot( pGraph, eRoot );
822  if ( pRoot->fPhase )
823  Dec_GraphComplement( pGraph );
824  return pGraph;
825 }
826 
827 
828 
829 
830 /**Function*************************************************************
831 
832  Synopsis [Derives single-node unate/binate divisors.]
833 
834  Description []
835 
836  SideEffects []
837 
838  SeeAlso []
839 
840 ***********************************************************************/
841 void Abc_ManResubDivsS( Abc_ManRes_t * p, int Required )
842 {
843  Abc_Obj_t * pObj;
844  unsigned * puData, * puDataR;
845  int i, w;
846  Vec_PtrClear( p->vDivs1UP );
847  Vec_PtrClear( p->vDivs1UN );
848  Vec_PtrClear( p->vDivs1B );
849  puDataR = (unsigned *)p->pRoot->pData;
850  Vec_PtrForEachEntryStop( Abc_Obj_t *, p->vDivs, pObj, i, p->nDivs )
851  {
852  if ( (int)pObj->Level > Required - 1 )
853  continue;
854 
855  puData = (unsigned *)pObj->pData;
856  // check positive containment
857  for ( w = 0; w < p->nWords; w++ )
858 // if ( puData[w] & ~puDataR[w] )
859  if ( puData[w] & ~puDataR[w] & p->pCareSet[w] ) // care set
860  break;
861  if ( w == p->nWords )
862  {
863  Vec_PtrPush( p->vDivs1UP, pObj );
864  continue;
865  }
866  // check negative containment
867  for ( w = 0; w < p->nWords; w++ )
868 // if ( ~puData[w] & puDataR[w] )
869  if ( ~puData[w] & puDataR[w] & p->pCareSet[w] ) // care set
870  break;
871  if ( w == p->nWords )
872  {
873  Vec_PtrPush( p->vDivs1UN, pObj );
874  continue;
875  }
876  // add the node to binates
877  Vec_PtrPush( p->vDivs1B, pObj );
878  }
879 }
880 
881 /**Function*************************************************************
882 
883  Synopsis [Derives double-node unate/binate divisors.]
884 
885  Description []
886 
887  SideEffects []
888 
889  SeeAlso []
890 
891 ***********************************************************************/
892 void Abc_ManResubDivsD( Abc_ManRes_t * p, int Required )
893 {
894  Abc_Obj_t * pObj0, * pObj1;
895  unsigned * puData0, * puData1, * puDataR;
896  int i, k, w;
897  Vec_PtrClear( p->vDivs2UP0 );
898  Vec_PtrClear( p->vDivs2UP1 );
899  Vec_PtrClear( p->vDivs2UN0 );
900  Vec_PtrClear( p->vDivs2UN1 );
901  puDataR = (unsigned *)p->pRoot->pData;
902  Vec_PtrForEachEntry( Abc_Obj_t *, p->vDivs1B, pObj0, i )
903  {
904  if ( (int)pObj0->Level > Required - 2 )
905  continue;
906 
907  puData0 = (unsigned *)pObj0->pData;
908  Vec_PtrForEachEntryStart( Abc_Obj_t *, p->vDivs1B, pObj1, k, i + 1 )
909  {
910  if ( (int)pObj1->Level > Required - 2 )
911  continue;
912 
913  puData1 = (unsigned *)pObj1->pData;
914 
915  if ( Vec_PtrSize(p->vDivs2UP0) < ABC_RS_DIV2_MAX )
916  {
917  // get positive unate divisors
918  for ( w = 0; w < p->nWords; w++ )
919 // if ( (puData0[w] & puData1[w]) & ~puDataR[w] )
920  if ( (puData0[w] & puData1[w]) & ~puDataR[w] & p->pCareSet[w] ) // care set
921  break;
922  if ( w == p->nWords )
923  {
924  Vec_PtrPush( p->vDivs2UP0, pObj0 );
925  Vec_PtrPush( p->vDivs2UP1, pObj1 );
926  }
927  for ( w = 0; w < p->nWords; w++ )
928 // if ( (~puData0[w] & puData1[w]) & ~puDataR[w] )
929  if ( (~puData0[w] & puData1[w]) & ~puDataR[w] & p->pCareSet[w] ) // care set
930  break;
931  if ( w == p->nWords )
932  {
933  Vec_PtrPush( p->vDivs2UP0, Abc_ObjNot(pObj0) );
934  Vec_PtrPush( p->vDivs2UP1, pObj1 );
935  }
936  for ( w = 0; w < p->nWords; w++ )
937 // if ( (puData0[w] & ~puData1[w]) & ~puDataR[w] )
938  if ( (puData0[w] & ~puData1[w]) & ~puDataR[w] & p->pCareSet[w] ) // care set
939  break;
940  if ( w == p->nWords )
941  {
942  Vec_PtrPush( p->vDivs2UP0, pObj0 );
943  Vec_PtrPush( p->vDivs2UP1, Abc_ObjNot(pObj1) );
944  }
945  for ( w = 0; w < p->nWords; w++ )
946 // if ( (puData0[w] | puData1[w]) & ~puDataR[w] )
947  if ( (puData0[w] | puData1[w]) & ~puDataR[w] & p->pCareSet[w] ) // care set
948  break;
949  if ( w == p->nWords )
950  {
951  Vec_PtrPush( p->vDivs2UP0, Abc_ObjNot(pObj0) );
952  Vec_PtrPush( p->vDivs2UP1, Abc_ObjNot(pObj1) );
953  }
954  }
955 
956  if ( Vec_PtrSize(p->vDivs2UN0) < ABC_RS_DIV2_MAX )
957  {
958  // get negative unate divisors
959  for ( w = 0; w < p->nWords; w++ )
960 // if ( ~(puData0[w] & puData1[w]) & puDataR[w] )
961  if ( ~(puData0[w] & puData1[w]) & puDataR[w] & p->pCareSet[w] ) // care set
962  break;
963  if ( w == p->nWords )
964  {
965  Vec_PtrPush( p->vDivs2UN0, pObj0 );
966  Vec_PtrPush( p->vDivs2UN1, pObj1 );
967  }
968  for ( w = 0; w < p->nWords; w++ )
969 // if ( ~(~puData0[w] & puData1[w]) & puDataR[w] )
970  if ( ~(~puData0[w] & puData1[w]) & puDataR[w] & p->pCareSet[w] ) // care set
971  break;
972  if ( w == p->nWords )
973  {
974  Vec_PtrPush( p->vDivs2UN0, Abc_ObjNot(pObj0) );
975  Vec_PtrPush( p->vDivs2UN1, pObj1 );
976  }
977  for ( w = 0; w < p->nWords; w++ )
978 // if ( ~(puData0[w] & ~puData1[w]) & puDataR[w] )
979  if ( ~(puData0[w] & ~puData1[w]) & puDataR[w] & p->pCareSet[w] ) // care set
980  break;
981  if ( w == p->nWords )
982  {
983  Vec_PtrPush( p->vDivs2UN0, pObj0 );
984  Vec_PtrPush( p->vDivs2UN1, Abc_ObjNot(pObj1) );
985  }
986  for ( w = 0; w < p->nWords; w++ )
987 // if ( ~(puData0[w] | puData1[w]) & puDataR[w] )
988  if ( ~(puData0[w] | puData1[w]) & puDataR[w] & p->pCareSet[w] ) // care set
989  break;
990  if ( w == p->nWords )
991  {
992  Vec_PtrPush( p->vDivs2UN0, Abc_ObjNot(pObj0) );
993  Vec_PtrPush( p->vDivs2UN1, Abc_ObjNot(pObj1) );
994  }
995  }
996  }
997  }
998 // printf( "%d %d ", Vec_PtrSize(p->vDivs2UP0), Vec_PtrSize(p->vDivs2UN0) );
999 }
1000 
1001 
1002 
1003 /**Function*************************************************************
1004 
1005  Synopsis []
1006 
1007  Description []
1008 
1009  SideEffects []
1010 
1011  SeeAlso []
1012 
1013 ***********************************************************************/
1014 Dec_Graph_t * Abc_ManResubQuit( Abc_ManRes_t * p )
1015 {
1016  Dec_Graph_t * pGraph;
1017  unsigned * upData;
1018  int w;
1019  upData = (unsigned *)p->pRoot->pData;
1020  for ( w = 0; w < p->nWords; w++ )
1021 // if ( upData[w] )
1022  if ( upData[w] & p->pCareSet[w] ) // care set
1023  break;
1024  if ( w != p->nWords )
1025  return NULL;
1026  // get constant node graph
1027  if ( p->pRoot->fPhase )
1028  pGraph = Dec_GraphCreateConst1();
1029  else
1030  pGraph = Dec_GraphCreateConst0();
1031  return pGraph;
1032 }
1033 
1034 /**Function*************************************************************
1035 
1036  Synopsis []
1037 
1038  Description []
1039 
1040  SideEffects []
1041 
1042  SeeAlso []
1043 
1044 ***********************************************************************/
1045 Dec_Graph_t * Abc_ManResubDivs0( Abc_ManRes_t * p )
1046 {
1047  Abc_Obj_t * pObj;
1048  unsigned * puData, * puDataR;
1049  int i, w;
1050  puDataR = (unsigned *)p->pRoot->pData;
1051  Vec_PtrForEachEntryStop( Abc_Obj_t *, p->vDivs, pObj, i, p->nDivs )
1052  {
1053  puData = (unsigned *)pObj->pData;
1054  for ( w = 0; w < p->nWords; w++ )
1055 // if ( puData[w] != puDataR[w] )
1056  if ( (puData[w] ^ puDataR[w]) & p->pCareSet[w] ) // care set
1057  break;
1058  if ( w == p->nWords )
1059  return Abc_ManResubQuit0( p->pRoot, pObj );
1060  }
1061  return NULL;
1062 }
1063 
1064 /**Function*************************************************************
1065 
1066  Synopsis []
1067 
1068  Description []
1069 
1070  SideEffects []
1071 
1072  SeeAlso []
1073 
1074 ***********************************************************************/
1075 Dec_Graph_t * Abc_ManResubDivs1( Abc_ManRes_t * p, int Required )
1076 {
1077  Abc_Obj_t * pObj0, * pObj1;
1078  unsigned * puData0, * puData1, * puDataR;
1079  int i, k, w;
1080  puDataR = (unsigned *)p->pRoot->pData;
1081  // check positive unate divisors
1082  Vec_PtrForEachEntry( Abc_Obj_t *, p->vDivs1UP, pObj0, i )
1083  {
1084  puData0 = (unsigned *)pObj0->pData;
1085  Vec_PtrForEachEntryStart( Abc_Obj_t *, p->vDivs1UP, pObj1, k, i + 1 )
1086  {
1087  puData1 = (unsigned *)pObj1->pData;
1088  for ( w = 0; w < p->nWords; w++ )
1089 // if ( (puData0[w] | puData1[w]) != puDataR[w] )
1090  if ( ((puData0[w] | puData1[w]) ^ puDataR[w]) & p->pCareSet[w] ) // care set
1091  break;
1092  if ( w == p->nWords )
1093  {
1094  p->nUsedNode1Or++;
1095  return Abc_ManResubQuit1( p->pRoot, pObj0, pObj1, 1 );
1096  }
1097  }
1098  }
1099  // check negative unate divisors
1100  Vec_PtrForEachEntry( Abc_Obj_t *, p->vDivs1UN, pObj0, i )
1101  {
1102  puData0 = (unsigned *)pObj0->pData;
1103  Vec_PtrForEachEntryStart( Abc_Obj_t *, p->vDivs1UN, pObj1, k, i + 1 )
1104  {
1105  puData1 = (unsigned *)pObj1->pData;
1106  for ( w = 0; w < p->nWords; w++ )
1107 // if ( (puData0[w] & puData1[w]) != puDataR[w] )
1108  if ( ((puData0[w] & puData1[w]) ^ puDataR[w]) & p->pCareSet[w] ) // care set
1109  break;
1110  if ( w == p->nWords )
1111  {
1112  p->nUsedNode1And++;
1113  return Abc_ManResubQuit1( p->pRoot, pObj0, pObj1, 0 );
1114  }
1115  }
1116  }
1117  return NULL;
1118 }
1119 
1120 /**Function*************************************************************
1121 
1122  Synopsis []
1123 
1124  Description []
1125 
1126  SideEffects []
1127 
1128  SeeAlso []
1129 
1130 ***********************************************************************/
1131 Dec_Graph_t * Abc_ManResubDivs12( Abc_ManRes_t * p, int Required )
1132 {
1133  Abc_Obj_t * pObj0, * pObj1, * pObj2, * pObjMax, * pObjMin0 = NULL, * pObjMin1 = NULL;
1134  unsigned * puData0, * puData1, * puData2, * puDataR;
1135  int i, k, j, w, LevelMax;
1136  puDataR = (unsigned *)p->pRoot->pData;
1137  // check positive unate divisors
1138  Vec_PtrForEachEntry( Abc_Obj_t *, p->vDivs1UP, pObj0, i )
1139  {
1140  puData0 = (unsigned *)pObj0->pData;
1141  Vec_PtrForEachEntryStart( Abc_Obj_t *, p->vDivs1UP, pObj1, k, i + 1 )
1142  {
1143  puData1 = (unsigned *)pObj1->pData;
1144  Vec_PtrForEachEntryStart( Abc_Obj_t *, p->vDivs1UP, pObj2, j, k + 1 )
1145  {
1146  puData2 = (unsigned *)pObj2->pData;
1147  for ( w = 0; w < p->nWords; w++ )
1148 // if ( (puData0[w] | puData1[w] | puData2[w]) != puDataR[w] )
1149  if ( ((puData0[w] | puData1[w] | puData2[w]) ^ puDataR[w]) & p->pCareSet[w] ) // care set
1150  break;
1151  if ( w == p->nWords )
1152  {
1153  LevelMax = Abc_MaxInt( pObj0->Level, Abc_MaxInt(pObj1->Level, pObj2->Level) );
1154  assert( LevelMax <= Required - 1 );
1155 
1156  pObjMax = NULL;
1157  if ( (int)pObj0->Level == LevelMax )
1158  pObjMax = pObj0, pObjMin0 = pObj1, pObjMin1 = pObj2;
1159  if ( (int)pObj1->Level == LevelMax )
1160  {
1161  if ( pObjMax ) continue;
1162  pObjMax = pObj1, pObjMin0 = pObj0, pObjMin1 = pObj2;
1163  }
1164  if ( (int)pObj2->Level == LevelMax )
1165  {
1166  if ( pObjMax ) continue;
1167  pObjMax = pObj2, pObjMin0 = pObj0, pObjMin1 = pObj1;
1168  }
1169 
1170  p->nUsedNode2Or++;
1171  assert(pObjMin0);
1172  assert(pObjMin1);
1173  return Abc_ManResubQuit21( p->pRoot, pObjMin0, pObjMin1, pObjMax, 1 );
1174  }
1175  }
1176  }
1177  }
1178  // check negative unate divisors
1179  Vec_PtrForEachEntry( Abc_Obj_t *, p->vDivs1UN, pObj0, i )
1180  {
1181  puData0 = (unsigned *)pObj0->pData;
1182  Vec_PtrForEachEntryStart( Abc_Obj_t *, p->vDivs1UN, pObj1, k, i + 1 )
1183  {
1184  puData1 = (unsigned *)pObj1->pData;
1185  Vec_PtrForEachEntryStart( Abc_Obj_t *, p->vDivs1UN, pObj2, j, k + 1 )
1186  {
1187  puData2 = (unsigned *)pObj2->pData;
1188  for ( w = 0; w < p->nWords; w++ )
1189 // if ( (puData0[w] & puData1[w] & puData2[w]) != puDataR[w] )
1190  if ( ((puData0[w] & puData1[w] & puData2[w]) ^ puDataR[w]) & p->pCareSet[w] ) // care set
1191  break;
1192  if ( w == p->nWords )
1193  {
1194  LevelMax = Abc_MaxInt( pObj0->Level, Abc_MaxInt(pObj1->Level, pObj2->Level) );
1195  assert( LevelMax <= Required - 1 );
1196 
1197  pObjMax = NULL;
1198  if ( (int)pObj0->Level == LevelMax )
1199  pObjMax = pObj0, pObjMin0 = pObj1, pObjMin1 = pObj2;
1200  if ( (int)pObj1->Level == LevelMax )
1201  {
1202  if ( pObjMax ) continue;
1203  pObjMax = pObj1, pObjMin0 = pObj0, pObjMin1 = pObj2;
1204  }
1205  if ( (int)pObj2->Level == LevelMax )
1206  {
1207  if ( pObjMax ) continue;
1208  pObjMax = pObj2, pObjMin0 = pObj0, pObjMin1 = pObj1;
1209  }
1210 
1211  p->nUsedNode2And++;
1212  assert(pObjMin0);
1213  assert(pObjMin1);
1214  return Abc_ManResubQuit21( p->pRoot, pObjMin0, pObjMin1, pObjMax, 0 );
1215  }
1216  }
1217  }
1218  }
1219  return NULL;
1220 }
1221 
1222 /**Function*************************************************************
1223 
1224  Synopsis []
1225 
1226  Description []
1227 
1228  SideEffects []
1229 
1230  SeeAlso []
1231 
1232 ***********************************************************************/
1233 Dec_Graph_t * Abc_ManResubDivs2( Abc_ManRes_t * p, int Required )
1234 {
1235  Abc_Obj_t * pObj0, * pObj1, * pObj2;
1236  unsigned * puData0, * puData1, * puData2, * puDataR;
1237  int i, k, w;
1238  puDataR = (unsigned *)p->pRoot->pData;
1239  // check positive unate divisors
1240  Vec_PtrForEachEntry( Abc_Obj_t *, p->vDivs1UP, pObj0, i )
1241  {
1242  puData0 = (unsigned *)pObj0->pData;
1243  Vec_PtrForEachEntry( Abc_Obj_t *, p->vDivs2UP0, pObj1, k )
1244  {
1245  pObj2 = (Abc_Obj_t *)Vec_PtrEntry( p->vDivs2UP1, k );
1246 
1247  puData1 = (unsigned *)Abc_ObjRegular(pObj1)->pData;
1248  puData2 = (unsigned *)Abc_ObjRegular(pObj2)->pData;
1249  if ( Abc_ObjIsComplement(pObj1) && Abc_ObjIsComplement(pObj2) )
1250  {
1251  for ( w = 0; w < p->nWords; w++ )
1252 // if ( (puData0[w] | (puData1[w] | puData2[w])) != puDataR[w] )
1253  if ( ((puData0[w] | (puData1[w] | puData2[w])) ^ puDataR[w]) & p->pCareSet[w] ) // care set
1254  break;
1255  }
1256  else if ( Abc_ObjIsComplement(pObj1) )
1257  {
1258  for ( w = 0; w < p->nWords; w++ )
1259 // if ( (puData0[w] | (~puData1[w] & puData2[w])) != puDataR[w] )
1260  if ( ((puData0[w] | (~puData1[w] & puData2[w])) ^ puDataR[w]) & p->pCareSet[w] ) // care set
1261  break;
1262  }
1263  else if ( Abc_ObjIsComplement(pObj2) )
1264  {
1265  for ( w = 0; w < p->nWords; w++ )
1266 // if ( (puData0[w] | (puData1[w] & ~puData2[w])) != puDataR[w] )
1267  if ( ((puData0[w] | (puData1[w] & ~puData2[w])) ^ puDataR[w]) & p->pCareSet[w] ) // care set
1268  break;
1269  }
1270  else
1271  {
1272  for ( w = 0; w < p->nWords; w++ )
1273 // if ( (puData0[w] | (puData1[w] & puData2[w])) != puDataR[w] )
1274  if ( ((puData0[w] | (puData1[w] & puData2[w])) ^ puDataR[w]) & p->pCareSet[w] ) // care set
1275  break;
1276  }
1277  if ( w == p->nWords )
1278  {
1279  p->nUsedNode2OrAnd++;
1280  return Abc_ManResubQuit2( p->pRoot, pObj0, pObj1, pObj2, 1 );
1281  }
1282  }
1283  }
1284  // check negative unate divisors
1285  Vec_PtrForEachEntry( Abc_Obj_t *, p->vDivs1UN, pObj0, i )
1286  {
1287  puData0 = (unsigned *)pObj0->pData;
1288  Vec_PtrForEachEntry( Abc_Obj_t *, p->vDivs2UN0, pObj1, k )
1289  {
1290  pObj2 = (Abc_Obj_t *)Vec_PtrEntry( p->vDivs2UN1, k );
1291 
1292  puData1 = (unsigned *)Abc_ObjRegular(pObj1)->pData;
1293  puData2 = (unsigned *)Abc_ObjRegular(pObj2)->pData;
1294  if ( Abc_ObjIsComplement(pObj1) && Abc_ObjIsComplement(pObj2) )
1295  {
1296  for ( w = 0; w < p->nWords; w++ )
1297 // if ( (puData0[w] & (puData1[w] | puData2[w])) != puDataR[w] )
1298  if ( ((puData0[w] & (puData1[w] | puData2[w])) ^ puDataR[w]) & p->pCareSet[w] ) // care set
1299  break;
1300  }
1301  else if ( Abc_ObjIsComplement(pObj1) )
1302  {
1303  for ( w = 0; w < p->nWords; w++ )
1304 // if ( (puData0[w] & (~puData1[w] & puData2[w])) != puDataR[w] )
1305  if ( ((puData0[w] & (~puData1[w] & puData2[w])) ^ puDataR[w]) & p->pCareSet[w] ) // care set
1306  break;
1307  }
1308  else if ( Abc_ObjIsComplement(pObj2) )
1309  {
1310  for ( w = 0; w < p->nWords; w++ )
1311 // if ( (puData0[w] & (puData1[w] & ~puData2[w])) != puDataR[w] )
1312  if ( ((puData0[w] & (puData1[w] & ~puData2[w])) ^ puDataR[w]) & p->pCareSet[w] ) // care set
1313  break;
1314  }
1315  else
1316  {
1317  for ( w = 0; w < p->nWords; w++ )
1318 // if ( (puData0[w] & (puData1[w] & puData2[w])) != puDataR[w] )
1319  if ( ((puData0[w] & (puData1[w] & puData2[w])) ^ puDataR[w]) & p->pCareSet[w] ) // care set
1320  break;
1321  }
1322  if ( w == p->nWords )
1323  {
1324  p->nUsedNode2AndOr++;
1325  return Abc_ManResubQuit2( p->pRoot, pObj0, pObj1, pObj2, 0 );
1326  }
1327  }
1328  }
1329  return NULL;
1330 }
1331 
1332 /**Function*************************************************************
1333 
1334  Synopsis []
1335 
1336  Description []
1337 
1338  SideEffects []
1339 
1340  SeeAlso []
1341 
1342 ***********************************************************************/
1343 Dec_Graph_t * Abc_ManResubDivs3( Abc_ManRes_t * p, int Required )
1344 {
1345  Abc_Obj_t * pObj0, * pObj1, * pObj2, * pObj3;
1346  unsigned * puData0, * puData1, * puData2, * puData3, * puDataR;
1347  int i, k, w = 0, Flag;
1348  puDataR = (unsigned *)p->pRoot->pData;
1349  // check positive unate divisors
1350  Vec_PtrForEachEntry( Abc_Obj_t *, p->vDivs2UP0, pObj0, i )
1351  {
1352  pObj1 = (Abc_Obj_t *)Vec_PtrEntry( p->vDivs2UP1, i );
1353  puData0 = (unsigned *)Abc_ObjRegular(pObj0)->pData;
1354  puData1 = (unsigned *)Abc_ObjRegular(pObj1)->pData;
1355  Flag = (Abc_ObjIsComplement(pObj0) << 3) | (Abc_ObjIsComplement(pObj1) << 2);
1356 
1357  Vec_PtrForEachEntryStart( Abc_Obj_t *, p->vDivs2UP0, pObj2, k, i + 1 )
1358  {
1359  pObj3 = (Abc_Obj_t *)Vec_PtrEntry( p->vDivs2UP1, k );
1360  puData2 = (unsigned *)Abc_ObjRegular(pObj2)->pData;
1361  puData3 = (unsigned *)Abc_ObjRegular(pObj3)->pData;
1362 
1363  Flag = (Flag & 12) | ((int)Abc_ObjIsComplement(pObj2) << 1) | (int)Abc_ObjIsComplement(pObj3);
1364  assert( Flag < 16 );
1365  switch( Flag )
1366  {
1367  case 0: // 0000
1368  for ( w = 0; w < p->nWords; w++ )
1369 // if ( ((puData0[w] & puData1[w]) | (puData2[w] & puData3[w])) != puDataR[w] )
1370  if ( (((puData0[w] & puData1[w]) | (puData2[w] & puData3[w])) ^ puDataR[w]) & p->pCareSet[w] ) // care set
1371  break;
1372  break;
1373  case 1: // 0001
1374  for ( w = 0; w < p->nWords; w++ )
1375 // if ( ((puData0[w] & puData1[w]) | (puData2[w] & ~puData3[w])) != puDataR[w] )
1376  if ( (((puData0[w] & puData1[w]) | (puData2[w] & ~puData3[w])) ^ puDataR[w]) & p->pCareSet[w] ) // care set
1377  break;
1378  break;
1379  case 2: // 0010
1380  for ( w = 0; w < p->nWords; w++ )
1381 // if ( ((puData0[w] & puData1[w]) | (~puData2[w] & puData3[w])) != puDataR[w] )
1382  if ( (((puData0[w] & puData1[w]) | (~puData2[w] & puData3[w])) ^ puDataR[w]) & p->pCareSet[w] ) // care set
1383  break;
1384  break;
1385  case 3: // 0011
1386  for ( w = 0; w < p->nWords; w++ )
1387 // if ( ((puData0[w] & puData1[w]) | (puData2[w] | puData3[w])) != puDataR[w] )
1388  if ( (((puData0[w] & puData1[w]) | (puData2[w] | puData3[w])) ^ puDataR[w]) & p->pCareSet[w] ) // care set
1389  break;
1390  break;
1391 
1392  case 4: // 0100
1393  for ( w = 0; w < p->nWords; w++ )
1394 // if ( ((puData0[w] & ~puData1[w]) | (puData2[w] & puData3[w])) != puDataR[w] )
1395  if ( (((puData0[w] & ~puData1[w]) | (puData2[w] & puData3[w])) ^ puDataR[w]) & p->pCareSet[w] ) // care set
1396  break;
1397  break;
1398  case 5: // 0101
1399  for ( w = 0; w < p->nWords; w++ )
1400 // if ( ((puData0[w] & ~puData1[w]) | (puData2[w] & ~puData3[w])) != puDataR[w] )
1401  if ( (((puData0[w] & ~puData1[w]) | (puData2[w] & ~puData3[w])) ^ puDataR[w]) & p->pCareSet[w] ) // care set
1402  break;
1403  break;
1404  case 6: // 0110
1405  for ( w = 0; w < p->nWords; w++ )
1406 // if ( ((puData0[w] & ~puData1[w]) | (~puData2[w] & puData3[w])) != puDataR[w] )
1407  if ( (((puData0[w] & ~puData1[w]) | (~puData2[w] & puData3[w])) ^ puDataR[w]) & p->pCareSet[w] ) // care set
1408  break;
1409  break;
1410  case 7: // 0111
1411  for ( w = 0; w < p->nWords; w++ )
1412 // if ( ((puData0[w] & ~puData1[w]) | (puData2[w] | puData3[w])) != puDataR[w] )
1413  if ( (((puData0[w] & ~puData1[w]) | (puData2[w] | puData3[w])) ^ puDataR[w]) & p->pCareSet[w] ) // care set
1414  break;
1415  break;
1416 
1417  case 8: // 1000
1418  for ( w = 0; w < p->nWords; w++ )
1419 // if ( ((~puData0[w] & puData1[w]) | (puData2[w] & puData3[w])) != puDataR[w] )
1420  if ( (((~puData0[w] & puData1[w]) | (puData2[w] & puData3[w])) ^ puDataR[w]) & p->pCareSet[w] ) // care set
1421  break;
1422  break;
1423  case 9: // 1001
1424  for ( w = 0; w < p->nWords; w++ )
1425 // if ( ((~puData0[w] & puData1[w]) | (puData2[w] & ~puData3[w])) != puDataR[w] )
1426  if ( (((~puData0[w] & puData1[w]) | (puData2[w] & ~puData3[w])) ^ puDataR[w]) & p->pCareSet[w] ) // care set
1427  break;
1428  break;
1429  case 10: // 1010
1430  for ( w = 0; w < p->nWords; w++ )
1431 // if ( ((~puData0[w] & puData1[w]) | (~puData2[w] & puData3[w])) != puDataR[w] )
1432  if ( (((~puData0[w] & puData1[w]) | (~puData2[w] & puData3[w])) ^ puDataR[w]) & p->pCareSet[w] ) // care set
1433  break;
1434  break;
1435  case 11: // 1011
1436  for ( w = 0; w < p->nWords; w++ )
1437 // if ( ((~puData0[w] & puData1[w]) | (puData2[w] | puData3[w])) != puDataR[w] )
1438  if ( (((~puData0[w] & puData1[w]) | (puData2[w] | puData3[w])) ^ puDataR[w]) & p->pCareSet[w] ) // care set
1439  break;
1440  break;
1441 
1442  case 12: // 1100
1443  for ( w = 0; w < p->nWords; w++ )
1444 // if ( ((puData0[w] | puData1[w]) | (puData2[w] & puData3[w])) != puDataR[w] )
1445  if ( (((puData0[w] | puData1[w]) | (puData2[w] & puData3[w])) ^ puDataR[w]) & p->pCareSet[w] ) // care set
1446  break;
1447  break;
1448  case 13: // 1101
1449  for ( w = 0; w < p->nWords; w++ )
1450 // if ( ((puData0[w] | puData1[w]) | (puData2[w] & ~puData3[w])) != puDataR[w] )
1451  if ( (((puData0[w] | puData1[w]) | (puData2[w] & ~puData3[w])) ^ puDataR[w]) & p->pCareSet[w] )
1452  break;
1453  break;
1454  case 14: // 1110
1455  for ( w = 0; w < p->nWords; w++ )
1456 // if ( ((puData0[w] | puData1[w]) | (~puData2[w] & puData3[w])) != puDataR[w] )
1457  if ( (((puData0[w] | puData1[w]) | (~puData2[w] & puData3[w])) ^ puDataR[w]) & p->pCareSet[w] )
1458  break;
1459  break;
1460  case 15: // 1111
1461  for ( w = 0; w < p->nWords; w++ )
1462 // if ( ((puData0[w] | puData1[w]) | (puData2[w] | puData3[w])) != puDataR[w] )
1463  if ( (((puData0[w] | puData1[w]) | (puData2[w] | puData3[w])) ^ puDataR[w]) & p->pCareSet[w] )
1464  break;
1465  break;
1466 
1467  }
1468  if ( w == p->nWords )
1469  {
1470  p->nUsedNode3OrAnd++;
1471  return Abc_ManResubQuit3( p->pRoot, pObj0, pObj1, pObj2, pObj3, 1 );
1472  }
1473  }
1474  }
1475 /*
1476  // check negative unate divisors
1477  Vec_PtrForEachEntry( Abc_Obj_t *, p->vDivs2UN0, pObj0, i )
1478  {
1479  pObj1 = Vec_PtrEntry( p->vDivs2UN1, i );
1480  puData0 = Abc_ObjRegular(pObj0)->pData;
1481  puData1 = Abc_ObjRegular(pObj1)->pData;
1482  Flag = (Abc_ObjIsComplement(pObj0) << 3) | (Abc_ObjIsComplement(pObj1) << 2);
1483 
1484  Vec_PtrForEachEntryStart( Abc_Obj_t *, p->vDivs2UN0, pObj2, k, i + 1 )
1485  {
1486  pObj3 = Vec_PtrEntry( p->vDivs2UN1, k );
1487  puData2 = Abc_ObjRegular(pObj2)->pData;
1488  puData3 = Abc_ObjRegular(pObj3)->pData;
1489 
1490  Flag = (Flag & 12) | (Abc_ObjIsComplement(pObj2) << 1) | Abc_ObjIsComplement(pObj3);
1491  assert( Flag < 16 );
1492  switch( Flag )
1493  {
1494  case 0: // 0000
1495  for ( w = 0; w < p->nWords; w++ )
1496  if ( ((puData0[w] & puData1[w]) & (puData2[w] & puData3[w])) != puDataR[w] )
1497  break;
1498  break;
1499  case 1: // 0001
1500  for ( w = 0; w < p->nWords; w++ )
1501  if ( ((puData0[w] & puData1[w]) & (puData2[w] & ~puData3[w])) != puDataR[w] )
1502  break;
1503  break;
1504  case 2: // 0010
1505  for ( w = 0; w < p->nWords; w++ )
1506  if ( ((puData0[w] & puData1[w]) & (~puData2[w] & puData3[w])) != puDataR[w] )
1507  break;
1508  break;
1509  case 3: // 0011
1510  for ( w = 0; w < p->nWords; w++ )
1511  if ( ((puData0[w] & puData1[w]) & (puData2[w] | puData3[w])) != puDataR[w] )
1512  break;
1513  break;
1514 
1515  case 4: // 0100
1516  for ( w = 0; w < p->nWords; w++ )
1517  if ( ((puData0[w] & ~puData1[w]) & (puData2[w] & puData3[w])) != puDataR[w] )
1518  break;
1519  break;
1520  case 5: // 0101
1521  for ( w = 0; w < p->nWords; w++ )
1522  if ( ((puData0[w] & ~puData1[w]) & (puData2[w] & ~puData3[w])) != puDataR[w] )
1523  break;
1524  break;
1525  case 6: // 0110
1526  for ( w = 0; w < p->nWords; w++ )
1527  if ( ((puData0[w] & ~puData1[w]) & (~puData2[w] & puData3[w])) != puDataR[w] )
1528  break;
1529  break;
1530  case 7: // 0111
1531  for ( w = 0; w < p->nWords; w++ )
1532  if ( ((puData0[w] & ~puData1[w]) & (puData2[w] | puData3[w])) != puDataR[w] )
1533  break;
1534  break;
1535 
1536  case 8: // 1000
1537  for ( w = 0; w < p->nWords; w++ )
1538  if ( ((~puData0[w] & puData1[w]) & (puData2[w] & puData3[w])) != puDataR[w] )
1539  break;
1540  break;
1541  case 9: // 1001
1542  for ( w = 0; w < p->nWords; w++ )
1543  if ( ((~puData0[w] & puData1[w]) & (puData2[w] & ~puData3[w])) != puDataR[w] )
1544  break;
1545  break;
1546  case 10: // 1010
1547  for ( w = 0; w < p->nWords; w++ )
1548  if ( ((~puData0[w] & puData1[w]) & (~puData2[w] & puData3[w])) != puDataR[w] )
1549  break;
1550  break;
1551  case 11: // 1011
1552  for ( w = 0; w < p->nWords; w++ )
1553  if ( ((~puData0[w] & puData1[w]) & (puData2[w] | puData3[w])) != puDataR[w] )
1554  break;
1555  break;
1556 
1557  case 12: // 1100
1558  for ( w = 0; w < p->nWords; w++ )
1559  if ( ((puData0[w] | puData1[w]) & (puData2[w] & puData3[w])) != puDataR[w] )
1560  break;
1561  break;
1562  case 13: // 1101
1563  for ( w = 0; w < p->nWords; w++ )
1564  if ( ((puData0[w] | puData1[w]) & (puData2[w] & ~puData3[w])) != puDataR[w] )
1565  break;
1566  break;
1567  case 14: // 1110
1568  for ( w = 0; w < p->nWords; w++ )
1569  if ( ((puData0[w] | puData1[w]) & (~puData2[w] & puData3[w])) != puDataR[w] )
1570  break;
1571  break;
1572  case 15: // 1111
1573  for ( w = 0; w < p->nWords; w++ )
1574  if ( ((puData0[w] | puData1[w]) & (puData2[w] | puData3[w])) != puDataR[w] )
1575  break;
1576  break;
1577 
1578  }
1579  if ( w == p->nWords )
1580  {
1581  p->nUsedNode3AndOr++;
1582  return Abc_ManResubQuit3( p->pRoot, pObj0, pObj1, pObj2, pObj3, 0 );
1583  }
1584  }
1585  }
1586 */
1587  return NULL;
1588 }
1589 
1590 /**Function*************************************************************
1591 
1592  Synopsis []
1593 
1594  Description []
1595 
1596  SideEffects []
1597 
1598  SeeAlso []
1599 
1600 ***********************************************************************/
1601 void Abc_ManResubCleanup( Abc_ManRes_t * p )
1602 {
1603  Abc_Obj_t * pObj;
1604  int i;
1605  Vec_PtrForEachEntry( Abc_Obj_t *, p->vDivs, pObj, i )
1606  pObj->pData = NULL;
1607  Vec_PtrClear( p->vDivs );
1608  p->pRoot = NULL;
1609 }
1610 
1611 /**Function*************************************************************
1612 
1613  Synopsis [Evaluates resubstution of one cut.]
1614 
1615  Description [Returns the graph to add if any.]
1616 
1617  SideEffects []
1618 
1619  SeeAlso []
1620 
1621 ***********************************************************************/
1622 Dec_Graph_t * Abc_ManResubEval( Abc_ManRes_t * p, Abc_Obj_t * pRoot, Vec_Ptr_t * vLeaves, int nSteps, int fUpdateLevel, int fVerbose )
1623 {
1624  extern int Abc_NodeMffcInside( Abc_Obj_t * pNode, Vec_Ptr_t * vLeaves, Vec_Ptr_t * vInside );
1625  Dec_Graph_t * pGraph;
1626  int Required;
1627  abctime clk;
1628 
1629  Required = fUpdateLevel? Abc_ObjRequiredLevel(pRoot) : ABC_INFINITY;
1630 
1631  assert( nSteps >= 0 );
1632  assert( nSteps <= 3 );
1633  p->pRoot = pRoot;
1634  p->nLeaves = Vec_PtrSize(vLeaves);
1635  p->nLastGain = -1;
1636 
1637  // collect the MFFC
1638 clk = Abc_Clock();
1639  p->nMffc = Abc_NodeMffcInside( pRoot, vLeaves, p->vTemp );
1640 p->timeMffc += Abc_Clock() - clk;
1641  assert( p->nMffc > 0 );
1642 
1643  // collect the divisor nodes
1644 clk = Abc_Clock();
1645  if ( !Abc_ManResubCollectDivs( p, pRoot, vLeaves, Required ) )
1646  return NULL;
1647  p->timeDiv += Abc_Clock() - clk;
1648 
1649  p->nTotalDivs += p->nDivs;
1650  p->nTotalLeaves += p->nLeaves;
1651 
1652  // simulate the nodes
1653 clk = Abc_Clock();
1654  Abc_ManResubSimulate( p->vDivs, p->nLeaves, p->vSims, p->nLeavesMax, p->nWords );
1655 p->timeSim += Abc_Clock() - clk;
1656 
1657 clk = Abc_Clock();
1658  // consider constants
1659  if ( (pGraph = Abc_ManResubQuit( p )) )
1660  {
1661  p->nUsedNodeC++;
1662  p->nLastGain = p->nMffc;
1663  return pGraph;
1664  }
1665 
1666  // consider equal nodes
1667  if ( (pGraph = Abc_ManResubDivs0( p )) )
1668  {
1669 p->timeRes1 += Abc_Clock() - clk;
1670  p->nUsedNode0++;
1671  p->nLastGain = p->nMffc;
1672  return pGraph;
1673  }
1674  if ( nSteps == 0 || p->nMffc == 1 )
1675  {
1676 p->timeRes1 += Abc_Clock() - clk;
1677  return NULL;
1678  }
1679 
1680  // get the one level divisors
1681  Abc_ManResubDivsS( p, Required );
1682 
1683  // consider one node
1684  if ( (pGraph = Abc_ManResubDivs1( p, Required )) )
1685  {
1686 p->timeRes1 += Abc_Clock() - clk;
1687  p->nLastGain = p->nMffc - 1;
1688  return pGraph;
1689  }
1690 p->timeRes1 += Abc_Clock() - clk;
1691  if ( nSteps == 1 || p->nMffc == 2 )
1692  return NULL;
1693 
1694 clk = Abc_Clock();
1695  // consider triples
1696  if ( (pGraph = Abc_ManResubDivs12( p, Required )) )
1697  {
1698 p->timeRes2 += Abc_Clock() - clk;
1699  p->nLastGain = p->nMffc - 2;
1700  return pGraph;
1701  }
1702 p->timeRes2 += Abc_Clock() - clk;
1703 
1704  // get the two level divisors
1705 clk = Abc_Clock();
1706  Abc_ManResubDivsD( p, Required );
1707 p->timeResD += Abc_Clock() - clk;
1708 
1709  // consider two nodes
1710 clk = Abc_Clock();
1711  if ( (pGraph = Abc_ManResubDivs2( p, Required )) )
1712  {
1713 p->timeRes2 += Abc_Clock() - clk;
1714  p->nLastGain = p->nMffc - 2;
1715  return pGraph;
1716  }
1717 p->timeRes2 += Abc_Clock() - clk;
1718  if ( nSteps == 2 || p->nMffc == 3 )
1719  return NULL;
1720 
1721  // consider two nodes
1722 clk = Abc_Clock();
1723  if ( (pGraph = Abc_ManResubDivs3( p, Required )) )
1724  {
1725 p->timeRes3 += Abc_Clock() - clk;
1726  p->nLastGain = p->nMffc - 3;
1727  return pGraph;
1728  }
1729 p->timeRes3 += Abc_Clock() - clk;
1730  if ( nSteps == 3 || p->nLeavesMax == 4 )
1731  return NULL;
1732  return NULL;
1733 }
1734 
1735 
1736 
1737 
1738 /**Function*************************************************************
1739 
1740  Synopsis [Computes the volume and checks if the cut is feasible.]
1741 
1742  Description []
1743 
1744  SideEffects []
1745 
1746  SeeAlso []
1747 
1748 ***********************************************************************/
1749 int Abc_CutVolumeCheck_rec( Abc_Obj_t * pObj )
1750 {
1751  // quit if the node is visited (or if it is a leaf)
1752  if ( Abc_NodeIsTravIdCurrent(pObj) )
1753  return 0;
1754  Abc_NodeSetTravIdCurrent(pObj);
1755  // report the error
1756  if ( Abc_ObjIsCi(pObj) )
1757  printf( "Abc_CutVolumeCheck() ERROR: The set of nodes is not a cut!\n" );
1758  // count the number of nodes in the leaves
1759  return 1 + Abc_CutVolumeCheck_rec( Abc_ObjFanin0(pObj) ) +
1760  Abc_CutVolumeCheck_rec( Abc_ObjFanin1(pObj) );
1761 }
1762 
1763 /**Function*************************************************************
1764 
1765  Synopsis [Computes the volume and checks if the cut is feasible.]
1766 
1767  Description []
1768 
1769  SideEffects []
1770 
1771  SeeAlso []
1772 
1773 ***********************************************************************/
1774 int Abc_CutVolumeCheck( Abc_Obj_t * pNode, Vec_Ptr_t * vLeaves )
1775 {
1776  Abc_Obj_t * pObj;
1777  int i;
1778  // mark the leaves
1779  Abc_NtkIncrementTravId( pNode->pNtk );
1780  Vec_PtrForEachEntry( Abc_Obj_t *, vLeaves, pObj, i )
1781  Abc_NodeSetTravIdCurrent( pObj );
1782  // traverse the nodes starting from the given one and count them
1783  return Abc_CutVolumeCheck_rec( pNode );
1784 }
1785 
1786 /**Function*************************************************************
1787 
1788  Synopsis [Computes the factor cut of the node.]
1789 
1790  Description []
1791 
1792  SideEffects []
1793 
1794  SeeAlso []
1795 
1796 ***********************************************************************/
1797 void Abc_CutFactor_rec( Abc_Obj_t * pObj, Vec_Ptr_t * vLeaves )
1798 {
1799  if ( pObj->fMarkA )
1800  return;
1801  if ( Abc_ObjIsCi(pObj) || (Abc_ObjFanoutNum(pObj) > 1 && !Abc_NodeIsMuxControlType(pObj)) )
1802  {
1803  Vec_PtrPush( vLeaves, pObj );
1804  pObj->fMarkA = 1;
1805  return;
1806  }
1807  Abc_CutFactor_rec( Abc_ObjFanin0(pObj), vLeaves );
1808  Abc_CutFactor_rec( Abc_ObjFanin1(pObj), vLeaves );
1809 }
1810 
1811 /**Function*************************************************************
1812 
1813  Synopsis [Computes the factor cut of the node.]
1814 
1815  Description [Factor-cut is the cut at a node in terms of factor-nodes.
1816  Factor-nodes are roots of the node trees (MUXes/EXORs are counted as single nodes).
1817  Factor-cut is unique for the given node.]
1818 
1819  SideEffects []
1820 
1821  SeeAlso []
1822 
1823 ***********************************************************************/
1824 Vec_Ptr_t * Abc_CutFactor( Abc_Obj_t * pNode )
1825 {
1826  Vec_Ptr_t * vLeaves;
1827  Abc_Obj_t * pObj;
1828  int i;
1829  assert( !Abc_ObjIsCi(pNode) );
1830  vLeaves = Vec_PtrAlloc( 10 );
1831  Abc_CutFactor_rec( Abc_ObjFanin0(pNode), vLeaves );
1832  Abc_CutFactor_rec( Abc_ObjFanin1(pNode), vLeaves );
1833  Vec_PtrForEachEntry( Abc_Obj_t *, vLeaves, pObj, i )
1834  pObj->fMarkA = 0;
1835  return vLeaves;
1836 }
1837 
1838 /**Function*************************************************************
1839 
1840  Synopsis [Cut computation.]
1841 
1842  Description [This cut computation works as follows:
1843  It starts with the factor cut at the node. If the factor-cut is large, quit.
1844  It supports the set of leaves of the cut under construction and labels all nodes
1845  in the cut under construction, including the leaves.
1846  It computes the factor-cuts of the leaves and checks if it is easible to add any of them.
1847  If it is, it randomly chooses one feasible and continues.]
1848 
1849  SideEffects []
1850 
1851  SeeAlso []
1852 
1853 ***********************************************************************/
1854 Vec_Ptr_t * Abc_CutFactorLarge( Abc_Obj_t * pNode, int nLeavesMax )
1855 {
1856  Vec_Ptr_t * vLeaves, * vFactors, * vFact, * vNext;
1857  Vec_Int_t * vFeasible;
1858  Abc_Obj_t * pLeaf, * pTemp;
1859  int i, k, Counter, RandLeaf;
1860  int BestCut, BestShare;
1861  assert( Abc_ObjIsNode(pNode) );
1862  // get one factor-cut
1863  vLeaves = Abc_CutFactor( pNode );
1864  if ( Vec_PtrSize(vLeaves) > nLeavesMax )
1865  {
1866  Vec_PtrFree(vLeaves);
1867  return NULL;
1868  }
1869  if ( Vec_PtrSize(vLeaves) == nLeavesMax )
1870  return vLeaves;
1871  // initialize the factor cuts for the leaves
1872  vFactors = Vec_PtrAlloc( nLeavesMax );
1873  Abc_NtkIncrementTravId( pNode->pNtk );
1874  Vec_PtrForEachEntry( Abc_Obj_t *, vLeaves, pLeaf, i )
1875  {
1876  Abc_NodeSetTravIdCurrent( pLeaf );
1877  if ( Abc_ObjIsCi(pLeaf) )
1878  Vec_PtrPush( vFactors, NULL );
1879  else
1880  Vec_PtrPush( vFactors, Abc_CutFactor(pLeaf) );
1881  }
1882  // construct larger factor cuts
1883  vFeasible = Vec_IntAlloc( nLeavesMax );
1884  while ( 1 )
1885  {
1886  BestCut = -1, BestShare = -1;
1887  // find the next feasible cut to add
1888  Vec_IntClear( vFeasible );
1889  Vec_PtrForEachEntry( Vec_Ptr_t *, vFactors, vFact, i )
1890  {
1891  if ( vFact == NULL )
1892  continue;
1893  // count the number of unmarked leaves of this factor cut
1894  Counter = 0;
1895  Vec_PtrForEachEntry( Abc_Obj_t *, vFact, pTemp, k )
1896  Counter += !Abc_NodeIsTravIdCurrent(pTemp);
1897  // if the number of new leaves is smaller than the diff, it is feasible
1898  if ( Counter <= nLeavesMax - Vec_PtrSize(vLeaves) + 1 )
1899  {
1900  Vec_IntPush( vFeasible, i );
1901  if ( BestCut == -1 || BestShare < Vec_PtrSize(vFact) - Counter )
1902  BestCut = i, BestShare = Vec_PtrSize(vFact) - Counter;
1903  }
1904  }
1905  // quit if there is no feasible factor cuts
1906  if ( Vec_IntSize(vFeasible) == 0 )
1907  break;
1908  // randomly choose one leaf and get its factor cut
1909 // RandLeaf = Vec_IntEntry( vFeasible, rand() % Vec_IntSize(vFeasible) );
1910  // choose the cut that has most sharing with the other cuts
1911  RandLeaf = BestCut;
1912 
1913  pLeaf = (Abc_Obj_t *)Vec_PtrEntry( vLeaves, RandLeaf );
1914  vNext = (Vec_Ptr_t *)Vec_PtrEntry( vFactors, RandLeaf );
1915  // unmark this leaf
1916  Abc_NodeSetTravIdPrevious( pLeaf );
1917  // remove this cut from the leaves and factor cuts
1918  for ( i = RandLeaf; i < Vec_PtrSize(vLeaves)-1; i++ )
1919  {
1920  Vec_PtrWriteEntry( vLeaves, i, Vec_PtrEntry(vLeaves, i+1) );
1921  Vec_PtrWriteEntry( vFactors, i, Vec_PtrEntry(vFactors,i+1) );
1922  }
1923  Vec_PtrShrink( vLeaves, Vec_PtrSize(vLeaves) -1 );
1924  Vec_PtrShrink( vFactors, Vec_PtrSize(vFactors)-1 );
1925  // add new leaves, compute their factor cuts
1926  Vec_PtrForEachEntry( Abc_Obj_t *, vNext, pLeaf, i )
1927  {
1928  if ( Abc_NodeIsTravIdCurrent(pLeaf) )
1929  continue;
1930  Abc_NodeSetTravIdCurrent( pLeaf );
1931  Vec_PtrPush( vLeaves, pLeaf );
1932  if ( Abc_ObjIsCi(pLeaf) )
1933  Vec_PtrPush( vFactors, NULL );
1934  else
1935  Vec_PtrPush( vFactors, Abc_CutFactor(pLeaf) );
1936  }
1937  Vec_PtrFree( vNext );
1938  assert( Vec_PtrSize(vLeaves) <= nLeavesMax );
1939  if ( Vec_PtrSize(vLeaves) == nLeavesMax )
1940  break;
1941  }
1942 
1943  // remove temporary storage
1944  Vec_PtrForEachEntry( Vec_Ptr_t *, vFactors, vFact, i )
1945  if ( vFact ) Vec_PtrFree( vFact );
1946  Vec_PtrFree( vFactors );
1947  Vec_IntFree( vFeasible );
1948  return vLeaves;
1949 }
1950 
1951 ////////////////////////////////////////////////////////////////////////
1952 /// END OF FILE ///
1953 ////////////////////////////////////////////////////////////////////////
1954 
1955 
1956 ABC_NAMESPACE_IMPL_END
1957 
memset
char * memset()
Abc_ManRes_t_::vDivs1UP
Vec_Ptr_t * vDivs1UP
Definition: abcResub.c:55
Abc_ManRes_t_::nBits
int nBits
Definition: abcResub.c:48
Abc_ManRes_t_::nUsedNodeC
int nUsedNodeC
Definition: abcResub.c:78
Abc_ManRes_t_
Definition: abcResub.c:35
Abc_NtkIsStrash
static int Abc_NtkIsStrash(Abc_Ntk_t *pNtk)
Definition: abc.h:251
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:724
Vec_Ptr_t
typedefABC_NAMESPACE_HEADER_START struct Vec_Ptr_t_ Vec_Ptr_t
INCLUDES ///.
Definition: vecPtr.h:42
Abc_ManResubPrintDivs
static void Abc_ManResubPrintDivs(Abc_ManRes_t *p, Abc_Obj_t *pRoot, Vec_Ptr_t *vLeaves)
Definition: abcResub.c:518
Abc_ObjFanin1
static Abc_Obj_t * Abc_ObjFanin1(Abc_Obj_t *pObj)
Definition: abc.h:374
Abc_ObjIsCi
static int Abc_ObjIsCi(Abc_Obj_t *pObj)
Definition: abc.h:351
Abc_Obj_t_::fMarkA
unsigned fMarkA
Definition: abc.h:134
Abc_ManRes_t_::nUsedNode2Or
int nUsedNode2Or
Definition: abcResub.c:82
Abc_ManRes_t_::vDivs2UP0
Vec_Ptr_t * vDivs2UP0
Definition: abcResub.c:58
Abc_NtkDontCareCompute
ABC_DLL int Abc_NtkDontCareCompute(Odc_Man_t *p, Abc_Obj_t *pNode, Vec_Ptr_t *vLeaves, unsigned *puTruth)
Definition: abcOdc.c:1033
Abc_NodeMffcInside
int Abc_NodeMffcInside(Abc_Obj_t *pNode, Vec_Ptr_t *vLeaves, Vec_Ptr_t *vInside)
Definition: abcRefs.c:351
Vec_PtrForEachEntryStart
#define Vec_PtrForEachEntryStart(Type, vVec, pEntry, i, Start)
Definition: vecPtr.h:57
Abc_ManRes_t_::nUsedNodeTotal
int nUsedNodeTotal
Definition: abcResub.c:88
Abc_NtkObjNumMax
static int Abc_NtkObjNumMax(Abc_Ntk_t *pNtk)
Definition: abc.h:284
s_ResubTime
abctime s_ResubTime
Definition: abcPrint.c:46
Abc_NtkResubstitute
int Abc_NtkResubstitute(Abc_Ntk_t *pNtk, int nCutMax, int nStepsMax, int nLevelsOdc, int fUpdateLevel, int fVerbose, int fVeryVerbose)
FUNCTION DEFINITIONS ///.
Definition: abcResub.c:137
p
static Llb_Mgr_t * p
Definition: llb3Image.c:950
Abc_ObjFaninC1
static int Abc_ObjFaninC1(Abc_Obj_t *pObj)
Definition: abc.h:378
Vec_Int_t
typedefABC_NAMESPACE_IMPL_START struct Vec_Int_t_ Vec_Int_t
DECLARATIONS ///.
Definition: bblif.c:37
ABC_RS_DIV2_MAX
#define ABC_RS_DIV2_MAX
Definition: abcResub.c:32
Abc_NtkDontCareAlloc
ABC_DLL Odc_Man_t * Abc_NtkDontCareAlloc(int nVarsMax, int nLevels, int fVerbose, int fVeryVerbose)
FUNCTION DEFINITIONS ///.
Definition: abcOdc.c:162
Abc_ManResubEval
static Dec_Graph_t * Abc_ManResubEval(Abc_ManRes_t *p, Abc_Obj_t *pRoot, Vec_Ptr_t *vLeaves, int nSteps, int fUpdateLevel, int fVerbose)
Definition: abcResub.c:1622
Abc_Ntk_t_
Definition: abc.h:153
Abc_ObjFanoutNum
static int Abc_ObjFanoutNum(Abc_Obj_t *pObj)
Definition: abc.h:365
Abc_ManRes_t_::nMffc
int nMffc
Definition: abcResub.c:44
Abc_ManResubStart
static Abc_ManRes_t * Abc_ManResubStart(int nLeavesMax, int nDivsMax)
Definition: abcResub.c:287
Abc_ManResubDivs3
static Dec_Graph_t * Abc_ManResubDivs3(Abc_ManRes_t *p, int Required)
Definition: abcResub.c:1343
Abc_ManRes_t_::nUsedNode3OrAnd
int nUsedNode3OrAnd
Definition: abcResub.c:86
Abc_NodeSetTravIdPrevious
static void Abc_NodeSetTravIdPrevious(Abc_Obj_t *p)
Definition: abc.h:410
Abc_ManResubQuit0
Dec_Graph_t * Abc_ManResubQuit0(Abc_Obj_t *pRoot, Abc_Obj_t *pObj)
Definition: abcResub.c:625
Abc_InfoFill
static void Abc_InfoFill(unsigned *p, int nWords)
Definition: abc.h:237
Abc_ManResubDivs1
static Dec_Graph_t * Abc_ManResubDivs1(Abc_ManRes_t *p, int Required)
Definition: abcResub.c:1075
Dec_EdgeCreate
static Dec_Edge_t Dec_EdgeCreate(int Node, int fCompl)
FUNCTION DEFINITIONS ///.
Definition: dec.h:134
Abc_ManRes_t_::timeMffc
abctime timeMffc
Definition: abcResub.c:69
Dec_GraphUpdateNetwork
void Dec_GraphUpdateNetwork(Abc_Obj_t *pRoot, Dec_Graph_t *pGraph, int fUpdateLevel, int nGain)
Definition: decAbc.c:240
Abc_NtkLatchNum
static int Abc_NtkLatchNum(Abc_Ntk_t *pNtk)
Definition: abc.h:294
Abc_ManRes_t_::nUsedNode2AndOr
int nUsedNode2AndOr
Definition: abcResub.c:85
Abc_ObjFaninC0
static int Abc_ObjFaninC0(Abc_Obj_t *pObj)
Definition: abc.h:377
Abc_ManResubDivsD
static void Abc_ManResubDivsD(Abc_ManRes_t *p, int Required)
Definition: abcResub.c:892
Abc_ManRes_t_::nNodesBeg
int nNodesBeg
Definition: abcResub.c:92
Vec_PtrPush
static void Vec_PtrPush(Vec_Ptr_t *p, void *Entry)
Definition: vecPtr.h:606
Abc_CutFactor
Vec_Ptr_t * Abc_CutFactor(Abc_Obj_t *pNode)
Definition: abcResub.c:1824
ABC_RS_DIV1_MAX
#define ABC_RS_DIV1_MAX
DECLARATIONS ///.
Definition: abcResub.c:31
ABC_ALLOC
#define ABC_ALLOC(type, num)
Definition: abc_global.h:229
Abc_ManResubDivs2
static Dec_Graph_t * Abc_ManResubDivs2(Abc_ManRes_t *p, int Required)
Definition: abcResub.c:1233
Dec_Edge_t
typedefABC_NAMESPACE_HEADER_START struct Dec_Edge_t_ Dec_Edge_t
INCLUDES ///.
Definition: dec.h:42
Abc_ManRes_t_::nUsedNode1Or
int nUsedNode1Or
Definition: abcResub.c:80
Abc_ManResubCleanup
static void Abc_ManResubCleanup(Abc_ManRes_t *p)
Definition: abcResub.c:1601
Abc_NtkCheck
ABC_DLL int Abc_NtkCheck(Abc_Ntk_t *pNtk)
FUNCTION DEFINITIONS ///.
Definition: abcCheck.c:61
Abc_ManRes_t_::nUsedNode2And
int nUsedNode2And
Definition: abcResub.c:83
Abc_ManRes_t_::nWords
int nWords
Definition: abcResub.c:49
Abc_Clock
static abctime Abc_Clock()
Definition: abc_global.h:279
Abc_ManRes_t_::timeRes1
abctime timeRes1
Definition: abcResub.c:71
Abc_MaxInt
static int Abc_MaxInt(int a, int b)
Definition: abc_global.h:238
Abc_ManRes_t_::timeTotal
abctime timeTotal
Definition: abcResub.c:76
Vec_PtrSize
static int Vec_PtrSize(Vec_Ptr_t *p)
Definition: vecPtr.h:295
Abc_ManRes_t_::vDivs2UP1
Vec_Ptr_t * vDivs2UP1
Definition: abcResub.c:59
Abc_ManRes_t_::vSims
Vec_Ptr_t * vSims
Definition: abcResub.c:50
nWords
int nWords
Definition: abcNpn.c:127
Abc_ObjFanin0
static Abc_Obj_t * Abc_ObjFanin0(Abc_Obj_t *pObj)
Definition: abc.h:373
for
for(p=first;p->value< newval;p=p->next)
Abc_Aig_t_
DECLARATIONS ///.
Definition: abcAig.c:52
Dec_GraphCreateConst1
static Dec_Graph_t * Dec_GraphCreateConst1()
Definition: dec.h:266
Abc_CutFactorLarge
static Vec_Ptr_t * Abc_CutFactorLarge(Abc_Obj_t *pNode, int nLeavesMax)
Definition: abcResub.c:1854
Abc_NtkStopReverseLevels
ABC_DLL void Abc_NtkStopReverseLevels(Abc_Ntk_t *pNtk)
Definition: abcTiming.c:1190
Abc_Obj_t_::Level
unsigned Level
Definition: abc.h:142
Abc_ObjIsCo
static int Abc_ObjIsCo(Abc_Obj_t *pObj)
Definition: abc.h:352
Abc_NodeIsMuxControlType
ABC_DLL int Abc_NodeIsMuxControlType(Abc_Obj_t *pNode)
Definition: abcUtil.c:1357
Dec_GraphAddNodeAnd
static Dec_Edge_t Dec_GraphAddNodeAnd(Dec_Graph_t *pGraph, Dec_Edge_t eEdge0, Dec_Edge_t eEdge1)
Definition: dec.h:591
Abc_NodeFindCut
ABC_DLL Vec_Ptr_t * Abc_NodeFindCut(Abc_ManCut_t *p, Abc_Obj_t *pRoot, int fContain)
Definition: abcReconv.c:253
Abc_ManRes_t_::nUsedNode0
int nUsedNode0
Definition: abcResub.c:79
Abc_NtkReassignIds
ABC_DLL void Abc_NtkReassignIds(Abc_Ntk_t *pNtk)
Definition: abcUtil.c:1769
Abc_ManRes_t_::pRoot
Abc_Obj_t * pRoot
Definition: abcResub.c:41
Abc_Obj_t_
Definition: abc.h:128
Abc_ManRes_t_::timeTruth
abctime timeTruth
Definition: abcResub.c:66
Abc_Ntk_t_::pManFunc
void * pManFunc
Definition: abc.h:191
Abc_ObjIsNode
static int Abc_ObjIsNode(Abc_Obj_t *pObj)
Definition: abc.h:355
Abc_NtkNodeNum
static int Abc_NtkNodeNum(Abc_Ntk_t *pNtk)
Definition: abc.h:293
ProgressBarStruct
DECLARATIONS ///.
Definition: extraUtilProgress.c:32
Vec_IntAlloc
static Vec_Int_t * Vec_IntAlloc(int nCap)
FUNCTION DEFINITIONS ///.
Definition: bblif.c:149
Abc_ManRes_t_::timeRes3
abctime timeRes3
Definition: abcResub.c:74
Abc_ObjRequiredLevel
ABC_DLL int Abc_ObjRequiredLevel(Abc_Obj_t *pObj)
Definition: abcTiming.c:1102
Vec_PtrEntryLast
static void * Vec_PtrEntryLast(Vec_Ptr_t *p)
Definition: vecPtr.h:413
Abc_AigCleanup
ABC_DLL int Abc_AigCleanup(Abc_Aig_t *pMan)
Definition: abcAig.c:194
Abc_ManResubStop
static void Abc_ManResubStop(Abc_ManRes_t *p)
Definition: abcResub.c:340
Abc_CutVolumeCheck
static int Abc_CutVolumeCheck(Abc_Obj_t *pNode, Vec_Ptr_t *vLeaves)
Definition: abcResub.c:1774
Dec_Graph_t_
Definition: dec.h:69
Abc_ManRes_t_::timeDiv
abctime timeDiv
Definition: abcResub.c:68
Abc_ManResubDivsS
static void Abc_ManResubDivsS(Abc_ManRes_t *p, int Required)
Definition: abcResub.c:841
Dec_GraphCreateConst0
static Dec_Graph_t * Dec_GraphCreateConst0()
Definition: dec.h:245
ABC_NAMESPACE_IMPL_END
#define ABC_NAMESPACE_IMPL_END
Definition: abc_global.h:108
Abc_NtkDontCareFree
ABC_DLL void Abc_NtkDontCareFree(Odc_Man_t *p)
Definition: abcOdc.c:274
Abc_ManRes_t_::nLeavesMax
int nLeavesMax
Definition: abcResub.c:38
if
if(last==0)
Definition: sparse_int.h:34
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:770
Abc_ManRes_t_::nTotalDivs
int nTotalDivs
Definition: abcResub.c:89
Vec_IntPush
static void Vec_IntPush(Vec_Int_t *p, int Entry)
Definition: bblif.c:468
Abc_ManRes_t_::timeCut
abctime timeCut
Definition: abcResub.c:65
Counter
static int Counter
Definition: extraBddMisc.c:1877
Abc_NtkDontCareClear
ABC_DLL void Abc_NtkDontCareClear(Odc_Man_t *p)
Definition: abcOdc.c:242
Abc_NtkForEachLatch
#define Abc_NtkForEachLatch(pNtk, pObj, i)
Definition: abc.h:497
Abc_NtkStartReverseLevels
ABC_DLL void Abc_NtkStartReverseLevels(Abc_Ntk_t *pNtk, int nMaxLevelIncrease)
Definition: abcTiming.c:1162
Extra_ProgressBarStop
void Extra_ProgressBarStop(ProgressBar *p)
Definition: extraUtilProgress.c:118
Abc_ManResubCollectDivs_rec
void Abc_ManResubCollectDivs_rec(Abc_Obj_t *pNode, Vec_Ptr_t *vInternal)
Definition: abcResub.c:408
Abc_ManResubQuit
static Dec_Graph_t * Abc_ManResubQuit(Abc_ManRes_t *p)
Definition: abcResub.c:1014
Vec_PtrWriteEntry
static void Vec_PtrWriteEntry(Vec_Ptr_t *p, int i, void *Entry)
Definition: vecPtr.h:396
Abc_NtkForEachNode
#define Abc_NtkForEachNode(pNtk, pNode, i)
Definition: abc.h:461
Abc_NodeIsPersistant
static int Abc_NodeIsPersistant(Abc_Obj_t *pNode)
Definition: abc.h:401
Dec_GraphSetRoot
static void Dec_GraphSetRoot(Dec_Graph_t *pGraph, Dec_Edge_t eRoot)
Definition: dec.h:551
Abc_ManRes_t_::timeResD
abctime timeResD
Definition: abcResub.c:72
Abc_ManRes_t_::vDivs2UN1
Vec_Ptr_t * vDivs2UN1
Definition: abcResub.c:61
Abc_ManRes_t_::nLeaves
int nLeaves
Definition: abcResub.c:42
Abc_CutVolumeCheck_rec
int Abc_CutVolumeCheck_rec(Abc_Obj_t *pObj)
Definition: abcResub.c:1749
ABC_NAMESPACE_IMPL_START
#define ABC_NAMESPACE_IMPL_START
Definition: abc_global.h:107
Abc_ManRes_t_::vDivs
Vec_Ptr_t * vDivs
Definition: abcResub.c:46
Vec_PtrEntry
static void * Vec_PtrEntry(Vec_Ptr_t *p, int i)
Definition: vecPtr.h:362
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:682
Abc_ManRes_t_::nUsedNode1And
int nUsedNode1And
Definition: abcResub.c:81
Abc_ManRes_t_::nUsedNode2OrAnd
int nUsedNode2OrAnd
Definition: abcResub.c:84
Dec_GraphCreate
static Dec_Graph_t * Dec_GraphCreate(int nLeaves)
Definition: dec.h:221
Dec_Node_t_::pFunc
void * pFunc
Definition: dec.h:56
Dec_GraphAddNodeOr
static Dec_Edge_t Dec_GraphAddNodeOr(Dec_Graph_t *pGraph, Dec_Edge_t eEdge0, Dec_Edge_t eEdge1)
Definition: dec.h:615
Abc_NodeIsTravIdCurrent
static int Abc_NodeIsTravIdCurrent(Abc_Obj_t *p)
Definition: abc.h:411
Abc_ObjRegular
static Abc_Obj_t * Abc_ObjRegular(Abc_Obj_t *p)
Definition: abc.h:323
Abc_Obj_t_::pNtk
Abc_Ntk_t * pNtk
Definition: abc.h:130
Vec_IntSize
static int Vec_IntSize(Vec_Int_t *p)
Definition: bblif.c:252
Vec_PtrForEachEntryStop
#define Vec_PtrForEachEntryStop(Type, vVec, pEntry, i, Stop)
Definition: vecPtr.h:59
Abc_ObjForEachFanout
#define Abc_ObjForEachFanout(pObj, pFanout, i)
Definition: abc.h:526
Abc_ManRes_t_::nTotalLeaves
int nTotalLeaves
Definition: abcResub.c:90
Vec_PtrAlloc
static Vec_Ptr_t * Vec_PtrAlloc(int nCap)
FUNCTION DEFINITIONS ///.
Definition: vecPtr.h:83
Abc_ManResubDivs12
static Dec_Graph_t * Abc_ManResubDivs12(Abc_ManRes_t *p, int Required)
Definition: abcResub.c:1131
ABC_FREE
#define ABC_FREE(obj)
Definition: abc_global.h:232
Abc_Obj_t_::Id
int Id
Definition: abc.h:132
ABC_PRT
#define ABC_PRT(a, t)
Definition: abc_global.h:220
Abc_ManRes_t_::timeSim
abctime timeSim
Definition: abcResub.c:70
Abc_ManRes_t_::nNodesEnd
int nNodesEnd
Definition: abcResub.c:93
Abc_NtkIncrementTravId
static void Abc_NtkIncrementTravId(Abc_Ntk_t *p)
Definition: abc.h:406
Abc_ManResubCollectDivs
static int Abc_ManResubCollectDivs(Abc_ManRes_t *p, Abc_Obj_t *pRoot, Vec_Ptr_t *vLeaves, int Required)
Definition: abcResub.c:433
Abc_ManRes_t_::nDivsMax
int nDivsMax
Definition: abcResub.c:39
Extra_ProgressBarStart
ProgressBar * Extra_ProgressBarStart(FILE *pFile, int nItemsTotal)
FUNCTION DEFINITIONS ///.
Definition: extraUtilProgress.c:62
Abc_ManRes_t_::vDivs2UN0
Vec_Ptr_t * vDivs2UN0
Definition: abcResub.c:60
Abc_ManRes_t_::pCareSet
unsigned * pCareSet
Definition: abcResub.c:53
Abc_ManRes_t_::timeRes2
abctime timeRes2
Definition: abcResub.c:73
Abc_ManRes_t_::nLastGain
int nLastGain
Definition: abcResub.c:45
Abc_NtkManCutStart
ABC_DLL Abc_ManCut_t * Abc_NtkManCutStart(int nNodeSizeMax, int nConeSizeMax, int nNodeFanStop, int nConeFanStop)
Definition: abcReconv.c:588
Abc_ManRes_t_::vTemp
Vec_Ptr_t * vTemp
Definition: abcResub.c:63
Abc_ManRes_t_::vDivs1B
Vec_Ptr_t * vDivs1B
Definition: abcResub.c:57
Dec_GraphFree
static void Dec_GraphFree(Dec_Graph_t *pGraph)
Definition: dec.h:307
ABC_INFINITY
#define ABC_INFINITY
MACRO DEFINITIONS ///.
Definition: abc_global.h:216
Abc_CutFactor_rec
void Abc_CutFactor_rec(Abc_Obj_t *pObj, Vec_Ptr_t *vLeaves)
Definition: abcResub.c:1797
Abc_ManRes_t_::timeNtk
abctime timeNtk
Definition: abcResub.c:75
Abc_Obj_t_::pNext
Abc_Obj_t * pNext
Definition: abc.h:131
assert
#define assert(ex)
Definition: util_old.h:213
Extra_ProgressBarUpdate
static void Extra_ProgressBarUpdate(ProgressBar *p, int nItemsCur, char *pString)
Definition: extra.h:243
Vec_PtrClear
static void Vec_PtrClear(Vec_Ptr_t *p)
Definition: vecPtr.h:545
Abc_ManRes_t_::vDivs1UN
Vec_Ptr_t * vDivs1UN
Definition: abcResub.c:56
Abc_NtkManCutStop
ABC_DLL void Abc_NtkManCutStop(Abc_ManCut_t *p)
Definition: abcReconv.c:616
Abc_ManRes_t_::nTotalGain
int nTotalGain
Definition: abcResub.c:91
Dec_GraphNode
static Dec_Node_t * Dec_GraphNode(Dec_Graph_t *pGraph, int i)
Definition: dec.h:437
Odc_Man_t_
Definition: abcOdc.c:45
Abc_ObjNot
static Abc_Obj_t * Abc_ObjNot(Abc_Obj_t *p)
Definition: abc.h:324
Abc_ManRes_t_::timeRes
abctime timeRes
Definition: abcResub.c:67
Abc_Obj_t_::pData
void * pData
Definition: abc.h:145
Abc_ManResubPrint
static void Abc_ManResubPrint(Abc_ManRes_t *p)
Definition: abcResub.c:367
Abc_ManResubSimulate
static void Abc_ManResubSimulate(Vec_Ptr_t *vDivs, int nLeaves, Vec_Ptr_t *vSims, int nLeavesMax, int nWords)
Definition: abcResub.c:568
Abc_ManRes_t_::pInfo
unsigned * pInfo
Definition: abcResub.c:51
Vec_IntFree
static void Vec_IntFree(Vec_Int_t *p)
Definition: bblif.c:235
Vec_PtrForEachEntry
#define Vec_PtrForEachEntry(Type, vVec, pEntry, i)
MACRO DEFINITIONS ///.
Definition: vecPtr.h:55
Abc_ObjIsComplement
static int Abc_ObjIsComplement(Abc_Obj_t *p)
Definition: abc.h:322
Vec_IntClear
static void Vec_IntClear(Vec_Int_t *p)
Definition: bblif.c:452
abctime
ABC_INT64_T abctime
Definition: abc_global.h:278
Vec_PtrShrink
static void Vec_PtrShrink(Vec_Ptr_t *p, int nSizeNew)
Definition: vecPtr.h:528
Abc_NtkForEachObj
#define Abc_NtkForEachObj(pNtk, pObj, i)
ITERATORS ///.
Definition: abc.h:446
Abc_NtkLevel
ABC_DLL int Abc_NtkLevel(Abc_Ntk_t *pNtk)
Definition: abcDfs.c:1265
Abc_ManResubQuit1
Dec_Graph_t * Abc_ManResubQuit1(Abc_Obj_t *pRoot, Abc_Obj_t *pObj0, Abc_Obj_t *pObj1, int fOrGate)
Definition: abcResub.c:649
Abc_Obj_t_::fPhase
unsigned fPhase
Definition: abc.h:137
Abc_ManRes_t_::nUsedNode3AndOr
int nUsedNode3AndOr
Definition: abcResub.c:87
Abc_ManResubDivs0
static Dec_Graph_t * Abc_ManResubDivs0(Abc_ManRes_t *p)
Definition: abcResub.c:1045
Abc_ManCut_t_
DECLARATIONS ///.
Definition: abcReconv.c:31
Abc_ManRes_t_::nDivs
int nDivs
Definition: abcResub.c:43
Abc_NodeSetTravIdCurrent
static void Abc_NodeSetTravIdCurrent(Abc_Obj_t *p)
Definition: abc.h:409
Vec_PtrFree
static void Vec_PtrFree(Vec_Ptr_t *p)
Definition: vecPtr.h:223
Dec_GraphComplement
static void Dec_GraphComplement(Dec_Graph_t *pGraph)
Definition: dec.h:388