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