mfsResub.c 19.3 KB
Newer Older
Alan Mishchenko committed
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22
/**CFile****************************************************************

  FileName    [mfsResub.c]

  SystemName  [ABC: Logic synthesis and verification system.]

  PackageName [The good old minimization with complete don't-cares.]

  Synopsis    [Procedures to perform resubstitution.]

  Author      [Alan Mishchenko]
  
  Affiliation [UC Berkeley]

  Date        [Ver. 1.0. Started - June 20, 2005.]

  Revision    [$Id: mfsResub.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]

***********************************************************************/

#include "mfsInt.h"

23 24 25
ABC_NAMESPACE_IMPL_START


Alan Mishchenko committed
26 27 28 29 30 31 32
////////////////////////////////////////////////////////////////////////
///                        DECLARATIONS                              ///
////////////////////////////////////////////////////////////////////////

////////////////////////////////////////////////////////////////////////
///                     FUNCTION DEFINITIONS                         ///
////////////////////////////////////////////////////////////////////////
Alan Mishchenko committed
33
 
Alan Mishchenko committed
34 35 36 37 38 39 40 41 42 43 44
/**Function*************************************************************

  Synopsis    [Updates the network after resubstitution.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
45
void Abc_NtkMfsUpdateNetwork( Mfs_Man_t * p, Abc_Obj_t * pObj, Vec_Ptr_t * vMfsFanins, Hop_Obj_t * pFunc )
Alan Mishchenko committed
46 47 48 49 50 51
{
    Abc_Obj_t * pObjNew, * pFanin;
    int k;
    // create the new node
    pObjNew = Abc_NtkCreateNode( pObj->pNtk );
    pObjNew->pData = pFunc;
52
    Vec_PtrForEachEntry( Abc_Obj_t *, vMfsFanins, pFanin, k )
Alan Mishchenko committed
53 54 55 56 57 58 59 60 61 62
        Abc_ObjAddFanin( pObjNew, pFanin );
    // replace the old node by the new node
//printf( "Replacing node " ); Abc_ObjPrint( stdout, pObj );
//printf( "Inserting node " ); Abc_ObjPrint( stdout, pObjNew );
    // update the level of the node
    Abc_NtkUpdate( pObj, pObjNew, p->vLevels );
}

/**Function*************************************************************

Alan Mishchenko committed
63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79 80 81 82 83 84 85
  Synopsis    [Prints resub candidate stats.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
void Abc_NtkMfsPrintResubStats( Mfs_Man_t * p )
{
    Abc_Obj_t * pFanin, * pNode;
    int i, k, nAreaCrits = 0, nAreaExpanse = 0;
    int nFaninMax = Abc_NtkGetFaninMax(p->pNtk);
    Abc_NtkForEachNode( p->pNtk, pNode, i )
        Abc_ObjForEachFanin( pNode, pFanin, k )
        {
            if ( !Abc_ObjIsCi(pFanin) && Abc_ObjFanoutNum(pFanin) == 1 )
            {
                nAreaCrits++;
                nAreaExpanse += (int)(Abc_ObjFaninNum(pNode) < nFaninMax);
            }
        }
Alan Mishchenko committed
86 87
//    printf( "Total area-critical fanins = %d. Belonging to expandable nodes = %d.\n", 
//        nAreaCrits, nAreaExpanse );
Alan Mishchenko committed
88 89 90 91
}

/**Function*************************************************************

Alan Mishchenko committed
92 93 94 95 96 97 98 99 100 101 102
  Synopsis    [Tries resubstitution.]

  Description [Returns 1 if it is feasible, or 0 if c-ex is found.]
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
int Abc_NtkMfsTryResubOnce( Mfs_Man_t * p, int * pCands, int nCands )
{
Alan Mishchenko committed
103
    int fVeryVerbose = 0;
Alan Mishchenko committed
104
    unsigned * pData;
105
    int RetValue, RetValue2 = -1, iVar, i;//, clk = Abc_Clock();
106
/*
Alan Mishchenko committed
107 108 109
    if ( p->pPars->fGiaSat )
    {
        RetValue2 = Abc_NtkMfsTryResubOnceGia( p, pCands, nCands );
110
p->timeGia += Abc_Clock() - clk;
Alan Mishchenko committed
111 112
        return RetValue2;
    }
113
*/ 
Alan Mishchenko committed
114
    p->nSatCalls++;
Alan Mishchenko committed
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 );
Alan Mishchenko committed
116
//    assert( RetValue == l_False || RetValue == l_True );
Alan Mishchenko committed
117

Alan Mishchenko committed
118 119 120 121
    if ( RetValue != l_Undef && RetValue2 != -1 )
    {
        assert( (RetValue == l_False) == (RetValue2 == 1) );
    }
Alan Mishchenko committed
122

Alan Mishchenko committed
123
    if ( RetValue == l_False )
Alan Mishchenko committed
124 125 126
    {
        if ( fVeryVerbose )
        printf( "U " );
Alan Mishchenko committed
127
        return 1;
Alan Mishchenko committed
128
    }
Alan Mishchenko committed
129 130
    if ( RetValue != l_True )
    {
Alan Mishchenko committed
131 132
        if ( fVeryVerbose )
        printf( "T " );
Alan Mishchenko committed
133 134 135
        p->nTimeOuts++;
        return -1;
    }
Alan Mishchenko committed
136 137
    if ( fVeryVerbose )
    printf( "S " );
Alan Mishchenko committed
138 139
    p->nSatCexes++;
    // store the counter-example
140
    Vec_IntForEachEntry( p->vProjVarsSat, iVar, i )
Alan Mishchenko committed
141
    {
142
        pData = (unsigned *)Vec_PtrEntry( p->vDivCexes, i );
Alan Mishchenko committed
143 144
        if ( !sat_solver_var_value( p->pSat, iVar ) ) // remove 0s!!!
        {
145 146
            assert( Abc_InfoHasBit(pData, p->nCexes) );
            Abc_InfoXorBit( pData, p->nCexes );
Alan Mishchenko committed
147
        }
Alan Mishchenko committed
148
    }
Alan Mishchenko committed
149
    p->nCexes++;
Alan Mishchenko committed
150
    return 0;
Alan Mishchenko committed
151

Alan Mishchenko committed
152 153 154 155 156 157 158 159 160 161 162 163 164
}

/**Function*************************************************************

  Synopsis    [Performs resubstitution for the node.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
Alan Mishchenko committed
165
int Abc_NtkMfsSolveSatResub( Mfs_Man_t * p, Abc_Obj_t * pNode, int iFanin, int fOnlyRemove, int fSkipUpdate )
Alan Mishchenko committed
166
{
Alan Mishchenko committed
167
    int fVeryVerbose = 0;//p->pPars->fVeryVerbose && Vec_PtrSize(p->vDivs) < 200;// || pNode->Id == 556;
Alan Mishchenko committed
168 169
    unsigned * pData;
    int pCands[MFS_FANIN_MAX];
170
    int RetValue, iVar, i, nCands, nWords, w;
171
    abctime clk;
Alan Mishchenko committed
172 173 174
    Abc_Obj_t * pFanin;
    Hop_Obj_t * pFunc;
    assert( iFanin >= 0 );
Alan Mishchenko committed
175
    p->nTryRemoves++;
Alan Mishchenko committed
176 177

    // clean simulation info
Alan Mishchenko committed
178
    Vec_PtrFillSimInfo( p->vDivCexes, 0, p->nDivWords ); 
Alan Mishchenko committed
179
    p->nCexes = 0;
Alan Mishchenko committed
180
    if ( p->pPars->fVeryVerbose )
Alan Mishchenko committed
181
    {
Alan Mishchenko committed
182
//        printf( "\n" );
Alan Mishchenko committed
183 184 185
        printf( "%5d : Lev =%3d. Leaf =%3d. Node =%3d. Divs =%3d.  Fanin = %4d (%d/%d), MFFC = %d\n", 
            pNode->Id, pNode->Level, Vec_PtrSize(p->vSupp), Vec_PtrSize(p->vNodes), Vec_PtrSize(p->vDivs)-Abc_ObjFaninNum(pNode), 
            Abc_ObjFaninId(pNode, iFanin), iFanin, Abc_ObjFaninNum(pNode), 
Alan Mishchenko committed
186 187 188 189 190
            Abc_ObjFanoutNum(Abc_ObjFanin(pNode, iFanin)) == 1 ? Abc_NodeMffcLabel(Abc_ObjFanin(pNode, iFanin)) : 0 );
    }

    // try fanins without the critical fanin
    nCands = 0;
191
    Vec_PtrClear( p->vMfsFanins );
Alan Mishchenko committed
192 193 194 195
    Abc_ObjForEachFanin( pNode, pFanin, i )
    {
        if ( i == iFanin )
            continue;
196
        Vec_PtrPush( p->vMfsFanins, pFanin );
Alan Mishchenko committed
197
        iVar = Vec_PtrSize(p->vDivs) - Abc_ObjFaninNum(pNode) + i;
198
        pCands[nCands++] = toLitCond( Vec_IntEntry( p->vProjVarsSat, iVar ), 1 );
Alan Mishchenko committed
199
    }
Alan Mishchenko committed
200 201 202 203
    RetValue = Abc_NtkMfsTryResubOnce( p, pCands, nCands );
    if ( RetValue == -1 )
        return 0;
    if ( RetValue == 1 )
Alan Mishchenko committed
204
    {
Alan Mishchenko committed
205 206
        if ( p->pPars->fVeryVerbose )
            printf( "Node %d: Fanin %d can be removed.\n", pNode->Id, iFanin );
Alan Mishchenko committed
207
        p->nNodesResub++;
Alan Mishchenko committed
208
        p->nNodesGainedLevel++;
Alan Mishchenko committed
209 210
        if ( fSkipUpdate )
            return 1;
211
clk = Abc_Clock();
Alan Mishchenko committed
212 213
        // derive the function
        pFunc = Abc_NtkMfsInterplate( p, pCands, nCands );
Alan Mishchenko committed
214 215
        if ( pFunc == NULL )
            return 0;
Alan Mishchenko committed
216
        // update the network
217
        Abc_NtkMfsUpdateNetwork( p, pNode, p->vMfsFanins, pFunc );
218
p->timeInt += Abc_Clock() - clk;
Alan Mishchenko committed
219
        p->nRemoves++;
Alan Mishchenko committed
220 221 222
        return 1;
    }

Alan Mishchenko committed
223
    if ( fOnlyRemove || p->pPars->fRrOnly )
Alan Mishchenko committed
224 225
        return 0;

Alan Mishchenko committed
226
    p->nTryResubs++;
Alan Mishchenko committed
227 228
    if ( fVeryVerbose )
    {
Alan Mishchenko committed
229
        for ( i = 0; i < 9; i++ )
Alan Mishchenko committed
230 231 232 233 234 235 236 237 238 239 240
            printf( " " );
        for ( i = 0; i < Vec_PtrSize(p->vDivs)-Abc_ObjFaninNum(pNode); i++ )
            printf( "%d", i % 10 );
        for ( i = 0; i < Abc_ObjFaninNum(pNode); i++ )
            if ( i == iFanin )
                printf( "*" );
            else
                printf( "%c", 'a' + i );
        printf( "\n" );
    }
    iVar = -1;
Alan Mishchenko committed
241
    while ( 1 ) 
Alan Mishchenko committed
242 243 244
    {
        if ( fVeryVerbose )
        {
Alan Mishchenko committed
245
            printf( "%3d: %3d ", p->nCexes, iVar );
Alan Mishchenko committed
246
            for ( i = 0; i < Vec_PtrSize(p->vDivs); i++ )
Alan Mishchenko committed
247
            {
248
                pData = (unsigned *)Vec_PtrEntry( p->vDivCexes, i );
249
                printf( "%d", Abc_InfoHasBit(pData, p->nCexes-1) );
Alan Mishchenko committed
250
            }
Alan Mishchenko committed
251 252 253 254
            printf( "\n" );
        }

        // find the next divisor to try
255
        nWords = Abc_BitWordNum(p->nCexes);
Alan Mishchenko committed
256
        assert( nWords <= p->nDivWords );
Alan Mishchenko committed
257
        for ( iVar = 0; iVar < Vec_PtrSize(p->vDivs)-Abc_ObjFaninNum(pNode); iVar++ )
Alan Mishchenko committed
258
        {
Alan Mishchenko committed
259 260
            if ( p->pPars->fPower )
            {
261
                Abc_Obj_t * pDiv = (Abc_Obj_t *)Vec_PtrEntry(p->vDivs, iVar);
Alan Mishchenko committed
262
                // only accept the divisor if it is "cool"
Alan Mishchenko committed
263
                if ( Abc_MfsObjProb(p, pDiv) >= 0.15 )
Alan Mishchenko committed
264 265
                    continue;
            }
266
            pData  = (unsigned *)Vec_PtrEntry( p->vDivCexes, iVar );
Alan Mishchenko committed
267 268 269 270
            for ( w = 0; w < nWords; w++ )
                if ( pData[w] != ~0 )
                    break;
            if ( w == nWords )
Alan Mishchenko committed
271
                break;
Alan Mishchenko committed
272
        }
Alan Mishchenko committed
273 274
        if ( iVar == Vec_PtrSize(p->vDivs)-Abc_ObjFaninNum(pNode) )
            return 0;
Alan Mishchenko committed
275

276
        pCands[nCands] = toLitCond( Vec_IntEntry(p->vProjVarsSat, iVar), 1 );
Alan Mishchenko committed
277 278 279 280
        RetValue = Abc_NtkMfsTryResubOnce( p, pCands, nCands+1 );
        if ( RetValue == -1 )
            return 0;
        if ( RetValue == 1 )
Alan Mishchenko committed
281
        {
Alan Mishchenko committed
282 283
            if ( p->pPars->fVeryVerbose )
                printf( "Node %d: Fanin %d can be replaced by divisor %d.\n", pNode->Id, iFanin, iVar );
Alan Mishchenko committed
284
            p->nNodesResub++;
Alan Mishchenko committed
285
            p->nNodesGainedLevel++;
Alan Mishchenko committed
286 287
            if ( fSkipUpdate )
                return 1;
288
clk = Abc_Clock();
Alan Mishchenko committed
289 290
            // derive the function
            pFunc = Abc_NtkMfsInterplate( p, pCands, nCands+1 );
Alan Mishchenko committed
291 292
            if ( pFunc == NULL )
                return 0;
Alan Mishchenko committed
293
            // update the network
294 295
            Vec_PtrPush( p->vMfsFanins, Vec_PtrEntry(p->vDivs, iVar) );
            Abc_NtkMfsUpdateNetwork( p, pNode, p->vMfsFanins, pFunc );
296
p->timeInt += Abc_Clock() - clk;
Alan Mishchenko committed
297
            p->nResubs++;
Alan Mishchenko committed
298 299
            return 1;
        }
300
        if ( p->nCexes >= p->pPars->nWinMax )
Alan Mishchenko committed
301
            break;
Alan Mishchenko committed
302
    }
Alan Mishchenko committed
303 304
    if ( p->pPars->fVeryVerbose )
        printf( "Node %d: Cannot find replacement for fanin %d.\n", pNode->Id, iFanin );
Alan Mishchenko committed
305 306 307 308 309 310 311 312 313 314 315 316 317 318
    return 0;
}

/**Function*************************************************************

  Synopsis    [Performs resubstitution for the node.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
Alan Mishchenko committed
319
int Abc_NtkMfsSolveSatResub2( Mfs_Man_t * p, Abc_Obj_t * pNode, int iFanin, int iFanin2 )
Alan Mishchenko committed
320
{
Alan Mishchenko committed
321 322 323
    int fVeryVerbose = p->pPars->fVeryVerbose && Vec_PtrSize(p->vDivs) < 80;
    unsigned * pData, * pData2;
    int pCands[MFS_FANIN_MAX];
324
    int RetValue, iVar, iVar2, i, w, nCands, nWords, fBreak;
325
    abctime clk;
Alan Mishchenko committed
326
    Abc_Obj_t * pFanin;
Alan Mishchenko committed
327 328 329 330 331 332 333 334 335 336 337 338 339 340 341 342 343 344
    Hop_Obj_t * pFunc;
    assert( iFanin >= 0 );
    assert( iFanin2 >= 0 || iFanin2 == -1 );

    // clean simulation info
    Vec_PtrFillSimInfo( p->vDivCexes, 0, p->nDivWords ); 
    p->nCexes = 0;
    if ( fVeryVerbose )
    {
        printf( "\n" );
        printf( "Node %5d : Level = %2d. Divs = %3d.  Fanins = %d/%d (out of %d). MFFC = %d\n", 
            pNode->Id, pNode->Level, Vec_PtrSize(p->vDivs)-Abc_ObjFaninNum(pNode), 
            iFanin, iFanin2, Abc_ObjFaninNum(pNode), 
            Abc_ObjFanoutNum(Abc_ObjFanin(pNode, iFanin)) == 1 ? Abc_NodeMffcLabel(Abc_ObjFanin(pNode, iFanin)) : 0 );
    }

    // try fanins without the critical fanin
    nCands = 0;
345
    Vec_PtrClear( p->vMfsFanins );
Alan Mishchenko committed
346
    Abc_ObjForEachFanin( pNode, pFanin, i )
Alan Mishchenko committed
347 348 349
    {
        if ( i == iFanin || i == iFanin2 )
            continue;
350
        Vec_PtrPush( p->vMfsFanins, pFanin );
Alan Mishchenko committed
351
        iVar = Vec_PtrSize(p->vDivs) - Abc_ObjFaninNum(pNode) + i;
352
        pCands[nCands++] = toLitCond( Vec_IntEntry( p->vProjVarsSat, iVar ), 1 );
Alan Mishchenko committed
353
    }
Alan Mishchenko committed
354 355 356 357
    RetValue = Abc_NtkMfsTryResubOnce( p, pCands, nCands );
    if ( RetValue == -1 )
        return 0;
    if ( RetValue == 1 )
Alan Mishchenko committed
358 359 360 361
    {
        if ( fVeryVerbose )
        printf( "Node %d: Fanins %d/%d can be removed.\n", pNode->Id, iFanin, iFanin2 );
        p->nNodesResub++;
Alan Mishchenko committed
362
        p->nNodesGainedLevel++;
363
clk = Abc_Clock();
Alan Mishchenko committed
364 365
        // derive the function
        pFunc = Abc_NtkMfsInterplate( p, pCands, nCands );
Alan Mishchenko committed
366 367
        if ( pFunc == NULL )
            return 0;
Alan Mishchenko committed
368
        // update the network
369
        Abc_NtkMfsUpdateNetwork( p, pNode, p->vMfsFanins, pFunc );
370
p->timeInt += Abc_Clock() - clk;
Alan Mishchenko committed
371 372 373 374 375 376 377 378 379 380 381 382 383 384 385 386 387 388 389
        return 1;
    }

    if ( fVeryVerbose )
    {
        for ( i = 0; i < 11; i++ )
            printf( " " );
        for ( i = 0; i < Vec_PtrSize(p->vDivs)-Abc_ObjFaninNum(pNode); i++ )
            printf( "%d", i % 10 );
        for ( i = 0; i < Abc_ObjFaninNum(pNode); i++ )
            if ( i == iFanin || i == iFanin2 )
                printf( "*" );
            else
                printf( "%c", 'a' + i );
        printf( "\n" );
    }
    iVar = iVar2 = -1;
    while ( 1 )
    {
Alan Mishchenko committed
390 391
#if 1 // sjang
#endif
Alan Mishchenko committed
392
        if ( fVeryVerbose )
Alan Mishchenko committed
393
        {
Alan Mishchenko committed
394 395 396
            printf( "%3d: %2d %2d ", p->nCexes, iVar, iVar2 );
            for ( i = 0; i < Vec_PtrSize(p->vDivs); i++ )
            {
397
                pData = (unsigned *)Vec_PtrEntry( p->vDivCexes, i );
398
                printf( "%d", Abc_InfoHasBit(pData, p->nCexes-1) );
Alan Mishchenko committed
399 400 401 402 403
            }
            printf( "\n" );
        }

        // find the next divisor to try
404
        nWords = Abc_BitWordNum(p->nCexes);
Alan Mishchenko committed
405 406 407 408
        assert( nWords <= p->nDivWords );
        fBreak = 0;
        for ( iVar = 1; iVar < Vec_PtrSize(p->vDivs)-Abc_ObjFaninNum(pNode); iVar++ )
        {
409
            pData  = (unsigned *)Vec_PtrEntry( p->vDivCexes, iVar );
Alan Mishchenko committed
410 411 412
#if 1  // sjang
            if ( p->pPars->fPower )
            {
413
                Abc_Obj_t * pDiv = (Abc_Obj_t *)Vec_PtrEntry(p->vDivs, iVar);
Alan Mishchenko committed
414
                // only accept the divisor if it is "cool"
Alan Mishchenko committed
415
                if ( Abc_MfsObjProb(p, pDiv) >= 0.12 )
Alan Mishchenko committed
416 417 418
                    continue;
            }
#endif
Alan Mishchenko committed
419 420
            for ( iVar2 = 0; iVar2 < iVar; iVar2++ )
            {
421
                pData2 = (unsigned *)Vec_PtrEntry( p->vDivCexes, iVar2 );
Alan Mishchenko committed
422 423 424
#if 1 // sjang
                if ( p->pPars->fPower )
                {
425
                    Abc_Obj_t * pDiv = (Abc_Obj_t *)Vec_PtrEntry(p->vDivs, iVar2);
Alan Mishchenko committed
426
                    // only accept the divisor if it is "cool"
Alan Mishchenko committed
427
                    if ( Abc_MfsObjProb(p, pDiv) >= 0.12 )
Alan Mishchenko committed
428 429 430
                        continue;
                }
#endif
Alan Mishchenko committed
431 432 433 434 435 436 437 438 439 440 441 442 443 444 445
                for ( w = 0; w < nWords; w++ )
                    if ( (pData[w] | pData2[w]) != ~0 )
                        break;
                if ( w == nWords )
                {
                    fBreak = 1;
                    break;
                }
            }
            if ( fBreak )
                break;
        }
        if ( iVar == Vec_PtrSize(p->vDivs)-Abc_ObjFaninNum(pNode) )
            return 0;

446 447
        pCands[nCands]   = toLitCond( Vec_IntEntry(p->vProjVarsSat, iVar2), 1 );
        pCands[nCands+1] = toLitCond( Vec_IntEntry(p->vProjVarsSat, iVar), 1 );
Alan Mishchenko committed
448 449 450 451
        RetValue = Abc_NtkMfsTryResubOnce( p, pCands, nCands+2 );
        if ( RetValue == -1 )
            return 0;
        if ( RetValue == 1 )
Alan Mishchenko committed
452 453 454 455
        {
            if ( fVeryVerbose )
            printf( "Node %d: Fanins %d/%d can be replaced by divisors %d/%d.\n", pNode->Id, iFanin, iFanin2, iVar, iVar2 );
            p->nNodesResub++;
Alan Mishchenko committed
456
            p->nNodesGainedLevel++;
457
clk = Abc_Clock();
Alan Mishchenko committed
458 459
            // derive the function
            pFunc = Abc_NtkMfsInterplate( p, pCands, nCands+2 );
Alan Mishchenko committed
460 461
            if ( pFunc == NULL )
                return 0;
Alan Mishchenko committed
462
            // update the network
463 464 465 466
            Vec_PtrPush( p->vMfsFanins, Vec_PtrEntry(p->vDivs, iVar2) );
            Vec_PtrPush( p->vMfsFanins, Vec_PtrEntry(p->vDivs, iVar) );
            assert( Vec_PtrSize(p->vMfsFanins) == nCands + 2 );
            Abc_NtkMfsUpdateNetwork( p, pNode, p->vMfsFanins, pFunc );
467
p->timeInt += Abc_Clock() - clk;
Alan Mishchenko committed
468
            return 1;
Alan Mishchenko committed
469
        }
470
        if ( p->nCexes >= p->pPars->nWinMax )
Alan Mishchenko committed
471 472 473 474 475 476 477 478 479 480 481 482 483 484 485 486 487 488 489 490 491 492 493
            break;
    }
    return 0;
}


/**Function*************************************************************

  Synopsis    [Evaluates the possibility of replacing given edge by another edge.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
int Abc_NtkMfsEdgeSwapEval( Mfs_Man_t * p, Abc_Obj_t * pNode )
{
    Abc_Obj_t * pFanin;
    int i;
    Abc_ObjForEachFanin( pNode, pFanin, i )
        Abc_NtkMfsSolveSatResub( p, pNode, i, 0, 1 );
Alan Mishchenko committed
494 495 496 497 498
    return 0;
}

/**Function*************************************************************

Alan Mishchenko committed
499 500 501 502 503 504 505 506 507 508 509 510 511 512 513 514
  Synopsis    [Evaluates the possibility of replacing given edge by another edge.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
int Abc_NtkMfsEdgePower( Mfs_Man_t * p, Abc_Obj_t * pNode )
{
    Abc_Obj_t * pFanin;
    int i;
    // try replacing area critical fanins
    Abc_ObjForEachFanin( pNode, pFanin, i )
    {
Alan Mishchenko committed
515
        if ( Abc_MfsObjProb(p, pFanin) >= 0.35 )
Alan Mishchenko committed
516 517 518
        {
            if ( Abc_NtkMfsSolveSatResub( p, pNode, i, 0, 0 ) )
                return 1;
Alan Mishchenko committed
519
        } else if ( Abc_MfsObjProb(p, pFanin) >= 0.25 ) // sjang
Alan Mishchenko committed
520 521 522 523 524 525 526 527 528 529
        {
            if ( Abc_NtkMfsSolveSatResub( p, pNode, i, 1, 0 ) )
                return 1;
        }
        }
    return 0;
}

/**Function*************************************************************

Alan Mishchenko committed
530 531 532 533 534 535 536 537 538
  Synopsis    [Performs resubstitution for the node.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
Alan Mishchenko committed
539
int Abc_NtkMfsResubNode( Mfs_Man_t * p, Abc_Obj_t * pNode )
Alan Mishchenko committed
540 541 542
{
    Abc_Obj_t * pFanin;
    int i;
Alan Mishchenko committed
543
    // try replacing area critical fanins
Alan Mishchenko committed
544 545 546
    Abc_ObjForEachFanin( pNode, pFanin, i )
        if ( !Abc_ObjIsCi(pFanin) && Abc_ObjFanoutNum(pFanin) == 1 )
        {
Alan Mishchenko committed
547
            if ( Abc_NtkMfsSolveSatResub( p, pNode, i, 0, 0 ) )
Alan Mishchenko committed
548 549
                return 1;
        }
Alan Mishchenko committed
550 551 552 553 554 555 556 557 558 559 560 561
    // try removing redundant edges
    if ( !p->pPars->fArea )
    {
        Abc_ObjForEachFanin( pNode, pFanin, i )
            if ( Abc_ObjIsCi(pFanin) || Abc_ObjFanoutNum(pFanin) != 1 )
            {
                if ( Abc_NtkMfsSolveSatResub( p, pNode, i, 1, 0 ) )
                    return 1;
            }
    }
    if ( Abc_ObjFaninNum(pNode) == p->nFaninMax )
        return 0;
Alan Mishchenko committed
562
/*
Alan Mishchenko committed
563
    // try replacing area critical fanins while adding two new fanins
Alan Mishchenko committed
564
    Abc_ObjForEachFanin( pNode, pFanin, i )
Alan Mishchenko committed
565
        if ( !Abc_ObjIsCi(pFanin) && Abc_ObjFanoutNum(pFanin) == 1 )
Alan Mishchenko committed
566
        {
Alan Mishchenko committed
567
            if ( Abc_NtkMfsSolveSatResub2( p, pNode, i, -1 ) )
Alan Mishchenko committed
568 569
                return 1;
        }
Alan Mishchenko committed
570
*/
Alan Mishchenko committed
571 572 573
    return 0;
}

Alan Mishchenko committed
574 575 576 577 578 579 580 581 582 583 584 585 586 587 588 589 590 591 592 593 594 595 596 597 598 599 600 601 602 603 604 605 606 607 608 609 610 611 612 613 614 615
/**Function*************************************************************

  Synopsis    [Performs resubstitution for the node.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
int Abc_NtkMfsResubNode2( Mfs_Man_t * p, Abc_Obj_t * pNode )
{
    Abc_Obj_t * pFanin, * pFanin2;
    int i, k;
/*
    Abc_ObjForEachFanin( pNode, pFanin, i )
        if ( !Abc_ObjIsCi(pFanin) && Abc_ObjFanoutNum(pFanin) == 1 )
        {
            if ( Abc_NtkMfsSolveSatResub( p, pNode, i, 0, 0 ) )
                return 1;
        }
*/
    if ( Abc_ObjFaninNum(pNode) < 2 )
        return 0;
    // try replacing one area critical fanin and one other fanin while adding two new fanins
    Abc_ObjForEachFanin( pNode, pFanin, i )
    {
        if ( !Abc_ObjIsCi(pFanin) && Abc_ObjFanoutNum(pFanin) == 1 )
        {
            // consider second fanin to remove at the same time
            Abc_ObjForEachFanin( pNode, pFanin2, k )
            {
                if ( i != k && Abc_NtkMfsSolveSatResub2( p, pNode, i, k ) )
                    return 1;
            }
        }
    }
    return 0;
}


Alan Mishchenko committed
616 617 618 619 620
////////////////////////////////////////////////////////////////////////
///                       END OF FILE                                ///
////////////////////////////////////////////////////////////////////////


621 622
ABC_NAMESPACE_IMPL_END