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 * vFanins, 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( vFanins, 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  unsigned * pData;
104  int RetValue, iVar, i;
105  p->nSatCalls++;
106  RetValue = sat_solver_solve( p->pSat, pCands, pCands + nCands, (sint64)p->pPars->nBTLimit, (sint64)0, (sint64)0, (sint64)0 );
107 // assert( RetValue == l_False || RetValue == l_True );
108  if ( RetValue == l_False )
109  return 1;
110  if ( RetValue != l_True )
111  {
112  p->nTimeOuts++;
113  return -1;
114  }
115  p->nSatCexes++;
116  // store the counter-example
117  Vec_IntForEachEntry( p->vProjVars, iVar, i )
118  {
119  pData = Vec_PtrEntry( p->vDivCexes, i );
120  if ( !sat_solver_var_value( p->pSat, iVar ) ) // remove 0s!!!
121  {
122  assert( Aig_InfoHasBit(pData, p->nCexes) );
123  Aig_InfoXorBit( pData, p->nCexes );
124  }
125  }
126  p->nCexes++;
127  return 0;
128 }
129 
130 /**Function*************************************************************
131 
132  Synopsis [Performs resubstitution for the node.]
133 
134  Description []
135 
136  SideEffects []
137 
138  SeeAlso []
139 
140 ***********************************************************************/
141 int Abc_NtkMfsSolveSatResub( Mfs_Man_t * p, Abc_Obj_t * pNode, int iFanin, int fOnlyRemove, int fSkipUpdate )
142 {
143  int fVeryVerbose = p->pPars->fVeryVerbose && Vec_PtrSize(p->vDivs) < 80;
144  unsigned * pData;
145  int pCands[MFS_FANIN_MAX];
146  int RetValue, iVar, i, nCands, nWords, w;
147  clock_t clk;
148  Abc_Obj_t * pFanin;
149  Hop_Obj_t * pFunc;
150  assert( iFanin >= 0 );
151 
152  // clean simulation info
153  Vec_PtrFillSimInfo( p->vDivCexes, 0, p->nDivWords );
154  p->nCexes = 0;
155  if ( fVeryVerbose )
156  {
157  printf( "\n" );
158  printf( "Node %5d : Level = %2d. Divs = %3d. Fanin = %d (out of %d). MFFC = %d\n",
159  pNode->Id, pNode->Level, Vec_PtrSize(p->vDivs)-Abc_ObjFaninNum(pNode),
160  iFanin, Abc_ObjFaninNum(pNode),
161  Abc_ObjFanoutNum(Abc_ObjFanin(pNode, iFanin)) == 1 ? Abc_NodeMffcLabel(Abc_ObjFanin(pNode, iFanin)) : 0 );
162  }
163 
164  // try fanins without the critical fanin
165  nCands = 0;
166  Vec_PtrClear( p->vFanins );
167  Abc_ObjForEachFanin( pNode, pFanin, i )
168  {
169  if ( i == iFanin )
170  continue;
171  Vec_PtrPush( p->vFanins, pFanin );
172  iVar = Vec_PtrSize(p->vDivs) - Abc_ObjFaninNum(pNode) + i;
173  pCands[nCands++] = toLitCond( Vec_IntEntry( p->vProjVars, iVar ), 1 );
174  }
175  RetValue = Abc_NtkMfsTryResubOnce( p, pCands, nCands );
176  if ( RetValue == -1 )
177  return 0;
178  if ( RetValue == 1 )
179  {
180  if ( fVeryVerbose )
181  printf( "Node %d: Fanin %d can be removed.\n", pNode->Id, iFanin );
182  p->nNodesResub++;
183  p->nNodesGainedLevel++;
184  if ( fSkipUpdate )
185  return 1;
186 clk = clock();
187  // derive the function
188  pFunc = Abc_NtkMfsInterplate( p, pCands, nCands );
189  if ( pFunc == NULL )
190  return 0;
191  // update the network
192  Abc_NtkMfsUpdateNetwork( p, pNode, p->vFanins, pFunc );
193 p->timeInt += clock() - clk;
194  return 1;
195  }
196 
197  if ( fOnlyRemove )
198  return 0;
199 
200  if ( fVeryVerbose )
201  {
202  for ( i = 0; i < 8; i++ )
203  printf( " " );
204  for ( i = 0; i < Vec_PtrSize(p->vDivs)-Abc_ObjFaninNum(pNode); i++ )
205  printf( "%d", i % 10 );
206  for ( i = 0; i < Abc_ObjFaninNum(pNode); i++ )
207  if ( i == iFanin )
208  printf( "*" );
209  else
210  printf( "%c", 'a' + i );
211  printf( "\n" );
212  }
213  iVar = -1;
214  while ( 1 )
215  {
216  float * pProbab = (float *)(p->vProbs? p->vProbs->pArray : NULL);
217  assert( (pProbab != NULL) == p->pPars->fPower );
218  if ( fVeryVerbose )
219  {
220  printf( "%3d: %2d ", p->nCexes, iVar );
221  for ( i = 0; i < Vec_PtrSize(p->vDivs); i++ )
222  {
223  pData = Vec_PtrEntry( p->vDivCexes, i );
224  printf( "%d", Aig_InfoHasBit(pData, p->nCexes-1) );
225  }
226  printf( "\n" );
227  }
228 
229  // find the next divisor to try
230  nWords = Aig_BitWordNum(p->nCexes);
231  assert( nWords <= p->nDivWords );
232  for ( iVar = 0; iVar < Vec_PtrSize(p->vDivs)-Abc_ObjFaninNum(pNode); iVar++ )
233  {
234  if ( p->pPars->fPower )
235  {
236  Abc_Obj_t * pDiv = Vec_PtrEntry(p->vDivs, iVar);
237  // only accept the divisor if it is "cool"
238  if ( pProbab[Abc_ObjId(pDiv)] >= 0.2 )
239  continue;
240  }
241  pData = Vec_PtrEntry( p->vDivCexes, iVar );
242  for ( w = 0; w < nWords; w++ )
243  if ( pData[w] != ~0 )
244  break;
245  if ( w == nWords )
246  break;
247  }
248  if ( iVar == Vec_PtrSize(p->vDivs)-Abc_ObjFaninNum(pNode) )
249  return 0;
250 
251  pCands[nCands] = toLitCond( Vec_IntEntry(p->vProjVars, iVar), 1 );
252  RetValue = Abc_NtkMfsTryResubOnce( p, pCands, nCands+1 );
253  if ( RetValue == -1 )
254  return 0;
255  if ( RetValue == 1 )
256  {
257  if ( fVeryVerbose )
258  printf( "Node %d: Fanin %d can be replaced by divisor %d.\n", pNode->Id, iFanin, iVar );
259  p->nNodesResub++;
260  p->nNodesGainedLevel++;
261  if ( fSkipUpdate )
262  return 1;
263 clk = clock();
264  // derive the function
265  pFunc = Abc_NtkMfsInterplate( p, pCands, nCands+1 );
266  if ( pFunc == NULL )
267  return 0;
268  // update the network
269  Vec_PtrPush( p->vFanins, Vec_PtrEntry(p->vDivs, iVar) );
270  Abc_NtkMfsUpdateNetwork( p, pNode, p->vFanins, pFunc );
271 p->timeInt += clock() - clk;
272  return 1;
273  }
274  if ( p->nCexes >= p->pPars->nDivMax )
275  break;
276  }
277  return 0;
278 }
279 
280 /**Function*************************************************************
281 
282  Synopsis [Performs resubstitution for the node.]
283 
284  Description []
285 
286  SideEffects []
287 
288  SeeAlso []
289 
290 ***********************************************************************/
291 int Abc_NtkMfsSolveSatResub2( Mfs_Man_t * p, Abc_Obj_t * pNode, int iFanin, int iFanin2 )
292 {
293  int fVeryVerbose = p->pPars->fVeryVerbose && Vec_PtrSize(p->vDivs) < 80;
294  unsigned * pData, * pData2;
295  int pCands[MFS_FANIN_MAX];
296  int RetValue, iVar, iVar2, i, w, nCands, nWords, fBreak;
297  clock_t clk;
298  Abc_Obj_t * pFanin;
299  Hop_Obj_t * pFunc;
300  assert( iFanin >= 0 );
301  assert( iFanin2 >= 0 || iFanin2 == -1 );
302 
303  // clean simulation info
304  Vec_PtrFillSimInfo( p->vDivCexes, 0, p->nDivWords );
305  p->nCexes = 0;
306  if ( fVeryVerbose )
307  {
308  printf( "\n" );
309  printf( "Node %5d : Level = %2d. Divs = %3d. Fanins = %d/%d (out of %d). MFFC = %d\n",
310  pNode->Id, pNode->Level, Vec_PtrSize(p->vDivs)-Abc_ObjFaninNum(pNode),
311  iFanin, iFanin2, Abc_ObjFaninNum(pNode),
312  Abc_ObjFanoutNum(Abc_ObjFanin(pNode, iFanin)) == 1 ? Abc_NodeMffcLabel(Abc_ObjFanin(pNode, iFanin)) : 0 );
313  }
314 
315  // try fanins without the critical fanin
316  nCands = 0;
317  Vec_PtrClear( p->vFanins );
318  Abc_ObjForEachFanin( pNode, pFanin, i )
319  {
320  if ( i == iFanin || i == iFanin2 )
321  continue;
322  Vec_PtrPush( p->vFanins, pFanin );
323  iVar = Vec_PtrSize(p->vDivs) - Abc_ObjFaninNum(pNode) + i;
324  pCands[nCands++] = toLitCond( Vec_IntEntry( p->vProjVars, iVar ), 1 );
325  }
326  RetValue = Abc_NtkMfsTryResubOnce( p, pCands, nCands );
327  if ( RetValue == -1 )
328  return 0;
329  if ( RetValue == 1 )
330  {
331  if ( fVeryVerbose )
332  printf( "Node %d: Fanins %d/%d can be removed.\n", pNode->Id, iFanin, iFanin2 );
333  p->nNodesResub++;
334  p->nNodesGainedLevel++;
335 clk = clock();
336  // derive the function
337  pFunc = Abc_NtkMfsInterplate( p, pCands, nCands );
338  if ( pFunc == NULL )
339  return 0;
340  // update the network
341  Abc_NtkMfsUpdateNetwork( p, pNode, p->vFanins, pFunc );
342 p->timeInt += clock() - clk;
343  return 1;
344  }
345 
346  if ( fVeryVerbose )
347  {
348  for ( i = 0; i < 11; i++ )
349  printf( " " );
350  for ( i = 0; i < Vec_PtrSize(p->vDivs)-Abc_ObjFaninNum(pNode); i++ )
351  printf( "%d", i % 10 );
352  for ( i = 0; i < Abc_ObjFaninNum(pNode); i++ )
353  if ( i == iFanin || i == iFanin2 )
354  printf( "*" );
355  else
356  printf( "%c", 'a' + i );
357  printf( "\n" );
358  }
359  iVar = iVar2 = -1;
360  while ( 1 )
361  {
362  if ( fVeryVerbose )
363  {
364  printf( "%3d: %2d %2d ", p->nCexes, iVar, iVar2 );
365  for ( i = 0; i < Vec_PtrSize(p->vDivs); i++ )
366  {
367  pData = Vec_PtrEntry( p->vDivCexes, i );
368  printf( "%d", Aig_InfoHasBit(pData, p->nCexes-1) );
369  }
370  printf( "\n" );
371  }
372 
373  // find the next divisor to try
374  nWords = Aig_BitWordNum(p->nCexes);
375  assert( nWords <= p->nDivWords );
376  fBreak = 0;
377  for ( iVar = 1; iVar < Vec_PtrSize(p->vDivs)-Abc_ObjFaninNum(pNode); iVar++ )
378  {
379  pData = Vec_PtrEntry( p->vDivCexes, iVar );
380  for ( iVar2 = 0; iVar2 < iVar; iVar2++ )
381  {
382  pData2 = Vec_PtrEntry( p->vDivCexes, iVar2 );
383  for ( w = 0; w < nWords; w++ )
384  if ( (pData[w] | pData2[w]) != ~0 )
385  break;
386  if ( w == nWords )
387  {
388  fBreak = 1;
389  break;
390  }
391  }
392  if ( fBreak )
393  break;
394  }
395  if ( iVar == Vec_PtrSize(p->vDivs)-Abc_ObjFaninNum(pNode) )
396  return 0;
397 
398  pCands[nCands] = toLitCond( Vec_IntEntry(p->vProjVars, iVar2), 1 );
399  pCands[nCands+1] = toLitCond( Vec_IntEntry(p->vProjVars, iVar), 1 );
400  RetValue = Abc_NtkMfsTryResubOnce( p, pCands, nCands+2 );
401  if ( RetValue == -1 )
402  return 0;
403  if ( RetValue == 1 )
404  {
405  if ( fVeryVerbose )
406  printf( "Node %d: Fanins %d/%d can be replaced by divisors %d/%d.\n", pNode->Id, iFanin, iFanin2, iVar, iVar2 );
407  p->nNodesResub++;
408  p->nNodesGainedLevel++;
409 clk = clock();
410  // derive the function
411  pFunc = Abc_NtkMfsInterplate( p, pCands, nCands+2 );
412  if ( pFunc == NULL )
413  return 0;
414  // update the network
415  Vec_PtrPush( p->vFanins, Vec_PtrEntry(p->vDivs, iVar2) );
416  Vec_PtrPush( p->vFanins, Vec_PtrEntry(p->vDivs, iVar) );
417  assert( Vec_PtrSize(p->vFanins) == nCands + 2 );
418  Abc_NtkMfsUpdateNetwork( p, pNode, p->vFanins, pFunc );
419 p->timeInt += clock() - clk;
420  return 1;
421  }
422  if ( p->nCexes >= p->pPars->nDivMax )
423  break;
424  }
425  return 0;
426 }
427 
428 
429 /**Function*************************************************************
430 
431  Synopsis [Evaluates the possibility of replacing given edge by another edge.]
432 
433  Description []
434 
435  SideEffects []
436 
437  SeeAlso []
438 
439 ***********************************************************************/
440 int Abc_NtkMfsEdgeSwapEval( Mfs_Man_t * p, Abc_Obj_t * pNode )
441 {
442  Abc_Obj_t * pFanin;
443  int i;
444  Abc_ObjForEachFanin( pNode, pFanin, i )
445  Abc_NtkMfsSolveSatResub( p, pNode, i, 0, 1 );
446  return 0;
447 }
448 
449 /**Function*************************************************************
450 
451  Synopsis [Evaluates the possibility of replacing given edge by another edge.]
452 
453  Description []
454 
455  SideEffects []
456 
457  SeeAlso []
458 
459 ***********************************************************************/
460 int Abc_NtkMfsEdgePower( Mfs_Man_t * p, Abc_Obj_t * pNode )
461 {
462  Abc_Obj_t * pFanin;
463  float * pProbab = (float *)p->vProbs->pArray;
464  int i;
465  // try replacing area critical fanins
466  Abc_ObjForEachFanin( pNode, pFanin, i )
467  if ( pProbab[pFanin->Id] >= 0.4 )
468  {
469  if ( Abc_NtkMfsSolveSatResub( p, pNode, i, 0, 0 ) )
470  return 1;
471  }
472  return 0;
473 }
474 
475 /**Function*************************************************************
476 
477  Synopsis [Performs resubstitution for the node.]
478 
479  Description []
480 
481  SideEffects []
482 
483  SeeAlso []
484 
485 ***********************************************************************/
486 int Abc_NtkMfsResubNode( Mfs_Man_t * p, Abc_Obj_t * pNode )
487 {
488  Abc_Obj_t * pFanin;
489  int i;
490  // try replacing area critical fanins
491  Abc_ObjForEachFanin( pNode, pFanin, i )
492  if ( !Abc_ObjIsCi(pFanin) && Abc_ObjFanoutNum(pFanin) == 1 )
493  {
494  if ( Abc_NtkMfsSolveSatResub( p, pNode, i, 0, 0 ) )
495  return 1;
496  }
497  // try removing redundant edges
498  if ( !p->pPars->fArea )
499  {
500  Abc_ObjForEachFanin( pNode, pFanin, i )
501  if ( Abc_ObjIsCi(pFanin) || Abc_ObjFanoutNum(pFanin) != 1 )
502  {
503  if ( Abc_NtkMfsSolveSatResub( p, pNode, i, 1, 0 ) )
504  return 1;
505  }
506  }
507  if ( Abc_ObjFaninNum(pNode) == p->nFaninMax )
508  return 0;
509  // try replacing area critical fanins while adding two new fanins
510  Abc_ObjForEachFanin( pNode, pFanin, i )
511  if ( !Abc_ObjIsCi(pFanin) && Abc_ObjFanoutNum(pFanin) == 1 )
512  {
513  if ( Abc_NtkMfsSolveSatResub2( p, pNode, i, -1 ) )
514  return 1;
515  }
516  return 0;
517 }
518 
519 /**Function*************************************************************
520 
521  Synopsis [Performs resubstitution for the node.]
522 
523  Description []
524 
525  SideEffects []
526 
527  SeeAlso []
528 
529 ***********************************************************************/
530 int Abc_NtkMfsResubNode2( Mfs_Man_t * p, Abc_Obj_t * pNode )
531 {
532  Abc_Obj_t * pFanin, * pFanin2;
533  int i, k;
534 /*
535  Abc_ObjForEachFanin( pNode, pFanin, i )
536  if ( !Abc_ObjIsCi(pFanin) && Abc_ObjFanoutNum(pFanin) == 1 )
537  {
538  if ( Abc_NtkMfsSolveSatResub( p, pNode, i, 0, 0 ) )
539  return 1;
540  }
541 */
542  if ( Abc_ObjFaninNum(pNode) < 2 )
543  return 0;
544  // try replacing one area critical fanin and one other fanin while adding two new fanins
545  Abc_ObjForEachFanin( pNode, pFanin, i )
546  {
547  if ( !Abc_ObjIsCi(pFanin) && Abc_ObjFanoutNum(pFanin) == 1 )
548  {
549  // consider second fanin to remove at the same time
550  Abc_ObjForEachFanin( pNode, pFanin2, k )
551  {
552  if ( i != k && Abc_NtkMfsSolveSatResub2( p, pNode, i, k ) )
553  return 1;
554  }
555  }
556  }
557  return 0;
558 }
559 
560 
561 ////////////////////////////////////////////////////////////////////////
562 /// END OF FILE ///
563 ////////////////////////////////////////////////////////////////////////
564 
565 
566 ABC_NAMESPACE_IMPL_END
567 
Abc_ObjId
static unsigned Abc_ObjId(Abc_Obj_t *pObj)
Definition: abc.h:329
Mfs_Man_t_::vProbs
Vec_Int_t * vProbs
Definition: mfsInt.h:97
Abc_NtkMfsTryResubOnce
int Abc_NtkMfsTryResubOnce(Mfs_Man_t *p, int *pCands, int nCands)
Definition: mfsResub_.c:101
Vec_Ptr_t
typedefABC_NAMESPACE_HEADER_START struct Vec_Ptr_t_ Vec_Ptr_t
INCLUDES ///.
Definition: vecPtr.h:42
Abc_ObjIsCi
static int Abc_ObjIsCi(Abc_Obj_t *pObj)
Definition: abc.h:351
Abc_NtkMfsEdgePower
int Abc_NtkMfsEdgePower(Mfs_Man_t *p, Abc_Obj_t *pNode)
Definition: mfsResub_.c:460
p
static Llb_Mgr_t * p
Definition: llb3Image.c:950
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
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
Abc_NtkMfsPrintResubStats
void Abc_NtkMfsPrintResubStats(Mfs_Man_t *p)
Definition: mfsResub_.c:72
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_NtkMfsResubNode2
int Abc_NtkMfsResubNode2(Mfs_Man_t *p, Abc_Obj_t *pNode)
Definition: mfsResub_.c:530
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
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_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_NtkMfsUpdateNetwork
ABC_NAMESPACE_IMPL_START void Abc_NtkMfsUpdateNetwork(Mfs_Man_t *p, Abc_Obj_t *pObj, Vec_Ptr_t *vFanins, Hop_Obj_t *pFunc)
DECLARATIONS ///.
Definition: mfsResub_.c:45
Abc_NtkMfsResubNode
int Abc_NtkMfsResubNode(Mfs_Man_t *p, Abc_Obj_t *pNode)
Definition: mfsResub_.c:486
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_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
Abc_NtkMfsEdgeSwapEval
int Abc_NtkMfsEdgeSwapEval(Mfs_Man_t *p, Abc_Obj_t *pNode)
Definition: mfsResub_.c:440
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
Mfs_Man_t_::nCexes
int nCexes
Definition: mfsInt.h:69
Abc_Obj_t_::pNtk
Abc_Ntk_t * pNtk
Definition: abc.h:130
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_::nSatCexes
int nSatCexes
Definition: mfsInt.h:71
Mfs_Man_t_::nNodesResub
int nNodesResub
Definition: mfsInt.h:109
assert
#define assert(ex)
Definition: util_old.h:213
Vec_PtrClear
static void Vec_PtrClear(Vec_Ptr_t *p)
Definition: vecPtr.h:545
Mfs_Man_t_::timeInt
abctime timeInt
Definition: mfsInt.h:133
Mfs_Man_t_::pSat
sat_solver * pSat
Definition: mfsInt.h:89
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
Vec_IntForEachEntry
#define Vec_IntForEachEntry(vVec, Entry, i)
MACRO DEFINITIONS ///.
Definition: vecInt.h:54
Abc_NtkMfsSolveSatResub
int Abc_NtkMfsSolveSatResub(Mfs_Man_t *p, Abc_Obj_t *pNode, int iFanin, int fOnlyRemove, int fSkipUpdate)
DECLARATIONS ///.
Definition: mfsResub_.c:141
Abc_NtkMfsSolveSatResub2
int Abc_NtkMfsSolveSatResub2(Mfs_Man_t *p, Abc_Obj_t *pNode, int iFanin, int iFanin2)
Definition: mfsResub_.c:291
MFS_FANIN_MAX
#define MFS_FANIN_MAX
INCLUDES ///.
Definition: mfsInt.h:47
Mfs_Man_t_::nTimeOuts
int nTimeOuts
Definition: mfsInt.h:114