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 ***********************************************************************/
Abc_NtkMfsUpdateNetwork(Mfs_Man_t * p,Abc_Obj_t * pObj,Vec_Ptr_t * vMfsFanins,Hop_Obj_t * pFunc)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 ***********************************************************************/
Abc_NtkMfsPrintResubStats(Mfs_Man_t * p)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 ***********************************************************************/
Abc_NtkMfsTryResubOnce(Mfs_Man_t * p,int * pCands,int nCands)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 ***********************************************************************/
Abc_NtkMfsSolveSatResub(Mfs_Man_t * p,Abc_Obj_t * pNode,int iFanin,int fOnlyRemove,int fSkipUpdate)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), NULL) : 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 ***********************************************************************/
Abc_NtkMfsSolveSatResub2(Mfs_Man_t * p,Abc_Obj_t * pNode,int iFanin,int iFanin2)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), NULL) : 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 ***********************************************************************/
Abc_NtkMfsEdgeSwapEval(Mfs_Man_t * p,Abc_Obj_t * pNode)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 ***********************************************************************/
Abc_NtkMfsEdgePower(Mfs_Man_t * p,Abc_Obj_t * pNode)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 ***********************************************************************/
Abc_NtkMfsResubNode(Mfs_Man_t * p,Abc_Obj_t * pNode)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 ***********************************************************************/
Abc_NtkMfsResubNode2(Mfs_Man_t * p,Abc_Obj_t * pNode)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 
623