abc-master
 All Data Structures Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros
mfsResub.c
Go to the documentation of this file.
1 /**CFile****************************************************************
2 
3  FileName [mfsResub.c]
4 
5  SystemName [ABC: Logic synthesis and verification system.]
6 
7  PackageName [The good old minimization with complete don't-cares.]
8 
9  Synopsis [Procedures to perform resubstitution.]
10 
11  Author [Alan Mishchenko]
12 
13  Affiliation [UC Berkeley]
14 
15  Date [Ver. 1.0. Started - June 20, 2005.]
16 
17  Revision [$Id: mfsResub.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
18 
19 ***********************************************************************/
20 
21 #include "mfsInt.h"
22 
23 ABC_NAMESPACE_IMPL_START
24 
25 
26 ////////////////////////////////////////////////////////////////////////
27 /// DECLARATIONS ///
28 ////////////////////////////////////////////////////////////////////////
29 
30 ////////////////////////////////////////////////////////////////////////
31 /// FUNCTION DEFINITIONS ///
32 ////////////////////////////////////////////////////////////////////////
33 
34 /**Function*************************************************************
35 
36  Synopsis [Updates the network after resubstitution.]
37 
38  Description []
39 
40  SideEffects []
41 
42  SeeAlso []
43 
44 ***********************************************************************/
45 void Abc_NtkMfsUpdateNetwork( Mfs_Man_t * p, Abc_Obj_t * pObj, Vec_Ptr_t * vMfsFanins, Hop_Obj_t * pFunc )
46 {
47  Abc_Obj_t * pObjNew, * pFanin;
48  int k;
49  // create the new node
50  pObjNew = Abc_NtkCreateNode( pObj->pNtk );
51  pObjNew->pData = pFunc;
52  Vec_PtrForEachEntry( Abc_Obj_t *, vMfsFanins, pFanin, k )
53  Abc_ObjAddFanin( pObjNew, pFanin );
54  // replace the old node by the new node
55 //printf( "Replacing node " ); Abc_ObjPrint( stdout, pObj );
56 //printf( "Inserting node " ); Abc_ObjPrint( stdout, pObjNew );
57  // update the level of the node
58  Abc_NtkUpdate( pObj, pObjNew, p->vLevels );
59 }
60 
61 /**Function*************************************************************
62 
63  Synopsis [Prints resub candidate stats.]
64 
65  Description []
66 
67  SideEffects []
68 
69  SeeAlso []
70 
71 ***********************************************************************/
72 void Abc_NtkMfsPrintResubStats( Mfs_Man_t * p )
73 {
74  Abc_Obj_t * pFanin, * pNode;
75  int i, k, nAreaCrits = 0, nAreaExpanse = 0;
76  int nFaninMax = Abc_NtkGetFaninMax(p->pNtk);
77  Abc_NtkForEachNode( p->pNtk, pNode, i )
78  Abc_ObjForEachFanin( pNode, pFanin, k )
79  {
80  if ( !Abc_ObjIsCi(pFanin) && Abc_ObjFanoutNum(pFanin) == 1 )
81  {
82  nAreaCrits++;
83  nAreaExpanse += (int)(Abc_ObjFaninNum(pNode) < nFaninMax);
84  }
85  }
86 // printf( "Total area-critical fanins = %d. Belonging to expandable nodes = %d.\n",
87 // nAreaCrits, nAreaExpanse );
88 }
89 
90 /**Function*************************************************************
91 
92  Synopsis [Tries resubstitution.]
93 
94  Description [Returns 1 if it is feasible, or 0 if c-ex is found.]
95 
96  SideEffects []
97 
98  SeeAlso []
99 
100 ***********************************************************************/
101 int Abc_NtkMfsTryResubOnce( Mfs_Man_t * p, int * pCands, int nCands )
102 {
103  int fVeryVerbose = 0;
104  unsigned * pData;
105  int RetValue, RetValue2 = -1, iVar, i;//, clk = Abc_Clock();
106 /*
107  if ( p->pPars->fGiaSat )
108  {
109  RetValue2 = Abc_NtkMfsTryResubOnceGia( p, pCands, nCands );
110 p->timeGia += Abc_Clock() - clk;
111  return RetValue2;
112  }
113 */
114  p->nSatCalls++;
115  RetValue = sat_solver_solve( p->pSat, pCands, pCands + nCands, (ABC_INT64_T)p->pPars->nBTLimit, (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0 );
116 // assert( RetValue == l_False || RetValue == l_True );
117 
118  if ( RetValue != l_Undef && RetValue2 != -1 )
119  {
120  assert( (RetValue == l_False) == (RetValue2 == 1) );
121  }
122 
123  if ( RetValue == l_False )
124  {
125  if ( fVeryVerbose )
126  printf( "U " );
127  return 1;
128  }
129  if ( RetValue != l_True )
130  {
131  if ( fVeryVerbose )
132  printf( "T " );
133  p->nTimeOuts++;
134  return -1;
135  }
136  if ( fVeryVerbose )
137  printf( "S " );
138  p->nSatCexes++;
139  // store the counter-example
140  Vec_IntForEachEntry( p->vProjVarsSat, iVar, i )
141  {
142  pData = (unsigned *)Vec_PtrEntry( p->vDivCexes, i );
143  if ( !sat_solver_var_value( p->pSat, iVar ) ) // remove 0s!!!
144  {
145  assert( Abc_InfoHasBit(pData, p->nCexes) );
146  Abc_InfoXorBit( pData, p->nCexes );
147  }
148  }
149  p->nCexes++;
150  return 0;
151 
152 }
153 
154 /**Function*************************************************************
155 
156  Synopsis [Performs resubstitution for the node.]
157 
158  Description []
159 
160  SideEffects []
161 
162  SeeAlso []
163 
164 ***********************************************************************/
165 int Abc_NtkMfsSolveSatResub( Mfs_Man_t * p, Abc_Obj_t * pNode, int iFanin, int fOnlyRemove, int fSkipUpdate )
166 {
167  int fVeryVerbose = 0;//p->pPars->fVeryVerbose && Vec_PtrSize(p->vDivs) < 200;// || pNode->Id == 556;
168  unsigned * pData;
169  int pCands[MFS_FANIN_MAX];
170  int RetValue, iVar, i, nCands, nWords, w;
171  abctime clk;
172  Abc_Obj_t * pFanin;
173  Hop_Obj_t * pFunc;
174  assert( iFanin >= 0 );
175  p->nTryRemoves++;
176 
177  // clean simulation info
178  Vec_PtrFillSimInfo( p->vDivCexes, 0, p->nDivWords );
179  p->nCexes = 0;
180  if ( p->pPars->fVeryVerbose )
181  {
182 // printf( "\n" );
183  printf( "%5d : Lev =%3d. Leaf =%3d. Node =%3d. Divs =%3d. Fanin = %4d (%d/%d), MFFC = %d\n",
184  pNode->Id, pNode->Level, Vec_PtrSize(p->vSupp), Vec_PtrSize(p->vNodes), Vec_PtrSize(p->vDivs)-Abc_ObjFaninNum(pNode),
185  Abc_ObjFaninId(pNode, iFanin), iFanin, Abc_ObjFaninNum(pNode),
186  Abc_ObjFanoutNum(Abc_ObjFanin(pNode, iFanin)) == 1 ? Abc_NodeMffcLabel(Abc_ObjFanin(pNode, iFanin)) : 0 );
187  }
188 
189  // try fanins without the critical fanin
190  nCands = 0;
191  Vec_PtrClear( p->vMfsFanins );
192  Abc_ObjForEachFanin( pNode, pFanin, i )
193  {
194  if ( i == iFanin )
195  continue;
196  Vec_PtrPush( p->vMfsFanins, pFanin );
197  iVar = Vec_PtrSize(p->vDivs) - Abc_ObjFaninNum(pNode) + i;
198  pCands[nCands++] = toLitCond( Vec_IntEntry( p->vProjVarsSat, iVar ), 1 );
199  }
200  RetValue = Abc_NtkMfsTryResubOnce( p, pCands, nCands );
201  if ( RetValue == -1 )
202  return 0;
203  if ( RetValue == 1 )
204  {
205  if ( p->pPars->fVeryVerbose )
206  printf( "Node %d: Fanin %d can be removed.\n", pNode->Id, iFanin );
207  p->nNodesResub++;
208  p->nNodesGainedLevel++;
209  if ( fSkipUpdate )
210  return 1;
211 clk = Abc_Clock();
212  // derive the function
213  pFunc = Abc_NtkMfsInterplate( p, pCands, nCands );
214  if ( pFunc == NULL )
215  return 0;
216  // update the network
217  Abc_NtkMfsUpdateNetwork( p, pNode, p->vMfsFanins, pFunc );
218 p->timeInt += Abc_Clock() - clk;
219  p->nRemoves++;
220  return 1;
221  }
222 
223  if ( fOnlyRemove || p->pPars->fRrOnly )
224  return 0;
225 
226  p->nTryResubs++;
227  if ( fVeryVerbose )
228  {
229  for ( i = 0; i < 9; i++ )
230  printf( " " );
231  for ( i = 0; i < Vec_PtrSize(p->vDivs)-Abc_ObjFaninNum(pNode); i++ )
232  printf( "%d", i % 10 );
233  for ( i = 0; i < Abc_ObjFaninNum(pNode); i++ )
234  if ( i == iFanin )
235  printf( "*" );
236  else
237  printf( "%c", 'a' + i );
238  printf( "\n" );
239  }
240  iVar = -1;
241  while ( 1 )
242  {
243  if ( fVeryVerbose )
244  {
245  printf( "%3d: %3d ", p->nCexes, iVar );
246  for ( i = 0; i < Vec_PtrSize(p->vDivs); i++ )
247  {
248  pData = (unsigned *)Vec_PtrEntry( p->vDivCexes, i );
249  printf( "%d", Abc_InfoHasBit(pData, p->nCexes-1) );
250  }
251  printf( "\n" );
252  }
253 
254  // find the next divisor to try
255  nWords = Abc_BitWordNum(p->nCexes);
256  assert( nWords <= p->nDivWords );
257  for ( iVar = 0; iVar < Vec_PtrSize(p->vDivs)-Abc_ObjFaninNum(pNode); iVar++ )
258  {
259  if ( p->pPars->fPower )
260  {
261  Abc_Obj_t * pDiv = (Abc_Obj_t *)Vec_PtrEntry(p->vDivs, iVar);
262  // only accept the divisor if it is "cool"
263  if ( Abc_MfsObjProb(p, pDiv) >= 0.15 )
264  continue;
265  }
266  pData = (unsigned *)Vec_PtrEntry( p->vDivCexes, iVar );
267  for ( w = 0; w < nWords; w++ )
268  if ( pData[w] != ~0 )
269  break;
270  if ( w == nWords )
271  break;
272  }
273  if ( iVar == Vec_PtrSize(p->vDivs)-Abc_ObjFaninNum(pNode) )
274  return 0;
275 
276  pCands[nCands] = toLitCond( Vec_IntEntry(p->vProjVarsSat, iVar), 1 );
277  RetValue = Abc_NtkMfsTryResubOnce( p, pCands, nCands+1 );
278  if ( RetValue == -1 )
279  return 0;
280  if ( RetValue == 1 )
281  {
282  if ( p->pPars->fVeryVerbose )
283  printf( "Node %d: Fanin %d can be replaced by divisor %d.\n", pNode->Id, iFanin, iVar );
284  p->nNodesResub++;
285  p->nNodesGainedLevel++;
286  if ( fSkipUpdate )
287  return 1;
288 clk = Abc_Clock();
289  // derive the function
290  pFunc = Abc_NtkMfsInterplate( p, pCands, nCands+1 );
291  if ( pFunc == NULL )
292  return 0;
293  // update the network
294  Vec_PtrPush( p->vMfsFanins, Vec_PtrEntry(p->vDivs, iVar) );
295  Abc_NtkMfsUpdateNetwork( p, pNode, p->vMfsFanins, pFunc );
296 p->timeInt += Abc_Clock() - clk;
297  p->nResubs++;
298  return 1;
299  }
300  if ( p->nCexes >= p->pPars->nWinMax )
301  break;
302  }
303  if ( p->pPars->fVeryVerbose )
304  printf( "Node %d: Cannot find replacement for fanin %d.\n", pNode->Id, iFanin );
305  return 0;
306 }
307 
308 /**Function*************************************************************
309 
310  Synopsis [Performs resubstitution for the node.]
311 
312  Description []
313 
314  SideEffects []
315 
316  SeeAlso []
317 
318 ***********************************************************************/
319 int Abc_NtkMfsSolveSatResub2( Mfs_Man_t * p, Abc_Obj_t * pNode, int iFanin, int iFanin2 )
320 {
321  int fVeryVerbose = p->pPars->fVeryVerbose && Vec_PtrSize(p->vDivs) < 80;
322  unsigned * pData, * pData2;
323  int pCands[MFS_FANIN_MAX];
324  int RetValue, iVar, iVar2, i, w, nCands, nWords, fBreak;
325  abctime clk;
326  Abc_Obj_t * pFanin;
327  Hop_Obj_t * pFunc;
328  assert( iFanin >= 0 );
329  assert( iFanin2 >= 0 || iFanin2 == -1 );
330 
331  // clean simulation info
332  Vec_PtrFillSimInfo( p->vDivCexes, 0, p->nDivWords );
333  p->nCexes = 0;
334  if ( fVeryVerbose )
335  {
336  printf( "\n" );
337  printf( "Node %5d : Level = %2d. Divs = %3d. Fanins = %d/%d (out of %d). MFFC = %d\n",
338  pNode->Id, pNode->Level, Vec_PtrSize(p->vDivs)-Abc_ObjFaninNum(pNode),
339  iFanin, iFanin2, Abc_ObjFaninNum(pNode),
340  Abc_ObjFanoutNum(Abc_ObjFanin(pNode, iFanin)) == 1 ? Abc_NodeMffcLabel(Abc_ObjFanin(pNode, iFanin)) : 0 );
341  }
342 
343  // try fanins without the critical fanin
344  nCands = 0;
345  Vec_PtrClear( p->vMfsFanins );
346  Abc_ObjForEachFanin( pNode, pFanin, i )
347  {
348  if ( i == iFanin || i == iFanin2 )
349  continue;
350  Vec_PtrPush( p->vMfsFanins, pFanin );
351  iVar = Vec_PtrSize(p->vDivs) - Abc_ObjFaninNum(pNode) + i;
352  pCands[nCands++] = toLitCond( Vec_IntEntry( p->vProjVarsSat, iVar ), 1 );
353  }
354  RetValue = Abc_NtkMfsTryResubOnce( p, pCands, nCands );
355  if ( RetValue == -1 )
356  return 0;
357  if ( RetValue == 1 )
358  {
359  if ( fVeryVerbose )
360  printf( "Node %d: Fanins %d/%d can be removed.\n", pNode->Id, iFanin, iFanin2 );
361  p->nNodesResub++;
362  p->nNodesGainedLevel++;
363 clk = Abc_Clock();
364  // derive the function
365  pFunc = Abc_NtkMfsInterplate( p, pCands, nCands );
366  if ( pFunc == NULL )
367  return 0;
368  // update the network
369  Abc_NtkMfsUpdateNetwork( p, pNode, p->vMfsFanins, pFunc );
370 p->timeInt += Abc_Clock() - clk;
371  return 1;
372  }
373 
374  if ( fVeryVerbose )
375  {
376  for ( i = 0; i < 11; i++ )
377  printf( " " );
378  for ( i = 0; i < Vec_PtrSize(p->vDivs)-Abc_ObjFaninNum(pNode); i++ )
379  printf( "%d", i % 10 );
380  for ( i = 0; i < Abc_ObjFaninNum(pNode); i++ )
381  if ( i == iFanin || i == iFanin2 )
382  printf( "*" );
383  else
384  printf( "%c", 'a' + i );
385  printf( "\n" );
386  }
387  iVar = iVar2 = -1;
388  while ( 1 )
389  {
390 #if 1 // sjang
391 #endif
392  if ( fVeryVerbose )
393  {
394  printf( "%3d: %2d %2d ", p->nCexes, iVar, iVar2 );
395  for ( i = 0; i < Vec_PtrSize(p->vDivs); i++ )
396  {
397  pData = (unsigned *)Vec_PtrEntry( p->vDivCexes, i );
398  printf( "%d", Abc_InfoHasBit(pData, p->nCexes-1) );
399  }
400  printf( "\n" );
401  }
402 
403  // find the next divisor to try
404  nWords = Abc_BitWordNum(p->nCexes);
405  assert( nWords <= p->nDivWords );
406  fBreak = 0;
407  for ( iVar = 1; iVar < Vec_PtrSize(p->vDivs)-Abc_ObjFaninNum(pNode); iVar++ )
408  {
409  pData = (unsigned *)Vec_PtrEntry( p->vDivCexes, iVar );
410 #if 1 // sjang
411  if ( p->pPars->fPower )
412  {
413  Abc_Obj_t * pDiv = (Abc_Obj_t *)Vec_PtrEntry(p->vDivs, iVar);
414  // only accept the divisor if it is "cool"
415  if ( Abc_MfsObjProb(p, pDiv) >= 0.12 )
416  continue;
417  }
418 #endif
419  for ( iVar2 = 0; iVar2 < iVar; iVar2++ )
420  {
421  pData2 = (unsigned *)Vec_PtrEntry( p->vDivCexes, iVar2 );
422 #if 1 // sjang
423  if ( p->pPars->fPower )
424  {
425  Abc_Obj_t * pDiv = (Abc_Obj_t *)Vec_PtrEntry(p->vDivs, iVar2);
426  // only accept the divisor if it is "cool"
427  if ( Abc_MfsObjProb(p, pDiv) >= 0.12 )
428  continue;
429  }
430 #endif
431  for ( w = 0; w < nWords; w++ )
432  if ( (pData[w] | pData2[w]) != ~0 )
433  break;
434  if ( w == nWords )
435  {
436  fBreak = 1;
437  break;
438  }
439  }
440  if ( fBreak )
441  break;
442  }
443  if ( iVar == Vec_PtrSize(p->vDivs)-Abc_ObjFaninNum(pNode) )
444  return 0;
445 
446  pCands[nCands] = toLitCond( Vec_IntEntry(p->vProjVarsSat, iVar2), 1 );
447  pCands[nCands+1] = toLitCond( Vec_IntEntry(p->vProjVarsSat, iVar), 1 );
448  RetValue = Abc_NtkMfsTryResubOnce( p, pCands, nCands+2 );
449  if ( RetValue == -1 )
450  return 0;
451  if ( RetValue == 1 )
452  {
453  if ( fVeryVerbose )
454  printf( "Node %d: Fanins %d/%d can be replaced by divisors %d/%d.\n", pNode->Id, iFanin, iFanin2, iVar, iVar2 );
455  p->nNodesResub++;
456  p->nNodesGainedLevel++;
457 clk = Abc_Clock();
458  // derive the function
459  pFunc = Abc_NtkMfsInterplate( p, pCands, nCands+2 );
460  if ( pFunc == NULL )
461  return 0;
462  // update the network
463  Vec_PtrPush( p->vMfsFanins, Vec_PtrEntry(p->vDivs, iVar2) );
464  Vec_PtrPush( p->vMfsFanins, Vec_PtrEntry(p->vDivs, iVar) );
465  assert( Vec_PtrSize(p->vMfsFanins) == nCands + 2 );
466  Abc_NtkMfsUpdateNetwork( p, pNode, p->vMfsFanins, pFunc );
467 p->timeInt += Abc_Clock() - clk;
468  return 1;
469  }
470  if ( p->nCexes >= p->pPars->nWinMax )
471  break;
472  }
473  return 0;
474 }
475 
476 
477 /**Function*************************************************************
478 
479  Synopsis [Evaluates the possibility of replacing given edge by another edge.]
480 
481  Description []
482 
483  SideEffects []
484 
485  SeeAlso []
486 
487 ***********************************************************************/
488 int Abc_NtkMfsEdgeSwapEval( Mfs_Man_t * p, Abc_Obj_t * pNode )
489 {
490  Abc_Obj_t * pFanin;
491  int i;
492  Abc_ObjForEachFanin( pNode, pFanin, i )
493  Abc_NtkMfsSolveSatResub( p, pNode, i, 0, 1 );
494  return 0;
495 }
496 
497 /**Function*************************************************************
498 
499  Synopsis [Evaluates the possibility of replacing given edge by another edge.]
500 
501  Description []
502 
503  SideEffects []
504 
505  SeeAlso []
506 
507 ***********************************************************************/
508 int Abc_NtkMfsEdgePower( Mfs_Man_t * p, Abc_Obj_t * pNode )
509 {
510  Abc_Obj_t * pFanin;
511  int i;
512  // try replacing area critical fanins
513  Abc_ObjForEachFanin( pNode, pFanin, i )
514  {
515  if ( Abc_MfsObjProb(p, pFanin) >= 0.35 )
516  {
517  if ( Abc_NtkMfsSolveSatResub( p, pNode, i, 0, 0 ) )
518  return 1;
519  } else if ( Abc_MfsObjProb(p, pFanin) >= 0.25 ) // sjang
520  {
521  if ( Abc_NtkMfsSolveSatResub( p, pNode, i, 1, 0 ) )
522  return 1;
523  }
524  }
525  return 0;
526 }
527 
528 /**Function*************************************************************
529 
530  Synopsis [Performs resubstitution for the node.]
531 
532  Description []
533 
534  SideEffects []
535 
536  SeeAlso []
537 
538 ***********************************************************************/
539 int Abc_NtkMfsResubNode( Mfs_Man_t * p, Abc_Obj_t * pNode )
540 {
541  Abc_Obj_t * pFanin;
542  int i;
543  // try replacing area critical fanins
544  Abc_ObjForEachFanin( pNode, pFanin, i )
545  if ( !Abc_ObjIsCi(pFanin) && Abc_ObjFanoutNum(pFanin) == 1 )
546  {
547  if ( Abc_NtkMfsSolveSatResub( p, pNode, i, 0, 0 ) )
548  return 1;
549  }
550  // try removing redundant edges
551  if ( !p->pPars->fArea )
552  {
553  Abc_ObjForEachFanin( pNode, pFanin, i )
554  if ( Abc_ObjIsCi(pFanin) || Abc_ObjFanoutNum(pFanin) != 1 )
555  {
556  if ( Abc_NtkMfsSolveSatResub( p, pNode, i, 1, 0 ) )
557  return 1;
558  }
559  }
560  if ( Abc_ObjFaninNum(pNode) == p->nFaninMax )
561  return 0;
562 /*
563  // try replacing area critical fanins while adding two new fanins
564  Abc_ObjForEachFanin( pNode, pFanin, i )
565  if ( !Abc_ObjIsCi(pFanin) && Abc_ObjFanoutNum(pFanin) == 1 )
566  {
567  if ( Abc_NtkMfsSolveSatResub2( p, pNode, i, -1 ) )
568  return 1;
569  }
570 */
571  return 0;
572 }
573 
574 /**Function*************************************************************
575 
576  Synopsis [Performs resubstitution for the node.]
577 
578  Description []
579 
580  SideEffects []
581 
582  SeeAlso []
583 
584 ***********************************************************************/
585 int Abc_NtkMfsResubNode2( Mfs_Man_t * p, Abc_Obj_t * pNode )
586 {
587  Abc_Obj_t * pFanin, * pFanin2;
588  int i, k;
589 /*
590  Abc_ObjForEachFanin( pNode, pFanin, i )
591  if ( !Abc_ObjIsCi(pFanin) && Abc_ObjFanoutNum(pFanin) == 1 )
592  {
593  if ( Abc_NtkMfsSolveSatResub( p, pNode, i, 0, 0 ) )
594  return 1;
595  }
596 */
597  if ( Abc_ObjFaninNum(pNode) < 2 )
598  return 0;
599  // try replacing one area critical fanin and one other fanin while adding two new fanins
600  Abc_ObjForEachFanin( pNode, pFanin, i )
601  {
602  if ( !Abc_ObjIsCi(pFanin) && Abc_ObjFanoutNum(pFanin) == 1 )
603  {
604  // consider second fanin to remove at the same time
605  Abc_ObjForEachFanin( pNode, pFanin2, k )
606  {
607  if ( i != k && Abc_NtkMfsSolveSatResub2( p, pNode, i, k ) )
608  return 1;
609  }
610  }
611  }
612  return 0;
613 }
614 
615 
616 ////////////////////////////////////////////////////////////////////////
617 /// END OF FILE ///
618 ////////////////////////////////////////////////////////////////////////
619 
620 
621 ABC_NAMESPACE_IMPL_END
622 
Vec_Ptr_t
typedefABC_NAMESPACE_HEADER_START struct Vec_Ptr_t_ Vec_Ptr_t
INCLUDES ///.
Definition: vecPtr.h:42
Mfs_Man_t_::nResubs
int nResubs
Definition: mfsInt.h:107
Abc_ObjIsCi
static int Abc_ObjIsCi(Abc_Obj_t *pObj)
Definition: abc.h:351
Mfs_Man_t_::vProjVarsSat
Vec_Int_t * vProjVarsSat
Definition: mfsInt.h:65
p
static Llb_Mgr_t * p
Definition: llb3Image.c:950
Abc_InfoHasBit
static int Abc_InfoHasBit(unsigned *p, int i)
Definition: abc_global.h:258
l_Undef
#define l_Undef
Definition: SolverTypes.h:86
Mfs_Man_t_::vSupp
Vec_Ptr_t * vSupp
Definition: mfsInt.h:60
Mfs_Man_t_::nRemoves
int nRemoves
Definition: mfsInt.h:106
sat_solver_solve
int sat_solver_solve(sat_solver *s, lit *begin, lit *end, ABC_INT64_T nConfLimit, ABC_INT64_T nInsLimit, ABC_INT64_T nConfLimitGlobal, ABC_INT64_T nInsLimitGlobal)
Definition: satSolver.c:1700
Abc_ObjFanoutNum
static int Abc_ObjFanoutNum(Abc_Obj_t *pObj)
Definition: abc.h:365
Mfs_Man_t_::pPars
Mfs_Par_t * pPars
Definition: mfsInt.h:53
Abc_InfoXorBit
static void Abc_InfoXorBit(unsigned *p, int i)
Definition: abc_global.h:260
Mfs_Man_t_::nNodesGainedLevel
int nNodesGainedLevel
Definition: mfsInt.h:85
Abc_ObjFaninNum
static int Abc_ObjFaninNum(Abc_Obj_t *pObj)
Definition: abc.h:364
Abc_NtkGetFaninMax
ABC_DLL int Abc_NtkGetFaninMax(Abc_Ntk_t *pNtk)
Definition: abcUtil.c:453
Vec_PtrPush
static void Vec_PtrPush(Vec_Ptr_t *p, void *Entry)
Definition: vecPtr.h:606
l_True
#define l_True
Definition: SolverTypes.h:84
Vec_PtrFillSimInfo
static void Vec_PtrFillSimInfo(Vec_Ptr_t *vInfo, int iWord, int nWords)
Definition: vecPtr.h:986
Abc_Clock
static abctime Abc_Clock()
Definition: abc_global.h:279
Vec_PtrSize
static int Vec_PtrSize(Vec_Ptr_t *p)
Definition: vecPtr.h:295
nWords
int nWords
Definition: abcNpn.c:127
Hop_Obj_t_
Definition: hop.h:65
Mfs_Man_t_::vNodes
Vec_Ptr_t * vNodes
Definition: mfsInt.h:61
sat_solver_var_value
static int sat_solver_var_value(sat_solver *s, int v)
Definition: satSolver.h:200
Mfs_Man_t_::vDivs
Vec_Ptr_t * vDivs
Definition: mfsInt.h:62
Abc_MfsObjProb
static float Abc_MfsObjProb(Mfs_Man_t *p, Abc_Obj_t *pObj)
Definition: mfsInt.h:137
Abc_Obj_t_::Level
unsigned Level
Definition: abc.h:142
Abc_ObjAddFanin
ABC_DLL void Abc_ObjAddFanin(Abc_Obj_t *pObj, Abc_Obj_t *pFanin)
Definition: abcFanio.c:84
Abc_Obj_t_
Definition: abc.h:128
Abc_NtkMfsResubNode2
int Abc_NtkMfsResubNode2(Mfs_Man_t *p, Abc_Obj_t *pNode)
Definition: mfsResub.c:585
Abc_NtkMfsEdgeSwapEval
int Abc_NtkMfsEdgeSwapEval(Mfs_Man_t *p, Abc_Obj_t *pNode)
Definition: mfsResub.c:488
Abc_NtkMfsEdgePower
int Abc_NtkMfsEdgePower(Mfs_Man_t *p, Abc_Obj_t *pNode)
Definition: mfsResub.c:508
toLitCond
static lit toLitCond(int v, int c)
Definition: satVec.h:143
Vec_IntEntry
static int Vec_IntEntry(Vec_Int_t *p, int i)
Definition: bblif.c:268
Abc_NtkMfsResubNode
int Abc_NtkMfsResubNode(Mfs_Man_t *p, Abc_Obj_t *pNode)
Definition: mfsResub.c:539
ABC_NAMESPACE_IMPL_END
#define ABC_NAMESPACE_IMPL_END
Definition: abc_global.h:108
Abc_NtkMfsInterplate
Hop_Obj_t * Abc_NtkMfsInterplate(Mfs_Man_t *p, int *pCands, int nCands)
Definition: mfsInter.c:329
Mfs_Man_t_::nFaninMax
int nFaninMax
Definition: mfsInt.h:57
Mfs_Man_t_::nSatCalls
int nSatCalls
Definition: mfsInt.h:70
Abc_NodeMffcLabel
ABC_DLL int Abc_NodeMffcLabel(Abc_Obj_t *pNode)
Definition: abcRefs.c:437
Mfs_Man_t_::nDivWords
int nDivWords
Definition: mfsInt.h:68
Mfs_Man_t_
Definition: mfsInt.h:50
Abc_NtkForEachNode
#define Abc_NtkForEachNode(pNtk, pNode, i)
Definition: abc.h:461
ABC_NAMESPACE_IMPL_START
#define ABC_NAMESPACE_IMPL_START
Definition: abc_global.h:107
Mfs_Man_t_::vDivCexes
Vec_Ptr_t * vDivCexes
Definition: mfsInt.h:67
Vec_PtrEntry
static void * Vec_PtrEntry(Vec_Ptr_t *p, int i)
Definition: vecPtr.h:362
Abc_NtkMfsSolveSatResub
int Abc_NtkMfsSolveSatResub(Mfs_Man_t *p, Abc_Obj_t *pNode, int iFanin, int fOnlyRemove, int fSkipUpdate)
DECLARATIONS ///.
Definition: mfsResub.c:165
Mfs_Man_t_::nCexes
int nCexes
Definition: mfsInt.h:69
Abc_Obj_t_::pNtk
Abc_Ntk_t * pNtk
Definition: abc.h:130
Mfs_Man_t_::nTryRemoves
int nTryRemoves
Definition: mfsInt.h:104
Abc_ObjForEachFanin
#define Abc_ObjForEachFanin(pObj, pFanin, i)
Definition: abc.h:524
Abc_NtkUpdate
ABC_DLL void Abc_NtkUpdate(Abc_Obj_t *pObj, Abc_Obj_t *pObjNew, Vec_Vec_t *vLevels)
Definition: abcTiming.c:1311
Abc_Obj_t_::Id
int Id
Definition: abc.h:132
Mfs_Man_t_::pNtk
Abc_Ntk_t * pNtk
Definition: mfsInt.h:54
Abc_NtkCreateNode
static Abc_Obj_t * Abc_NtkCreateNode(Abc_Ntk_t *pNtk)
Definition: abc.h:308
l_False
#define l_False
Definition: SolverTypes.h:85
Mfs_Man_t_::vMfsFanins
Vec_Ptr_t * vMfsFanins
Definition: mfsInt.h:93
Mfs_Man_t_::nSatCexes
int nSatCexes
Definition: mfsInt.h:71
Mfs_Man_t_::nNodesResub
int nNodesResub
Definition: mfsInt.h:109
Abc_NtkMfsSolveSatResub2
int Abc_NtkMfsSolveSatResub2(Mfs_Man_t *p, Abc_Obj_t *pNode, int iFanin, int iFanin2)
Definition: mfsResub.c:319
Abc_BitWordNum
static int Abc_BitWordNum(int nBits)
Definition: abc_global.h:255
assert
#define assert(ex)
Definition: util_old.h:213
Vec_PtrClear
static void Vec_PtrClear(Vec_Ptr_t *p)
Definition: vecPtr.h:545
Abc_NtkMfsTryResubOnce
int Abc_NtkMfsTryResubOnce(Mfs_Man_t *p, int *pCands, int nCands)
Definition: mfsResub.c:101
Mfs_Man_t_::timeInt
abctime timeInt
Definition: mfsInt.h:133
Mfs_Man_t_::pSat
sat_solver * pSat
Definition: mfsInt.h:89
Abc_ObjFaninId
static int Abc_ObjFaninId(Abc_Obj_t *pObj, int i)
Definition: abc.h:366
Abc_Obj_t_::pData
void * pData
Definition: abc.h:145
Abc_ObjFanin
static Abc_Obj_t * Abc_ObjFanin(Abc_Obj_t *pObj, int i)
Definition: abc.h:372
Vec_PtrForEachEntry
#define Vec_PtrForEachEntry(Type, vVec, pEntry, i)
MACRO DEFINITIONS ///.
Definition: vecPtr.h:55
Mfs_Man_t_::vLevels
Vec_Vec_t * vLevels
Definition: mfsInt.h:92
abctime
ABC_INT64_T abctime
Definition: abc_global.h:278
Abc_NtkMfsPrintResubStats
void Abc_NtkMfsPrintResubStats(Mfs_Man_t *p)
Definition: mfsResub.c:72
Vec_IntForEachEntry
#define Vec_IntForEachEntry(vVec, Entry, i)
MACRO DEFINITIONS ///.
Definition: vecInt.h:54
Abc_NtkMfsUpdateNetwork
ABC_NAMESPACE_IMPL_START void Abc_NtkMfsUpdateNetwork(Mfs_Man_t *p, Abc_Obj_t *pObj, Vec_Ptr_t *vMfsFanins, Hop_Obj_t *pFunc)
DECLARATIONS ///.
Definition: mfsResub.c:45
Mfs_Man_t_::nTryResubs
int nTryResubs
Definition: mfsInt.h:105
MFS_FANIN_MAX
#define MFS_FANIN_MAX
INCLUDES ///.
Definition: mfsInt.h:47
Mfs_Man_t_::nTimeOuts
int nTimeOuts
Definition: mfsInt.h:114