sswClass.c 35.2 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    [sswClass.c]

  SystemName  [ABC: Logic synthesis and verification system.]

  PackageName [Inductive prover with constraints.]

  Synopsis    [Representation of candidate equivalence classes.]

  Author      [Alan Mishchenko]
  
  Affiliation [UC Berkeley]

  Date        [Ver. 1.0. Started - September 1, 2008.]

  Revision    [$Id: sswClass.c,v 1.00 2008/09/01 00:00:00 alanmi Exp $]

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

#include "sswInt.h"

23 24 25
ABC_NAMESPACE_IMPL_START


Alan Mishchenko committed
26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41
/*
    The candidate equivalence classes are stored as a vector of pointers 
    to the array of pointers to the nodes in each class.
    The first node of the class is its representative node.
    The representative has the smallest topological order among the class nodes.
    The nodes inside each class are ordered according to their topological order.
    The classes are ordered according to the topo order of their representatives.
*/

// internal representation of candidate equivalence classes
struct Ssw_Cla_t_
{
    // class information
    Aig_Man_t *      pAig;             // original AIG manager
    Aig_Obj_t ***    pId2Class;        // non-const classes by ID of repr node
    int *            pClassSizes;      // sizes of each equivalence class
42
    int              fConstCorr;
Alan Mishchenko committed
43 44 45 46 47 48 49 50 51 52
    // statistics
    int              nClasses;         // the total number of non-const classes
    int              nCands1;          // the total number of const candidates
    int              nLits;            // the number of literals in all classes
    // memory
    Aig_Obj_t **     pMemClasses;      // memory allocated for equivalence classes
    Aig_Obj_t **     pMemClassesFree;  // memory allocated for equivalence classes to be used
    // temporary data
    Vec_Ptr_t *      vClassOld;        // old equivalence class after splitting
    Vec_Ptr_t *      vClassNew;        // new equivalence class(es) after splitting
Alan Mishchenko committed
53
    Vec_Ptr_t *      vRefined;         // the nodes refined since the last iteration
Alan Mishchenko committed
54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79 80 81 82 83 84 85 86 87 88 89 90 91
    // procedures used for class refinement
    void *           pManData;
    unsigned (*pFuncNodeHash) (void *,Aig_Obj_t *);              // returns hash key of the node
    int (*pFuncNodeIsConst)   (void *,Aig_Obj_t *);              // returns 1 if the node is a constant
    int (*pFuncNodesAreEqual) (void *,Aig_Obj_t *, Aig_Obj_t *); // returns 1 if nodes are equal up to a complement
};

////////////////////////////////////////////////////////////////////////
///                        DECLARATIONS                              ///
////////////////////////////////////////////////////////////////////////

static inline Aig_Obj_t *  Ssw_ObjNext( Aig_Obj_t ** ppNexts, Aig_Obj_t * pObj )                       { return ppNexts[pObj->Id];  }
static inline void         Ssw_ObjSetNext( Aig_Obj_t ** ppNexts, Aig_Obj_t * pObj, Aig_Obj_t * pNext ) { ppNexts[pObj->Id] = pNext; }

// iterator through the equivalence classes
#define Ssw_ManForEachClass( p, ppClass, i )                 \
    for ( i = 0; i < Aig_ManObjNumMax(p->pAig); i++ )        \
        if ( ((ppClass) = p->pId2Class[i]) == NULL ) {} else
// iterator through the nodes in one class
#define Ssw_ClassForEachNode( p, pRepr, pNode, i )           \
    for ( i = 0; i < p->pClassSizes[pRepr->Id]; i++ )        \
        if ( ((pNode) = p->pId2Class[pRepr->Id][i]) == NULL ) {} else

////////////////////////////////////////////////////////////////////////
///                     FUNCTION DEFINITIONS                         ///
////////////////////////////////////////////////////////////////////////

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

  Synopsis    [Creates one equivalence class.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
92
static inline void Ssw_ObjAddClass( Ssw_Cla_t * p, Aig_Obj_t * pRepr, Aig_Obj_t ** pClass, int nSize )
Alan Mishchenko committed
93 94
{
    assert( p->pId2Class[pRepr->Id] == NULL );
Alan Mishchenko committed
95
    assert( pClass[0] == pRepr );
96
    p->pId2Class[pRepr->Id] = pClass;
Alan Mishchenko committed
97 98 99 100 101 102 103 104 105 106 107 108 109 110 111 112 113 114
    assert( p->pClassSizes[pRepr->Id] == 0 );
    assert( nSize > 1 );
    p->pClassSizes[pRepr->Id] = nSize;
    p->nClasses++;
    p->nLits += nSize - 1;
}

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

  Synopsis    [Removes one equivalence class.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
115
static inline Aig_Obj_t ** Ssw_ObjRemoveClass( Ssw_Cla_t * p, Aig_Obj_t * pRepr )
Alan Mishchenko committed
116 117 118 119
{
    Aig_Obj_t ** pClass = p->pId2Class[pRepr->Id];
    int nSize;
    assert( pClass != NULL );
120
    p->pId2Class[pRepr->Id] = NULL;
Alan Mishchenko committed
121 122 123 124 125 126 127 128 129 130 131 132 133
    nSize = p->pClassSizes[pRepr->Id];
    assert( nSize > 1 );
    p->nClasses--;
    p->nLits -= nSize - 1;
    p->pClassSizes[pRepr->Id] = 0;
    return pClass;
}

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

  Synopsis    [Starts representation of equivalence classes.]

  Description []
134

Alan Mishchenko committed
135 136 137 138 139 140 141 142
  SideEffects []

  SeeAlso     []

***********************************************************************/
Ssw_Cla_t * Ssw_ClassesStart( Aig_Man_t * pAig )
{
    Ssw_Cla_t * p;
Alan Mishchenko committed
143
    p = ABC_ALLOC( Ssw_Cla_t, 1 );
Alan Mishchenko committed
144 145
    memset( p, 0, sizeof(Ssw_Cla_t) );
    p->pAig         = pAig;
Alan Mishchenko committed
146 147
    p->pId2Class    = ABC_CALLOC( Aig_Obj_t **, Aig_ManObjNumMax(pAig) );
    p->pClassSizes  = ABC_CALLOC( int, Aig_ManObjNumMax(pAig) );
Alan Mishchenko committed
148 149
    p->vClassOld    = Vec_PtrAlloc( 100 );
    p->vClassNew    = Vec_PtrAlloc( 100 );
Alan Mishchenko committed
150
    p->vRefined     = Vec_PtrAlloc( 1000 );
151 152
    if ( pAig->pReprs == NULL )
        Aig_ManReprStart( pAig, Aig_ManObjNumMax(pAig) );
Alan Mishchenko committed
153 154 155 156 157 158 159 160
    return p;
}

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

  Synopsis    [Starts representation of equivalence classes.]

  Description []
161

Alan Mishchenko committed
162 163 164 165 166
  SideEffects []

  SeeAlso     []

***********************************************************************/
167
void Ssw_ClassesSetData( Ssw_Cla_t * p, void * pManData,
Alan Mishchenko committed
168 169 170 171 172 173 174 175 176 177 178 179 180 181 182
    unsigned (*pFuncNodeHash)(void *,Aig_Obj_t *),               // returns hash key of the node
    int (*pFuncNodeIsConst)(void *,Aig_Obj_t *),                 // returns 1 if the node is a constant
    int (*pFuncNodesAreEqual)(void *,Aig_Obj_t *, Aig_Obj_t *) ) // returns 1 if nodes are equal up to a complement
{
    p->pManData           = pManData;
    p->pFuncNodeHash      = pFuncNodeHash;
    p->pFuncNodeIsConst   = pFuncNodeIsConst;
    p->pFuncNodesAreEqual = pFuncNodesAreEqual;
}

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

  Synopsis    [Stop representation of equivalence classes.]

  Description []
183

Alan Mishchenko committed
184 185 186 187 188 189 190 191 192
  SideEffects []

  SeeAlso     []

***********************************************************************/
void Ssw_ClassesStop( Ssw_Cla_t * p )
{
    if ( p->vClassNew )    Vec_PtrFree( p->vClassNew );
    if ( p->vClassOld )    Vec_PtrFree( p->vClassOld );
Alan Mishchenko committed
193
    Vec_PtrFree( p->vRefined );
Alan Mishchenko committed
194 195 196 197
    ABC_FREE( p->pId2Class );
    ABC_FREE( p->pClassSizes );
    ABC_FREE( p->pMemClasses );
    ABC_FREE( p );
Alan Mishchenko committed
198 199 200 201
}

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

Alan Mishchenko committed
202 203 204
  Synopsis    [Stop representation of equivalence classes.]

  Description []
205

Alan Mishchenko committed
206 207 208 209 210 211 212 213 214 215 216 217
  SideEffects []

  SeeAlso     []

***********************************************************************/
Aig_Man_t * Ssw_ClassesReadAig( Ssw_Cla_t * p )
{
    return p->pAig;
}

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

Alan Mishchenko committed
218 219 220
  Synopsis    []

  Description []
221

Alan Mishchenko committed
222 223 224 225 226 227 228 229 230 231 232 233 234 235 236
  SideEffects []

  SeeAlso     []

***********************************************************************/
Vec_Ptr_t * Ssw_ClassesGetRefined( Ssw_Cla_t * p )
{
    return p->vRefined;
}

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

  Synopsis    []

  Description []
237

Alan Mishchenko committed
238 239 240 241 242 243 244 245 246 247 248 249
  SideEffects []

  SeeAlso     []

***********************************************************************/
void Ssw_ClassesClearRefined( Ssw_Cla_t * p )
{
    Vec_PtrClear( p->vRefined );
}

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

Alan Mishchenko committed
250 251 252
  Synopsis    [Stop representation of equivalence classes.]

  Description []
253

Alan Mishchenko committed
254 255 256 257 258 259 260 261 262 263 264 265 266 267 268
  SideEffects []

  SeeAlso     []

***********************************************************************/
int Ssw_ClassesCand1Num( Ssw_Cla_t * p )
{
    return p->nCands1;
}

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

  Synopsis    [Stop representation of equivalence classes.]

  Description []
269

Alan Mishchenko committed
270 271 272 273 274 275 276 277 278 279 280 281 282 283 284
  SideEffects []

  SeeAlso     []

***********************************************************************/
int Ssw_ClassesClassNum( Ssw_Cla_t * p )
{
    return p->nClasses;
}

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

  Synopsis    [Stop representation of equivalence classes.]

  Description []
285

Alan Mishchenko committed
286 287 288 289 290 291 292 293 294 295 296 297 298 299 300
  SideEffects []

  SeeAlso     []

***********************************************************************/
int Ssw_ClassesLitNum( Ssw_Cla_t * p )
{
    return p->nLits;
}

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

  Synopsis    [Stop representation of equivalence classes.]

  Description []
301

Alan Mishchenko committed
302 303 304 305 306 307 308
  SideEffects []

  SeeAlso     []

***********************************************************************/
Aig_Obj_t ** Ssw_ClassesReadClass( Ssw_Cla_t * p, Aig_Obj_t * pRepr, int * pnSize )
{
Alan Mishchenko committed
309 310
    if ( p->pId2Class[pRepr->Id] == NULL )
        return NULL;
Alan Mishchenko committed
311 312 313 314 315 316 317
    assert( p->pId2Class[pRepr->Id] != NULL );
    assert( p->pClassSizes[pRepr->Id] > 1 );
    *pnSize = p->pClassSizes[pRepr->Id];
    return p->pId2Class[pRepr->Id];
}

/**Function*************************************************************
Alan Mishchenko committed
318 319 320 321

  Synopsis    [Stop representation of equivalence classes.]

  Description []
322

Alan Mishchenko committed
323 324 325 326 327 328 329 330 331 332 333 334 335 336 337 338 339
  SideEffects []

  SeeAlso     []

***********************************************************************/
void Ssw_ClassesCollectClass( Ssw_Cla_t * p, Aig_Obj_t * pRepr, Vec_Ptr_t * vClass )
{
    int i;
    Vec_PtrClear( vClass );
    if ( p->pId2Class[pRepr->Id] == NULL )
        return;
    assert( p->pClassSizes[pRepr->Id] > 1 );
    for ( i = 1; i < p->pClassSizes[pRepr->Id]; i++ )
        Vec_PtrPush( vClass, p->pId2Class[pRepr->Id][i] );
}

/**Function*************************************************************
Alan Mishchenko committed
340 341 342 343 344 345 346 347 348 349 350 351 352 353 354 355 356 357

  Synopsis    [Checks candidate equivalence classes.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
void Ssw_ClassesCheck( Ssw_Cla_t * p )
{
    Aig_Obj_t * pObj, * pPrev, ** ppClass;
    int i, k, nLits, nClasses, nCands1;
    nClasses = nLits = 0;
    Ssw_ManForEachClass( p, ppClass, k )
    {
        pPrev = NULL;
Alan Mishchenko committed
358
        assert( p->pClassSizes[ppClass[0]->Id] >= 2 );
Alan Mishchenko committed
359 360 361 362 363 364 365 366 367 368 369 370 371 372 373 374 375 376 377 378 379 380 381 382 383 384 385 386 387 388 389 390 391 392 393 394 395
        Ssw_ClassForEachNode( p, ppClass[0], pObj, i )
        {
            if ( i == 0 )
                assert( Aig_ObjRepr(p->pAig, pObj) == NULL );
            else
            {
                assert( Aig_ObjRepr(p->pAig, pObj) == ppClass[0] );
                assert( pPrev->Id < pObj->Id );
                nLits++;
            }
            pPrev = pObj;
        }
        nClasses++;
    }
    nCands1 = 0;
    Aig_ManForEachObj( p->pAig, pObj, i )
        nCands1 += Ssw_ObjIsConst1Cand( p->pAig, pObj );
    assert( p->nLits == nLits );
    assert( p->nCands1 == nCands1 );
    assert( p->nClasses == nClasses );
}

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

  Synopsis    [Prints simulation classes.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
void Ssw_ClassesPrintOne( Ssw_Cla_t * p, Aig_Obj_t * pRepr )
{
    Aig_Obj_t * pObj;
    int i;
396
    Abc_Print( 1, "{ " );
Alan Mishchenko committed
397
    Ssw_ClassForEachNode( p, pRepr, pObj, i )
398
        Abc_Print( 1, "%d(%d,%d,%d) ", pObj->Id, pObj->Level,
Alan Mishchenko committed
399
        Aig_SupportSize(p->pAig,pObj), Aig_NodeMffcSupp(p->pAig,pObj,0,NULL) );
400
    Abc_Print( 1, "}\n" );
Alan Mishchenko committed
401 402 403 404 405 406 407 408 409 410 411 412 413 414 415 416 417 418
}

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

  Synopsis    [Prints simulation classes.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
void Ssw_ClassesPrint( Ssw_Cla_t * p, int fVeryVerbose )
{
    Aig_Obj_t ** ppClass;
    Aig_Obj_t * pObj;
    int i;
419
    Abc_Print( 1, "Equiv classes: Const1 = %5d. Class = %5d. Lit = %5d.\n",
Alan Mishchenko committed
420
        p->nCands1, p->nClasses, p->nCands1+p->nLits );
Alan Mishchenko committed
421 422
    if ( !fVeryVerbose )
        return;
423
    Abc_Print( 1, "Constants { " );
Alan Mishchenko committed
424 425
    Aig_ManForEachObj( p->pAig, pObj, i )
        if ( Ssw_ObjIsConst1Cand( p->pAig, pObj ) )
426
            Abc_Print( 1, "%d(%d,%d,%d) ", pObj->Id, pObj->Level,
Alan Mishchenko committed
427
            Aig_SupportSize(p->pAig,pObj), Aig_NodeMffcSupp(p->pAig,pObj,0,NULL) );
428
    Abc_Print( 1, "}\n" );
Alan Mishchenko committed
429 430
    Ssw_ManForEachClass( p, ppClass, i )
    {
431
        Abc_Print( 1, "%3d (%3d) : ", i, p->pClassSizes[i] );
Alan Mishchenko committed
432 433
        Ssw_ClassesPrintOne( p, ppClass[0] );
    }
434
    Abc_Print( 1, "\n" );
Alan Mishchenko committed
435 436 437 438 439 440 441 442 443 444 445 446 447 448 449 450
}

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

  Synopsis    [Prints simulation classes.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
void Ssw_ClassesRemoveNode( Ssw_Cla_t * p, Aig_Obj_t * pObj )
{
    Aig_Obj_t * pRepr, * pTemp;
Alan Mishchenko committed
451
    assert( p->pClassSizes[pObj->Id] == 0 );
Alan Mishchenko committed
452 453 454
    assert( p->pId2Class[pObj->Id] == NULL );
    pRepr = Aig_ObjRepr( p->pAig, pObj );
    assert( pRepr != NULL );
Alan Mishchenko committed
455
//    Vec_PtrPush( p->vRefined, pObj );
Alan Mishchenko committed
456 457
    if ( Ssw_ObjIsConst1Cand( p->pAig, pObj ) )
    {
Alan Mishchenko committed
458 459
        assert( p->pClassSizes[pRepr->Id] == 0 );
        assert( p->pId2Class[pRepr->Id] == NULL );
Alan Mishchenko committed
460
        Aig_ObjSetRepr( p->pAig, pObj, NULL );
Alan Mishchenko committed
461 462 463
        p->nCands1--;
        return;
    }
Alan Mishchenko committed
464
//    Vec_PtrPush( p->vRefined, pRepr );
Alan Mishchenko committed
465
    Aig_ObjSetRepr( p->pAig, pObj, NULL );
Alan Mishchenko committed
466 467 468 469
    assert( p->pId2Class[pRepr->Id][0] == pRepr );
    assert( p->pClassSizes[pRepr->Id] >= 2 );
    if ( p->pClassSizes[pRepr->Id] == 2 )
    {
Alan Mishchenko committed
470
        p->pId2Class[pRepr->Id] = NULL;
Alan Mishchenko committed
471 472 473 474 475 476 477 478 479 480 481 482 483 484 485 486 487 488 489 490
        p->nClasses--;
        p->pClassSizes[pRepr->Id] = 0;
        p->nLits--;
    }
    else
    {
        int i, k = 0;
        // remove the entry from the class
        Ssw_ClassForEachNode( p, pRepr, pTemp, i )
            if ( pTemp != pObj )
                p->pId2Class[pRepr->Id][k++] = pTemp;
        assert( k + 1 == p->pClassSizes[pRepr->Id] );
        // reduce the class
        p->pClassSizes[pRepr->Id]--;
        p->nLits--;
    }
}

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

Alan Mishchenko committed
491
  Synopsis    [Takes the set of const1 cands and rehashes them using sim info.]
Alan Mishchenko committed
492

Alan Mishchenko committed
493
  Description []
494

Alan Mishchenko committed
495 496 497 498 499
  SideEffects []

  SeeAlso     []

***********************************************************************/
500
int Ssw_ClassesPrepareRehash( Ssw_Cla_t * p, Vec_Ptr_t * vCands, int fConstCorr )
Alan Mishchenko committed
501
{
502
//    Aig_Man_t * pAig = p->pAig;
Alan Mishchenko committed
503 504
    Aig_Obj_t ** ppTable, ** ppNexts, ** ppClassNew;
    Aig_Obj_t * pObj, * pTemp, * pRepr;
Alan Mishchenko committed
505
    int i, k, nTableSize, nNodes, iEntry, nEntries, nEntries2;
Alan Mishchenko committed
506 507

    // allocate the hash table hashing simulation info into nodes
508
    nTableSize = Abc_PrimeCudd( Vec_PtrSize(vCands)/2 );
509 510
    ppTable = ABC_CALLOC( Aig_Obj_t *, nTableSize );
    ppNexts = ABC_CALLOC( Aig_Obj_t *, Aig_ManObjNumMax(p->pAig) );
Alan Mishchenko committed
511

Alan Mishchenko committed
512
    // sort through the candidates
Alan Mishchenko committed
513
    nEntries = 0;
Alan Mishchenko committed
514
    p->nCands1 = 0;
515
    Vec_PtrForEachEntry( Aig_Obj_t *, vCands, pObj, i )
Alan Mishchenko committed
516
    {
Alan Mishchenko committed
517 518
        assert( p->pClassSizes[pObj->Id] == 0 );
        Aig_ObjSetRepr( p->pAig, pObj, NULL );
Alan Mishchenko committed
519 520 521 522 523 524 525
        // check if the node belongs to the class of constant 1
        if ( p->pFuncNodeIsConst( p->pManData, pObj ) )
        {
            Ssw_ObjSetConst1Cand( p->pAig, pObj );
            p->nCands1++;
            continue;
        }
526 527
        if ( fConstCorr )
            continue;
Alan Mishchenko committed
528 529 530 531
        // hash the node by its simulation info
        iEntry = p->pFuncNodeHash( p->pManData, pObj ) % nTableSize;
        // add the node to the class
        if ( ppTable[iEntry] == NULL )
Alan Mishchenko committed
532
        {
Alan Mishchenko committed
533
            ppTable[iEntry] = pObj;
Alan Mishchenko committed
534
        }
Alan Mishchenko committed
535 536 537 538 539 540 541 542 543 544 545 546 547 548 549 550 551 552
        else
        {
            // set the representative of this node
            pRepr = ppTable[iEntry];
            Aig_ObjSetRepr( p->pAig, pObj, pRepr );
            // add node to the table
            if ( Ssw_ObjNext( ppNexts, pRepr ) == NULL )
            { // this will be the second entry
                p->pClassSizes[pRepr->Id]++;
                nEntries++;
            }
            // add the entry to the list
            Ssw_ObjSetNext( ppNexts, pObj, Ssw_ObjNext( ppNexts, pRepr ) );
            Ssw_ObjSetNext( ppNexts, pRepr, pObj );
            p->pClassSizes[pRepr->Id]++;
            nEntries++;
        }
    }
553

Alan Mishchenko committed
554 555
    // copy the entries into storage in the topological order
    nEntries2 = 0;
556
    Vec_PtrForEachEntry( Aig_Obj_t *, vCands, pObj, i )
Alan Mishchenko committed
557 558 559 560 561 562 563
    {
        nNodes = p->pClassSizes[pObj->Id];
        // skip the nodes that are not representatives of non-trivial classes
        if ( nNodes == 0 )
            continue;
        assert( nNodes > 1 );
        // add the nodes to the class in the topological order
Alan Mishchenko committed
564
        ppClassNew = p->pMemClassesFree + nEntries2;
Alan Mishchenko committed
565
        ppClassNew[0] = pObj;
566
        for ( pTemp = Ssw_ObjNext(ppNexts, pObj), k = 1; pTemp;
Alan Mishchenko committed
567 568 569 570 571 572 573 574 575 576
              pTemp = Ssw_ObjNext(ppNexts, pTemp), k++ )
        {
            ppClassNew[nNodes-k] = pTemp;
        }
        // add the class of nodes
        p->pClassSizes[pObj->Id] = 0;
        Ssw_ObjAddClass( p, pObj, ppClassNew, nNodes );
        // increment the number of entries
        nEntries2 += nNodes;
    }
Alan Mishchenko committed
577
    p->pMemClassesFree += nEntries2;
Alan Mishchenko committed
578
    assert( nEntries == nEntries2 );
Alan Mishchenko committed
579 580
    ABC_FREE( ppTable );
    ABC_FREE( ppNexts );
Alan Mishchenko committed
581 582 583 584 585 586 587 588 589 590 591 592 593 594 595
    // now it is time to refine the classes
    return Ssw_ClassesRefine( p, 1 );
}

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

  Synopsis    [Creates initial simulation classes.]

  Description [Assumes that simulation info is assigned.]
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
596
Ssw_Cla_t * Ssw_ClassesPrepare( Aig_Man_t * pAig, int nFramesK, int fLatchCorr, int fConstCorr, int fOutputCorr, int nMaxLevs, int fVerbose )
Alan Mishchenko committed
597 598 599 600 601 602 603 604 605
{
//    int nFrames =  4;
//    int nWords  =  1;
//    int nIters  = 16;

//    int nFrames = 32;
//    int nWords  =  4;
//    int nIters  =  0;

606
    int nFrames =  Abc_MaxInt( nFramesK, 4 );
Alan Mishchenko committed
607 608 609 610 611 612
    int nWords  =  2;
    int nIters  = 16;
    Ssw_Cla_t * p;
    Ssw_Sml_t * pSml;
    Vec_Ptr_t * vCands;
    Aig_Obj_t * pObj;
613
    int i, k, RetValue;
614
    abctime clk;
Alan Mishchenko committed
615 616 617

    // start the classes
    p = Ssw_ClassesStart( pAig );
618
    p->fConstCorr = fConstCorr;
Alan Mishchenko committed
619 620

    // perform sequential simulation
621
clk = Abc_Clock();
Alan Mishchenko committed
622 623 624
    pSml = Ssw_SmlSimulateSeq( pAig, 0, nFrames, nWords );
if ( fVerbose )
{
625
    Abc_Print( 1, "Allocated %.2f MB to store simulation information.\n",
Alan Mishchenko committed
626
        1.0*(sizeof(unsigned) * Aig_ManObjNumMax(pAig) * nFrames * nWords)/(1<<20) );
627
    Abc_Print( 1, "Initial simulation of %d frames with %d words.     ", nFrames, nWords );
628
    ABC_PRT( "Time", Abc_Clock() - clk );
Alan Mishchenko committed
629 630 631
}

    // set comparison procedures
632
clk = Abc_Clock();
633
    Ssw_ClassesSetData( p, pSml, (unsigned(*)(void *,Aig_Obj_t *))Ssw_SmlObjHashWord, (int(*)(void *,Aig_Obj_t *))Ssw_SmlObjIsConstWord, (int(*)(void *,Aig_Obj_t *,Aig_Obj_t *))Ssw_SmlObjsAreEqualWord );
Alan Mishchenko committed
634 635 636 637 638 639 640 641 642 643 644 645

    // collect nodes to be considered as candidates
    vCands = Vec_PtrAlloc( 1000 );
    Aig_ManForEachObj( p->pAig, pObj, i )
    {
        if ( fLatchCorr )
        {
            if ( !Saig_ObjIsLo(p->pAig, pObj) )
                continue;
        }
        else
        {
646
            if ( !Aig_ObjIsNode(pObj) && !Aig_ObjIsCi(pObj) )
Alan Mishchenko committed
647 648 649 650 651 652 653
                continue;
            // skip the node with more that the given number of levels
            if ( nMaxLevs && (int)pObj->Level > nMaxLevs )
                continue;
        }
        Vec_PtrPush( vCands, pObj );
    }
654

655 656 657 658 659 660 661 662 663 664 665 666 667 668 669
    // this change will consider all PO drivers
    if ( fOutputCorr )
    {
        Vec_PtrClear( vCands );
        Aig_ManForEachObj( p->pAig, pObj, i )
            pObj->fMarkB = 0;
        Saig_ManForEachPo( p->pAig, pObj, i )
            if ( Aig_ObjIsCand(Aig_ObjFanin0(pObj)) )
                Aig_ObjFanin0(pObj)->fMarkB = 1;
        Aig_ManForEachObj( p->pAig, pObj, i )
            if ( pObj->fMarkB )
                Vec_PtrPush( vCands, pObj );
        Aig_ManForEachObj( p->pAig, pObj, i )
            pObj->fMarkB = 0;
    }
Alan Mishchenko committed
670 671

    // allocate room for classes
Alan Mishchenko committed
672
    p->pMemClasses = ABC_ALLOC( Aig_Obj_t *, Vec_PtrSize(vCands) );
Alan Mishchenko committed
673
    p->pMemClassesFree = p->pMemClasses;
Alan Mishchenko committed
674

Alan Mishchenko committed
675
    // now it is time to refine the classes
676
    Ssw_ClassesPrepareRehash( p, vCands, fConstCorr );
Alan Mishchenko committed
677 678
if ( fVerbose )
{
679
    Abc_Print( 1, "Collecting candidate equivalence classes.        " );
680
ABC_PRT( "Time", Abc_Clock() - clk );
Alan Mishchenko committed
681 682
}

683
clk = Abc_Clock();
Alan Mishchenko committed
684 685 686
    // perform iterative refinement using simulation
    for ( i = 1; i < nIters; i++ )
    {
Alan Mishchenko committed
687 688 689 690 691 692 693
        // collect const1 candidates
        Vec_PtrClear( vCands );
        Aig_ManForEachObj( p->pAig, pObj, k )
            if ( Ssw_ObjIsConst1Cand( p->pAig, pObj ) )
                Vec_PtrPush( vCands, pObj );
        assert( Vec_PtrSize(vCands) == p->nCands1 );
        // perform new round of simulation
Alan Mishchenko committed
694 695
        Ssw_SmlResimulateSeq( pSml );
        // check equivalence classes
696
        RetValue = Ssw_ClassesPrepareRehash( p, vCands, fConstCorr );
Alan Mishchenko committed
697 698 699
        if ( RetValue == 0 )
            break;
    }
Alan Mishchenko committed
700
    Ssw_SmlStop( pSml );
Alan Mishchenko committed
701
    Vec_PtrFree( vCands );
Alan Mishchenko committed
702 703
if ( fVerbose )
{
704
    Abc_Print( 1, "Simulation of %d frames with %d words (%2d rounds). ",
Alan Mishchenko committed
705
        nFrames, nWords, i-1 );
706
    ABC_PRT( "Time", Abc_Clock() - clk );
Alan Mishchenko committed
707
}
Alan Mishchenko committed
708
    Ssw_ClassesCheck( p );
Alan Mishchenko committed
709
//    Ssw_ClassesPrint( p, 0 );
Alan Mishchenko committed
710
    return p;
Alan Mishchenko committed
711 712 713 714 715 716 717 718 719 720 721 722 723 724 725 726 727 728 729 730 731 732
}

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

  Synopsis    [Creates initial simulation classes.]

  Description [Assumes that simulation info is assigned.]
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
Ssw_Cla_t * Ssw_ClassesPrepareSimple( Aig_Man_t * pAig, int fLatchCorr, int nMaxLevs )
{
    Ssw_Cla_t * p;
    Aig_Obj_t * pObj;
    int i;
    // start the classes
    p = Ssw_ClassesStart( pAig );
    // go through the nodes
    p->nCands1 = 0;
Alan Mishchenko committed
733
    Aig_ManForEachObj( pAig, pObj, i )
Alan Mishchenko committed
734 735 736 737 738 739 740 741 742 743 744
    {
        if ( fLatchCorr )
        {
            if ( !Saig_ObjIsLo(pAig, pObj) )
                continue;
        }
        else
        {
            if ( !Aig_ObjIsNode(pObj) && !Saig_ObjIsLo(pAig, pObj) )
                continue;
            // skip the node with more that the given number of levels
Alan Mishchenko committed
745
            if ( nMaxLevs && (int)pObj->Level > nMaxLevs )
Alan Mishchenko committed
746 747
                continue;
        }
Alan Mishchenko committed
748
        Ssw_ObjSetConst1Cand( pAig, pObj );
Alan Mishchenko committed
749 750 751
        p->nCands1++;
    }
    // allocate room for classes
Alan Mishchenko committed
752
    p->pMemClassesFree = p->pMemClasses = ABC_ALLOC( Aig_Obj_t *, p->nCands1 );
Alan Mishchenko committed
753 754 755 756 757 758 759 760 761
//    Ssw_ClassesPrint( p, 0 );
    return p;
}

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

  Synopsis    [Creates initial simulation classes.]

  Description [Assumes that simulation info is assigned.]
762

Alan Mishchenko committed
763 764 765 766 767
  SideEffects []

  SeeAlso     []

***********************************************************************/
768 769 770 771 772 773 774 775 776 777 778 779 780 781 782 783 784 785 786 787 788 789 790 791 792 793 794 795 796 797 798 799 800 801 802 803 804 805 806 807 808 809 810 811 812 813 814
Ssw_Cla_t * Ssw_ClassesPrepareFromReprs( Aig_Man_t * pAig )
{
    Ssw_Cla_t * p;
    Aig_Obj_t * pObj, * pRepr;
    int * pClassSizes, nEntries, i;
    // start the classes
    p = Ssw_ClassesStart( pAig );
    // allocate memory for classes
    p->pMemClasses = ABC_CALLOC( Aig_Obj_t *, Aig_ManObjNumMax(pAig) );
    // count classes
    p->nCands1 = 0;
    Aig_ManForEachObj( pAig, pObj, i )
    {
        if ( Ssw_ObjIsConst1Cand(pAig, pObj) )
        {
            p->nCands1++;
            continue;
        }
        if ( (pRepr = Aig_ObjRepr(pAig, pObj)) )
        {
            if ( p->pClassSizes[pRepr->Id]++ == 0 )
                p->pClassSizes[pRepr->Id]++;
        }
    }
    // add nodes
    nEntries = 0;
    p->nClasses = 0;
    pClassSizes = ABC_CALLOC( int, Aig_ManObjNumMax(pAig) );
    Aig_ManForEachObj( pAig, pObj, i )
    {
        if ( p->pClassSizes[i] )
        {
            p->pId2Class[i] = p->pMemClasses + nEntries;
            nEntries += p->pClassSizes[i];
            p->pId2Class[i][pClassSizes[i]++] = pObj;
            p->nClasses++;
            continue;
        }
        if ( Ssw_ObjIsConst1Cand(pAig, pObj) )
            continue;
        if ( (pRepr = Aig_ObjRepr(pAig, pObj)) )
            p->pId2Class[pRepr->Id][pClassSizes[pRepr->Id]++] = pObj;
    }
    p->pMemClassesFree = p->pMemClasses + nEntries;
    p->nLits = nEntries - p->nClasses;
    assert( memcmp(pClassSizes, p->pClassSizes, sizeof(int)*Aig_ManObjNumMax(pAig)) == 0 );
    ABC_FREE( pClassSizes );
815
//    Abc_Print( 1, "After converting:\n" );
816 817 818 819 820 821 822 823 824 825 826 827 828 829 830
//    Ssw_ClassesPrint( p, 0 );
    return p;
}

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

  Synopsis    [Creates initial simulation classes.]

  Description [Assumes that simulation info is assigned.]
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
Alan Mishchenko committed
831 832 833 834 835 836 837 838 839 840 841 842 843 844 845
Ssw_Cla_t * Ssw_ClassesPrepareTargets( Aig_Man_t * pAig )
{
    Ssw_Cla_t * p;
    Aig_Obj_t * pObj;
    int i;
    // start the classes
    p = Ssw_ClassesStart( pAig );
    // go through the nodes
    p->nCands1 = 0;
    Saig_ManForEachPo( pAig, pObj, i )
    {
        Ssw_ObjSetConst1Cand( pAig, Aig_ObjFanin0(pObj) );
        p->nCands1++;
    }
    // allocate room for classes
Alan Mishchenko committed
846
    p->pMemClassesFree = p->pMemClasses = ABC_ALLOC( Aig_Obj_t *, p->nCands1 );
Alan Mishchenko committed
847 848 849 850 851 852
//    Ssw_ClassesPrint( p, 0 );
    return p;
}

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

Alan Mishchenko committed
853 854 855 856 857 858 859 860 861 862 863 864 865 866 867 868 869 870 871 872
  Synopsis    [Creates classes from the temporary representation.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
Ssw_Cla_t * Ssw_ClassesPreparePairs( Aig_Man_t * pAig, Vec_Int_t ** pvClasses )
{
    Ssw_Cla_t * p;
    Aig_Obj_t ** ppClassNew;
    Aig_Obj_t * pObj, * pRepr, * pPrev;
    int i, k, nTotalObjs, nEntries, Entry;
    // start the classes
    p = Ssw_ClassesStart( pAig );
    // count the number of entries in the classes
    nTotalObjs = 0;
    for ( i = 0; i < Aig_ManObjNumMax(pAig); i++ )
873
        nTotalObjs += pvClasses[i] ? Vec_IntSize(pvClasses[i]) : 0;
Alan Mishchenko committed
874
    // allocate memory for classes
Alan Mishchenko committed
875
    p->pMemClasses = ABC_ALLOC( Aig_Obj_t *, nTotalObjs );
Alan Mishchenko committed
876 877 878 879 880 881 882 883 884 885 886 887 888 889 890 891 892 893 894 895 896 897 898 899 900 901 902 903 904 905 906 907 908 909 910 911 912 913 914 915 916 917 918
    // create constant-1 class
    if ( pvClasses[0] )
    Vec_IntForEachEntry( pvClasses[0], Entry, i )
    {
        assert( (i == 0) == (Entry == 0) );
        if ( i == 0 )
            continue;
        pObj = Aig_ManObj( pAig, Entry );
        Ssw_ObjSetConst1Cand( pAig, pObj );
        p->nCands1++;
    }
    // create classes
    nEntries = 0;
    for ( i = 1; i < Aig_ManObjNumMax(pAig); i++ )
    {
        if ( pvClasses[i] == NULL )
            continue;
        // get room for storing the class
        ppClassNew = p->pMemClasses + nEntries;
        nEntries  += Vec_IntSize( pvClasses[i] );
        // store the nodes of the class
        pPrev = pRepr = Aig_ManObj( pAig, Vec_IntEntry(pvClasses[i],0) );
        ppClassNew[0] = pRepr;
        Vec_IntForEachEntryStart( pvClasses[i], Entry, k, 1 )
        {
            pObj = Aig_ManObj( pAig, Entry );
            assert( pPrev->Id < pObj->Id );
            pPrev = pObj;
            ppClassNew[k] = pObj;
            Aig_ObjSetRepr( pAig, pObj, pRepr );
        }
        // create new class
        Ssw_ObjAddClass( p, pRepr, ppClassNew, Vec_IntSize(pvClasses[i]) );
    }
    // prepare room for new classes
    p->pMemClassesFree = p->pMemClasses + nEntries;
    Ssw_ClassesCheck( p );
//    Ssw_ClassesPrint( p, 0 );
    return p;
}

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

Alan Mishchenko committed
919 920 921
  Synopsis    [Creates classes from the temporary representation.]

  Description []
922

Alan Mishchenko committed
923 924 925 926 927
  SideEffects []

  SeeAlso     []

***********************************************************************/
Alan Mishchenko committed
928
Ssw_Cla_t * Ssw_ClassesPreparePairsSimple( Aig_Man_t * pMiter, Vec_Int_t * vPairs )
Alan Mishchenko committed
929 930 931 932 933 934 935 936
{
    Ssw_Cla_t * p;
    Aig_Obj_t ** ppClassNew;
    Aig_Obj_t * pObj, * pRepr;
    int i;
    // start the classes
    p = Ssw_ClassesStart( pMiter );
    // allocate memory for classes
Alan Mishchenko committed
937
    p->pMemClasses = ABC_ALLOC( Aig_Obj_t *, Vec_IntSize(vPairs) );
Alan Mishchenko committed
938 939 940 941 942 943 944 945 946 947 948 949 950 951 952 953 954 955 956 957 958 959 960
    // create classes
    for ( i = 0; i < Vec_IntSize(vPairs); i += 2 )
    {
        pRepr = Aig_ManObj( pMiter, Vec_IntEntry(vPairs, i) );
        pObj  = Aig_ManObj( pMiter, Vec_IntEntry(vPairs, i+1) );
        assert( Aig_ObjId(pRepr) < Aig_ObjId(pObj) );
        Aig_ObjSetRepr( pMiter, pObj, pRepr );
        // get room for storing the class
        ppClassNew = p->pMemClasses + i;
        ppClassNew[0] = pRepr;
        ppClassNew[1] = pObj;
        // create new class
        Ssw_ObjAddClass( p, pRepr, ppClassNew, 2 );
    }
    // prepare room for new classes
    p->pMemClassesFree = NULL;
    Ssw_ClassesCheck( p );
//    Ssw_ClassesPrint( p, 0 );
    return p;
}

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

Alan Mishchenko committed
961 962 963
  Synopsis    [Iteratively refines the classes after simulation.]

  Description [Returns the number of refinements performed.]
964

Alan Mishchenko committed
965 966 967 968 969 970 971 972 973
  SideEffects []

  SeeAlso     []

***********************************************************************/
int Ssw_ClassesRefineOneClass( Ssw_Cla_t * p, Aig_Obj_t * pReprOld, int fRecursive )
{
    Aig_Obj_t ** pClassOld, ** pClassNew;
    Aig_Obj_t * pObj, * pReprNew;
974
    int i;
Alan Mishchenko committed
975 976 977 978 979 980 981 982 983 984 985 986

    // split the class
    Vec_PtrClear( p->vClassOld );
    Vec_PtrClear( p->vClassNew );
    Ssw_ClassForEachNode( p, pReprOld, pObj, i )
        if ( p->pFuncNodesAreEqual(p->pManData, pReprOld, pObj) )
            Vec_PtrPush( p->vClassOld, pObj );
        else
            Vec_PtrPush( p->vClassNew, pObj );
    // check if splitting happened
    if ( Vec_PtrSize(p->vClassNew) == 0 )
        return 0;
Alan Mishchenko committed
987
    // remember that this class is refined
Alan Mishchenko committed
988 989
//    Ssw_ClassForEachNode( p, pReprOld, pObj, i )
//        Vec_PtrPush( p->vRefined, pObj );
Alan Mishchenko committed
990 991

    // get the new representative
992
    pReprNew = (Aig_Obj_t *)Vec_PtrEntry( p->vClassNew, 0 );
Alan Mishchenko committed
993 994 995 996 997
    assert( Vec_PtrSize(p->vClassOld) > 0 );
    assert( Vec_PtrSize(p->vClassNew) > 0 );

    // create old class
    pClassOld = Ssw_ObjRemoveClass( p, pReprOld );
998
    Vec_PtrForEachEntry( Aig_Obj_t *, p->vClassOld, pObj, i )
Alan Mishchenko committed
999 1000 1001 1002 1003 1004
    {
        pClassOld[i] = pObj;
        Aig_ObjSetRepr( p->pAig, pObj, i? pReprOld : NULL );
    }
    // create new class
    pClassNew = pClassOld + i;
1005
    Vec_PtrForEachEntry( Aig_Obj_t *, p->vClassNew, pObj, i )
Alan Mishchenko committed
1006 1007 1008 1009 1010 1011 1012 1013 1014 1015 1016 1017 1018 1019 1020 1021 1022 1023 1024 1025 1026 1027
    {
        pClassNew[i] = pObj;
        Aig_ObjSetRepr( p->pAig, pObj, i? pReprNew : NULL );
    }

    // put classes back
    if ( Vec_PtrSize(p->vClassOld) > 1 )
        Ssw_ObjAddClass( p, pReprOld, pClassOld, Vec_PtrSize(p->vClassOld) );
    if ( Vec_PtrSize(p->vClassNew) > 1 )
        Ssw_ObjAddClass( p, pReprNew, pClassNew, Vec_PtrSize(p->vClassNew) );

    // check if the class should be recursively refined
    if ( fRecursive && Vec_PtrSize(p->vClassNew) > 1 )
        return 1 + Ssw_ClassesRefineOneClass( p, pReprNew, 1 );
    return 1;
}

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

  Synopsis    [Refines the classes after simulation.]

  Description []
1028

Alan Mishchenko committed
1029 1030 1031 1032 1033
  SideEffects []

  SeeAlso     []

***********************************************************************/
Alan Mishchenko committed
1034
int Ssw_ClassesRefine( Ssw_Cla_t * p, int fRecursive )
Alan Mishchenko committed
1035 1036 1037 1038
{
    Aig_Obj_t ** ppClass;
    int i, nRefis = 0;
    Ssw_ManForEachClass( p, ppClass, i )
Alan Mishchenko committed
1039
        nRefis += Ssw_ClassesRefineOneClass( p, ppClass[0], fRecursive );
Alan Mishchenko committed
1040 1041 1042 1043 1044
    return nRefis;
}

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

1045 1046 1047
  Synopsis    [Refines the classes after simulation.]

  Description []
1048

1049 1050 1051 1052 1053 1054 1055 1056 1057 1058 1059 1060 1061 1062 1063 1064
  SideEffects []

  SeeAlso     []

***********************************************************************/
int Ssw_ClassesRefineGroup( Ssw_Cla_t * p, Vec_Ptr_t * vReprs, int fRecursive )
{
    Aig_Obj_t * pObj;
    int i, nRefis = 0;
    Vec_PtrForEachEntry( Aig_Obj_t *, vReprs, pObj, i )
        nRefis += Ssw_ClassesRefineOneClass( p, pObj, fRecursive );
    return nRefis;
}

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

Alan Mishchenko committed
1065 1066 1067
  Synopsis    [Refine the group of constant 1 nodes.]

  Description []
1068

Alan Mishchenko committed
1069 1070 1071 1072 1073 1074 1075 1076 1077 1078 1079 1080 1081
  SideEffects []

  SeeAlso     []

***********************************************************************/
int Ssw_ClassesRefineConst1Group( Ssw_Cla_t * p, Vec_Ptr_t * vRoots, int fRecursive )
{
    Aig_Obj_t * pObj, * pReprNew, ** ppClassNew;
    int i;
    if ( Vec_PtrSize(vRoots) == 0 )
        return 0;
    // collect the nodes to be refined
    Vec_PtrClear( p->vClassNew );
1082
    Vec_PtrForEachEntry( Aig_Obj_t *, vRoots, pObj, i )
Alan Mishchenko committed
1083 1084 1085 1086 1087 1088
        if ( !p->pFuncNodeIsConst( p->pManData, pObj ) )
            Vec_PtrPush( p->vClassNew, pObj );
    // check if there is a new class
    if ( Vec_PtrSize(p->vClassNew) == 0 )
        return 0;
    p->nCands1 -= Vec_PtrSize(p->vClassNew);
1089
    pReprNew = (Aig_Obj_t *)Vec_PtrEntry( p->vClassNew, 0 );
Alan Mishchenko committed
1090 1091 1092 1093 1094 1095
    Aig_ObjSetRepr( p->pAig, pReprNew, NULL );
    if ( Vec_PtrSize(p->vClassNew) == 1 )
        return 1;
    // create a new class composed of these nodes
    ppClassNew = p->pMemClassesFree;
    p->pMemClassesFree += Vec_PtrSize(p->vClassNew);
1096
    Vec_PtrForEachEntry( Aig_Obj_t *, p->vClassNew, pObj, i )
Alan Mishchenko committed
1097 1098 1099 1100 1101 1102 1103 1104 1105 1106 1107
    {
        ppClassNew[i] = pObj;
        Aig_ObjSetRepr( p->pAig, pObj, i? pReprNew : NULL );
    }
    Ssw_ObjAddClass( p, pReprNew, ppClassNew, Vec_PtrSize(p->vClassNew) );
    // refine them recursively
    if ( fRecursive )
        return 1 + Ssw_ClassesRefineOneClass( p, pReprNew, 1 );
    return 1;
}

Alan Mishchenko committed
1108 1109 1110 1111 1112
/**Function*************************************************************

  Synopsis    [Refine the group of constant 1 nodes.]

  Description []
1113

Alan Mishchenko committed
1114 1115 1116 1117 1118 1119 1120 1121 1122 1123 1124 1125 1126 1127 1128 1129
  SideEffects []

  SeeAlso     []

***********************************************************************/
int Ssw_ClassesRefineConst1( Ssw_Cla_t * p, int fRecursive )
{
    Aig_Obj_t * pObj, * pReprNew, ** ppClassNew;
    int i;
    // collect the nodes to be refined
    Vec_PtrClear( p->vClassNew );
    for ( i = 0; i < Vec_PtrSize(p->pAig->vObjs); i++ )
        if ( p->pAig->pReprs[i] == Aig_ManConst1(p->pAig) )
        {
            pObj = Aig_ManObj( p->pAig, i );
            if ( !p->pFuncNodeIsConst( p->pManData, pObj ) )
Alan Mishchenko committed
1130
            {
Alan Mishchenko committed
1131
                Vec_PtrPush( p->vClassNew, pObj );
Alan Mishchenko committed
1132
//                Vec_PtrPush( p->vRefined, pObj );
Alan Mishchenko committed
1133
            }
Alan Mishchenko committed
1134 1135 1136 1137
        }
    // check if there is a new class
    if ( Vec_PtrSize(p->vClassNew) == 0 )
        return 0;
1138 1139 1140 1141 1142 1143
    if ( p->fConstCorr )
    {
        Vec_PtrForEachEntry( Aig_Obj_t *, p->vClassNew, pObj, i )
            Aig_ObjSetRepr( p->pAig, pObj, NULL );
        return 1;
    }
Alan Mishchenko committed
1144
    p->nCands1 -= Vec_PtrSize(p->vClassNew);
1145
    pReprNew = (Aig_Obj_t *)Vec_PtrEntry( p->vClassNew, 0 );
Alan Mishchenko committed
1146 1147 1148 1149 1150 1151
    Aig_ObjSetRepr( p->pAig, pReprNew, NULL );
    if ( Vec_PtrSize(p->vClassNew) == 1 )
        return 1;
    // create a new class composed of these nodes
    ppClassNew = p->pMemClassesFree;
    p->pMemClassesFree += Vec_PtrSize(p->vClassNew);
1152
    Vec_PtrForEachEntry( Aig_Obj_t *, p->vClassNew, pObj, i )
Alan Mishchenko committed
1153 1154 1155 1156 1157 1158 1159 1160 1161 1162 1163
    {
        ppClassNew[i] = pObj;
        Aig_ObjSetRepr( p->pAig, pObj, i? pReprNew : NULL );
    }
    Ssw_ObjAddClass( p, pReprNew, ppClassNew, Vec_PtrSize(p->vClassNew) );
    // refine them recursively
    if ( fRecursive )
        return 1 + Ssw_ClassesRefineOneClass( p, pReprNew, 1 );
    return 1;
}

Alan Mishchenko committed
1164 1165 1166 1167 1168 1169

////////////////////////////////////////////////////////////////////////
///                       END OF FILE                                ///
////////////////////////////////////////////////////////////////////////


1170
ABC_NAMESPACE_IMPL_END