Major restructuring of the code.

1 files changed, 0 insertions, 862 deletions

diff --git a/src/aig/fra/fraClass.c b/src/aig/fra/fraClass.c
deleted file mode 100644
index 8cf2a54d..00000000
--- a/src/aig/fra/fraClass.c
+++ /dev/null
@@ -1,862 +0,0 @@
-/**CFile****************************************************************
-
-  FileName    [fraClass.c]
-
-  SystemName  [ABC: Logic synthesis and verification system.]
-
-  PackageName [New FRAIG package.]
-
-  Synopsis    []
-
-  Author      [Alan Mishchenko]
-  
-  Affiliation [UC Berkeley]
-
-  Date        [Ver. 1.0. Started - June 30, 2007.]
-
-  Revision    [$Id: fraClass.c,v 1.00 2007/06/30 00:00:00 alanmi Exp $]
-
-***********************************************************************/
-
-#include "fra.h"
-
-ABC_NAMESPACE_IMPL_START
-
-
-/*
-    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 topological order of their representatives.
-    The array of pointers to the class nodes is terminated with a NULL pointer.
-    To enable dynamic addition of new classes (during class refinement),
-    each array has at least as many NULLs in the end, as there are nodes in the class.
-*/
-
-////////////////////////////////////////////////////////////////////////
-///                        DECLARATIONS                              ///
-////////////////////////////////////////////////////////////////////////
-
-static inline Aig_Obj_t *  Fra_ObjNext( Aig_Obj_t ** ppNexts, Aig_Obj_t * pObj )                       { return ppNexts[pObj->Id];  }
-static inline void         Fra_ObjSetNext( Aig_Obj_t ** ppNexts, Aig_Obj_t * pObj, Aig_Obj_t * pNext ) { ppNexts[pObj->Id] = pNext; }
-
-////////////////////////////////////////////////////////////////////////
-///                     FUNCTION DEFINITIONS                         ///
-////////////////////////////////////////////////////////////////////////
-
-/**Function*************************************************************
-
-  Synopsis    [Starts representation of equivalence classes.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-Fra_Cla_t * Fra_ClassesStart( Aig_Man_t * pAig )
-{
-    Fra_Cla_t * p;
-    p = ABC_ALLOC( Fra_Cla_t, 1 );
-    memset( p, 0, sizeof(Fra_Cla_t) );
-    p->pAig = pAig;
-    p->pMemRepr  = ABC_ALLOC( Aig_Obj_t *, Aig_ManObjNumMax(pAig) );
-    memset( p->pMemRepr, 0, sizeof(Aig_Obj_t *) * Aig_ManObjNumMax(pAig) );
-    p->vClasses     = Vec_PtrAlloc( 100 );
-    p->vClasses1    = Vec_PtrAlloc( 100 );
-    p->vClassesTemp = Vec_PtrAlloc( 100 );
-    p->vClassOld    = Vec_PtrAlloc( 100 );
-    p->vClassNew    = Vec_PtrAlloc( 100 );
-    p->pFuncNodeHash      = Fra_SmlNodeHash;
-    p->pFuncNodeIsConst   = Fra_SmlNodeIsConst;
-    p->pFuncNodesAreEqual = Fra_SmlNodesAreEqual;
-    return p;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Stop representation of equivalence classes.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Fra_ClassesStop( Fra_Cla_t * p )
-{
-    ABC_FREE( p->pMemClasses );
-    ABC_FREE( p->pMemRepr );
-    if ( p->vClassesTemp ) Vec_PtrFree( p->vClassesTemp );
-    if ( p->vClassNew )    Vec_PtrFree( p->vClassNew );
-    if ( p->vClassOld )    Vec_PtrFree( p->vClassOld );
-    if ( p->vClasses1 )    Vec_PtrFree( p->vClasses1 );
-    if ( p->vClasses )     Vec_PtrFree( p->vClasses );
-    if ( p->vImps )        Vec_IntFree( p->vImps );
-    ABC_FREE( p );
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Starts representation of equivalence classes.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Fra_ClassesCopyReprs( Fra_Cla_t * p, Vec_Ptr_t * vFailed )
-{
-    Aig_Obj_t * pObj;
-    int i;
-    Aig_ManReprStart( p->pAig, Aig_ManObjNumMax(p->pAig) );
-    memmove( p->pAig->pReprs, p->pMemRepr, sizeof(Aig_Obj_t *) * Aig_ManObjNumMax(p->pAig) );
-    if ( Vec_PtrSize(p->vClasses1) == 0 && Vec_PtrSize(p->vClasses) == 0 )
-    {
-        Aig_ManForEachObj( p->pAig, pObj, i )
-        {
-            if ( p->pAig->pReprs[i] != NULL )
-                printf( "Classes are not cleared!\n" );
-            assert( p->pAig->pReprs[i] == NULL );
-        }
-    }
-    if ( vFailed )
-        Vec_PtrForEachEntry( Aig_Obj_t *, vFailed, pObj, i )
-            p->pAig->pReprs[pObj->Id] = NULL;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Prints simulation classes.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-int Fra_ClassCount( Aig_Obj_t ** pClass )
-{
-    Aig_Obj_t * pTemp;
-    int i;
-    for ( i = 0; (pTemp = pClass[i]); i++ );
-    return i;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Count the number of literals.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-int Fra_ClassesCountLits( Fra_Cla_t * p )
-{
-    Aig_Obj_t ** pClass;
-    int i, nNodes, nLits = 0;
-    nLits = Vec_PtrSize( p->vClasses1 );
-    Vec_PtrForEachEntry( Aig_Obj_t **, p->vClasses, pClass, i )
-    {
-        nNodes = Fra_ClassCount( pClass );
-        assert( nNodes > 1 );
-        nLits += nNodes - 1;
-    }
-    return nLits;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Count the number of pairs.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-int Fra_ClassesCountPairs( Fra_Cla_t * p )
-{
-    Aig_Obj_t ** pClass;
-    int i, nNodes, nPairs = 0;
-    Vec_PtrForEachEntry( Aig_Obj_t **, p->vClasses, pClass, i )
-    {
-        nNodes = Fra_ClassCount( pClass );
-        assert( nNodes > 1 );
-        nPairs += nNodes * (nNodes - 1) / 2;
-    }
-    return nPairs;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Prints simulation classes.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Fra_PrintClass( Fra_Cla_t * p, Aig_Obj_t ** pClass )
-{
-    Aig_Obj_t * pTemp;
-    int i;
-    for ( i = 1; (pTemp = pClass[i]); i++ )
-        assert( Fra_ClassObjRepr(pTemp) == pClass[0] );
-    printf( "{ " );
-    for ( i = 0; (pTemp = pClass[i]); i++ )
-        printf( "%d(%d,%d) ", pTemp->Id, pTemp->Level, Aig_SupportSize(p->pAig,pTemp) );
-    printf( "}\n" );
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Prints simulation classes.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Fra_ClassesPrint( Fra_Cla_t * p, int fVeryVerbose )
-{
-    Aig_Obj_t ** pClass;
-    Aig_Obj_t * pObj;
-    int i;
-
-    printf( "Const = %5d. Class = %5d. Lit = %5d. ", 
-        Vec_PtrSize(p->vClasses1), Vec_PtrSize(p->vClasses), Fra_ClassesCountLits(p) );
-    if ( p->vImps && Vec_IntSize(p->vImps) > 0 )
-        printf( "Imp = %5d. ", Vec_IntSize(p->vImps) );
-    printf( "\n" );
-
-    if ( fVeryVerbose )
-    {
-        Vec_PtrForEachEntry( Aig_Obj_t *, p->vClasses1, pObj, i )
-            assert( Fra_ClassObjRepr(pObj) == Aig_ManConst1(p->pAig) );
-        printf( "Constants { " );
-        Vec_PtrForEachEntry( Aig_Obj_t *, p->vClasses1, pObj, i )
-            printf( "%d(%d,%d) ", pObj->Id, pObj->Level, Aig_SupportSize(p->pAig,pObj) );
-        printf( "}\n" );
-        Vec_PtrForEachEntry( Aig_Obj_t **, p->vClasses, pClass, i )
-        {
-            printf( "%3d (%3d) : ", i, Fra_ClassCount(pClass) );
-            Fra_PrintClass( p, pClass );
-        }
-        printf( "\n" );
-    }
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Creates initial simulation classes.]
-
-  Description [Assumes that simulation info is assigned.]
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Fra_ClassesPrepare( Fra_Cla_t * p, int fLatchCorr, int nMaxLevs )
-{
-    Aig_Obj_t ** ppTable, ** ppNexts;
-    Aig_Obj_t * pObj, * pTemp;
-    int i, k, nTableSize, nEntries, nNodes, iEntry;
-
-    // allocate the hash table hashing simulation info into nodes
-    nTableSize = Aig_PrimeCudd( Aig_ManObjNumMax(p->pAig) );
-    ppTable = ABC_FALLOC( Aig_Obj_t *, nTableSize ); 
-    ppNexts = ABC_FALLOC( Aig_Obj_t *, nTableSize ); 
-    memset( ppTable, 0, sizeof(Aig_Obj_t *) * nTableSize );
-
-    // add all the nodes to the hash table
-    Vec_PtrClear( p->vClasses1 );
-    Aig_ManForEachObj( p->pAig, pObj, i )
-    {
-        if ( fLatchCorr )
-        {
-            if ( !Aig_ObjIsPi(pObj) )
-                continue;
-        }
-        else
-        {
-            if ( !Aig_ObjIsNode(pObj) && !Aig_ObjIsPi(pObj) )
-                continue;
-            // skip the node with more that the given number of levels
-            if ( nMaxLevs && (int)pObj->Level > nMaxLevs )
-                continue;
-        }
-        // hash the node by its simulation info
-        iEntry = p->pFuncNodeHash( pObj, nTableSize );
-        // check if the node belongs to the class of constant 1
-        if ( p->pFuncNodeIsConst( pObj ) )
-        {
-            Vec_PtrPush( p->vClasses1, pObj );
-            Fra_ClassObjSetRepr( pObj, Aig_ManConst1(p->pAig) );
-            continue;
-        }
-        // add the node to the class
-        if ( ppTable[iEntry] == NULL )
-        {
-            ppTable[iEntry] = pObj;
-            Fra_ObjSetNext( ppNexts, pObj, pObj );
-        }
-        else
-        {
-            Fra_ObjSetNext( ppNexts, pObj, Fra_ObjNext(ppNexts,ppTable[iEntry]) );
-            Fra_ObjSetNext( ppNexts, ppTable[iEntry], pObj );
-        }
-    }
-
-    // count the total number of nodes in the non-trivial classes
-    // mark the representative nodes of each equivalence class
-    nEntries = 0;
-    for ( i = 0; i < nTableSize; i++ )
-        if ( ppTable[i] && ppTable[i] != Fra_ObjNext(ppNexts, ppTable[i]) )
-        {
-            for ( pTemp = Fra_ObjNext(ppNexts, ppTable[i]), k = 1; 
-                  pTemp != ppTable[i]; 
-                  pTemp = Fra_ObjNext(ppNexts, pTemp), k++ );
-            assert( k > 1 );
-            nEntries += k;
-            // mark the node
-            assert( ppTable[i]->fMarkA == 0 );
-            ppTable[i]->fMarkA = 1;
-        }
-
-    // allocate room for classes
-    p->pMemClasses = ABC_ALLOC( Aig_Obj_t *, 2*(nEntries + Vec_PtrSize(p->vClasses1)) );
-    p->pMemClassesFree = p->pMemClasses + 2*nEntries;
- 
-    // copy the entries into storage in the topological order
-    Vec_PtrClear( p->vClasses );
-    nEntries = 0;
-    Aig_ManForEachObj( p->pAig, pObj, i )
-    {
-        if ( !Aig_ObjIsNode(pObj) && !Aig_ObjIsPi(pObj) )
-            continue;
-        // skip the nodes that are not representatives of non-trivial classes
-        if ( pObj->fMarkA == 0 )
-            continue;
-        pObj->fMarkA = 0;
-        // add the class of nodes
-        Vec_PtrPush( p->vClasses, p->pMemClasses + 2*nEntries );
-        // count the number of entries in this class
-        for ( pTemp = Fra_ObjNext(ppNexts, pObj), k = 1; 
-              pTemp != pObj; 
-              pTemp = Fra_ObjNext(ppNexts, pTemp), k++ );
-        nNodes = k;
-        assert( nNodes > 1 );
-        // add the nodes to the class in the topological order
-        p->pMemClasses[2*nEntries] = pObj;
-        for ( pTemp = Fra_ObjNext(ppNexts, pObj), k = 1; 
-              pTemp != pObj; 
-              pTemp = Fra_ObjNext(ppNexts, pTemp), k++ )
-        {
-            p->pMemClasses[2*nEntries+nNodes-k] = pTemp;
-            Fra_ClassObjSetRepr( pTemp, pObj );
-        }
-        // add as many empty entries
-        p->pMemClasses[2*nEntries + nNodes] = NULL;
-        // increment the number of entries
-        nEntries += k;
-    }
-    ABC_FREE( ppTable );
-    ABC_FREE( ppNexts );
-    // now it is time to refine the classes
-    Fra_ClassesRefine( p );
-//    Fra_ClassesPrint( p, 0 );
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Refines one class using simulation info.]
-
-  Description [Returns the new class if refinement happened.]
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-Aig_Obj_t ** Fra_RefineClassOne( Fra_Cla_t * p, Aig_Obj_t ** ppClass )
-{
-    Aig_Obj_t * pObj, ** ppThis;
-    int i;
-    assert( ppClass[0] != NULL && ppClass[1] != NULL );
-
-    // check if the class is going to be refined
-    for ( ppThis = ppClass + 1; (pObj = *ppThis); ppThis++ )        
-        if ( !p->pFuncNodesAreEqual(ppClass[0], pObj) )
-            break;
-    if ( pObj == NULL )
-        return NULL;
-    // split the class
-    Vec_PtrClear( p->vClassOld );
-    Vec_PtrClear( p->vClassNew );
-    Vec_PtrPush( p->vClassOld, ppClass[0] );
-    for ( ppThis = ppClass + 1; (pObj = *ppThis); ppThis++ )        
-        if ( p->pFuncNodesAreEqual(ppClass[0], pObj) )
-            Vec_PtrPush( p->vClassOld, pObj );
-        else
-            Vec_PtrPush( p->vClassNew, pObj );
-/*
-    printf( "Refining class (" );
-    Vec_PtrForEachEntry( Aig_Obj_t *, p->vClassOld, pObj, i )
-        printf( "%d,", pObj->Id );
-    printf( ") + (" );
-    Vec_PtrForEachEntry( Aig_Obj_t *, p->vClassNew, pObj, i )
-        printf( "%d,", pObj->Id );
-    printf( ")\n" );
-*/
-    // put the nodes back into the class memory
-    Vec_PtrForEachEntry( Aig_Obj_t *, p->vClassOld, pObj, i )
-    {
-        ppClass[i] = pObj;
-        ppClass[Vec_PtrSize(p->vClassOld)+i] = NULL;
-        Fra_ClassObjSetRepr( pObj, i? ppClass[0] : NULL );
-    }
-    ppClass += 2*Vec_PtrSize(p->vClassOld);
-    // put the new nodes into the class memory
-    Vec_PtrForEachEntry( Aig_Obj_t *, p->vClassNew, pObj, i )
-    {
-        ppClass[i] = pObj;
-        ppClass[Vec_PtrSize(p->vClassNew)+i] = NULL;
-        Fra_ClassObjSetRepr( pObj, i? ppClass[0] : NULL );
-    }
-    return ppClass;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Iteratively refines the classes after simulation.]
-
-  Description [Returns the number of refinements performed.]
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-int Fra_RefineClassLastIter( Fra_Cla_t * p, Vec_Ptr_t * vClasses )
-{
-    Aig_Obj_t ** pClass, ** pClass2;
-    int nRefis;
-    pClass = (Aig_Obj_t **)Vec_PtrEntryLast( vClasses );
-    for ( nRefis = 0; (pClass2 = Fra_RefineClassOne( p, pClass )); nRefis++ )
-    {
-        // if the original class is trivial, remove it
-        if ( pClass[1] == NULL )
-            Vec_PtrPop( vClasses );
-        // if the new class is trivial, stop
-        if ( pClass2[1] == NULL )
-        {
-            nRefis++;
-            break;
-        }
-        // othewise, add the class and continue
-        assert( pClass2[0] != NULL );
-        Vec_PtrPush( vClasses, pClass2 );
-        pClass = pClass2;
-    }
-    return nRefis;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Refines the classes after simulation.]
-
-  Description [Assumes that simulation info is assigned. Returns the
-  number of classes refined.]
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-int Fra_ClassesRefine( Fra_Cla_t * p )
-{
-    Vec_Ptr_t * vTemp;
-    Aig_Obj_t ** pClass;
-    int i, nRefis;
-    // refine the classes
-    nRefis = 0;
-    Vec_PtrClear( p->vClassesTemp );
-    Vec_PtrForEachEntry( Aig_Obj_t **, p->vClasses, pClass, i )
-    {
-        // add the class to the new array
-        assert( pClass[0] != NULL );
-        Vec_PtrPush( p->vClassesTemp, pClass );
-        // refine the class iteratively
-        nRefis += Fra_RefineClassLastIter( p, p->vClassesTemp );
-    }
-    // exchange the class representation
-    vTemp = p->vClassesTemp;
-    p->vClassesTemp = p->vClasses;
-    p->vClasses = vTemp;
-    return nRefis;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Refines constant 1 equivalence class.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-int Fra_ClassesRefine1( Fra_Cla_t * p, int fRefineNewClass, int * pSkipped )
-{
-    Aig_Obj_t * pObj, ** ppClass;
-    int i, k, nRefis = 1;
-    // check if there is anything to refine
-    if ( Vec_PtrSize(p->vClasses1) == 0 )
-        return 0;
-    // make sure constant 1 class contains only non-constant nodes
-    assert( Vec_PtrEntry(p->vClasses1,0) != Aig_ManConst1(p->pAig) );
-    // collect all the nodes to be refined
-    k = 0;
-    Vec_PtrClear( p->vClassNew );
-    Vec_PtrForEachEntry( Aig_Obj_t *, p->vClasses1, pObj, i )
-    {
-        if ( p->pFuncNodeIsConst( pObj ) )
-            Vec_PtrWriteEntry( p->vClasses1, k++, pObj );
-        else 
-            Vec_PtrPush( p->vClassNew, pObj );
-    }
-    Vec_PtrShrink( p->vClasses1, k );
-    if ( Vec_PtrSize(p->vClassNew) == 0 )
-        return 0;
-/*
-    printf( "Refined const-1 class: {" );
-    Vec_PtrForEachEntry( Aig_Obj_t *, p->vClassNew, pObj, i )
-        printf( " %d", pObj->Id );
-    printf( " }\n" );
-*/
-    if ( Vec_PtrSize(p->vClassNew) == 1 )
-    {
-        Fra_ClassObjSetRepr( (Aig_Obj_t *)Vec_PtrEntry(p->vClassNew,0), NULL );
-        return 1;
-    }
-    // create a new class composed of these nodes
-    ppClass = p->pMemClassesFree;
-    p->pMemClassesFree += 2 * Vec_PtrSize(p->vClassNew);
-    Vec_PtrForEachEntry( Aig_Obj_t *, p->vClassNew, pObj, i )
-    {
-        ppClass[i] = pObj;
-        ppClass[Vec_PtrSize(p->vClassNew)+i] = NULL;
-        Fra_ClassObjSetRepr( pObj, i? ppClass[0] : NULL );
-    }
-    assert( ppClass[0] != NULL );
-    Vec_PtrPush( p->vClasses, ppClass );
-    // iteratively refine this class
-    if ( fRefineNewClass )
-        nRefis += Fra_RefineClassLastIter( p, p->vClasses );
-    else if ( pSkipped )
-        (*pSkipped)++;
-    return nRefis;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Starts representation of equivalence classes with one class.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Fra_ClassesTest( Fra_Cla_t * p, int Id1, int Id2 )
-{
-    Aig_Obj_t ** pClass;
-    p->pMemClasses = ABC_ALLOC( Aig_Obj_t *, 4 );
-    pClass = p->pMemClasses;
-    assert( Id1 < Id2 );
-    pClass[0] = Aig_ManObj( p->pAig, Id1 );
-    pClass[1] = Aig_ManObj( p->pAig, Id2 );
-    pClass[2] = NULL;
-    pClass[3] = NULL;
-    Fra_ClassObjSetRepr( pClass[1], pClass[0] );
-    Vec_PtrPush( p->vClasses, pClass );
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Creates latch correspondence classes.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Fra_ClassesLatchCorr( Fra_Man_t * p )
-{
-    Aig_Obj_t * pObj;
-    int i, nEntries = 0;
-    Vec_PtrClear( p->pCla->vClasses1 );
-    Aig_ManForEachLoSeq( p->pManAig, pObj, i )
-    {
-        Vec_PtrPush( p->pCla->vClasses1, pObj );
-        Fra_ClassObjSetRepr( pObj, Aig_ManConst1(p->pManAig) );
-    }
-    // allocate room for classes
-    p->pCla->pMemClasses = ABC_ALLOC( Aig_Obj_t *, 2*(nEntries + Vec_PtrSize(p->pCla->vClasses1)) );
-    p->pCla->pMemClassesFree = p->pCla->pMemClasses + 2*nEntries;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Postprocesses the classes by removing half of the less useful.]
-
-  Description []
-               
-  SideEffects [] 
-
-  SeeAlso     []
-
-***********************************************************************/
-void Fra_ClassesPostprocess( Fra_Cla_t * p )
-{
-    int Ratio = 2;
-    Fra_Sml_t * pComb;
-    Aig_Obj_t * pObj, * pRepr, ** ppClass;
-    int * pWeights, WeightMax = 0, i, k, c;
-    // perform combinational simulation
-    pComb = Fra_SmlSimulateComb( p->pAig, 32 );
-    // compute the weight of each node in the classes
-    pWeights = ABC_ALLOC( int, Aig_ManObjNumMax(p->pAig) );
-    memset( pWeights, 0, sizeof(int) * Aig_ManObjNumMax(p->pAig) );
-    Aig_ManForEachObj( p->pAig, pObj, i )
-    { 
-        pRepr = Fra_ClassObjRepr( pObj );
-        if ( pRepr == NULL )
-            continue;
-        pWeights[i] = Fra_SmlNodeNotEquWeight( pComb, pRepr->Id, pObj->Id );
-        WeightMax = ABC_MAX( WeightMax, pWeights[i] );
-    }
-    Fra_SmlStop( pComb );
-    printf( "Before: Const = %6d. Class = %6d.  ", Vec_PtrSize(p->vClasses1), Vec_PtrSize(p->vClasses) );
-    // remove nodes from classes whose weight is less than WeightMax/Ratio
-    k = 0;
-    Vec_PtrForEachEntry( Aig_Obj_t *, p->vClasses1, pObj, i )
-    {
-        if ( pWeights[pObj->Id] >= WeightMax/Ratio )
-            Vec_PtrWriteEntry( p->vClasses1, k++, pObj );
-        else
-            Fra_ClassObjSetRepr( pObj, NULL );
-    }
-    Vec_PtrShrink( p->vClasses1, k );
-    // in each class, compact the nodes
-    Vec_PtrForEachEntry( Aig_Obj_t **, p->vClasses, ppClass, i )
-    {
-        k = 1;
-        for ( c = 1; ppClass[c]; c++ )
-        {
-            if ( pWeights[ppClass[c]->Id] >= WeightMax/Ratio )
-                ppClass[k++] = ppClass[c];
-            else
-                Fra_ClassObjSetRepr( ppClass[c], NULL );
-        }
-        ppClass[k] = NULL;
-    }
-    // remove classes with only repr
-    k = 0;
-    Vec_PtrForEachEntry( Aig_Obj_t **, p->vClasses, ppClass, i )
-        if ( ppClass[1] != NULL )
-            Vec_PtrWriteEntry( p->vClasses, k++, ppClass );
-    Vec_PtrShrink( p->vClasses, k );
-    printf( "After: Const = %6d. Class = %6d. \n", Vec_PtrSize(p->vClasses1), Vec_PtrSize(p->vClasses) );
-    ABC_FREE( pWeights );
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Postprocesses the classes by selecting representative lowest in top order.]
-
-  Description []
-               
-  SideEffects [] 
-
-  SeeAlso     []
-
-***********************************************************************/
-void Fra_ClassesSelectRepr( Fra_Cla_t * p )
-{
-    Aig_Obj_t ** pClass, * pNodeMin;
-    int i, c, cMinSupp, nSuppSizeMin, nSuppSizeCur;
-    // reassign representatives in each class
-    Vec_PtrForEachEntry( Aig_Obj_t **, p->vClasses, pClass, i )
-    {
-        // collect support sizes and find the min-support node
-        cMinSupp = -1;
-        pNodeMin = NULL;
-        nSuppSizeMin = ABC_INFINITY;
-        for ( c = 0; pClass[c]; c++ )
-        {
-            nSuppSizeCur = Aig_SupportSize( p->pAig, pClass[c] );
-//            nSuppSizeCur = 1;
-            if ( nSuppSizeMin > nSuppSizeCur || 
-                (nSuppSizeMin == nSuppSizeCur && pNodeMin->Level > pClass[c]->Level) )
-            {
-                nSuppSizeMin = nSuppSizeCur;
-                pNodeMin = pClass[c];
-                cMinSupp = c; 
-            }
-        }
-        // skip the case when the repr did not change
-        if ( cMinSupp == 0 )
-            continue;
-        // make the new node the representative of the class
-        pClass[cMinSupp] = pClass[0];
-        pClass[0] = pNodeMin;
-        // set the representative
-        for ( c = 0; pClass[c]; c++ )
-            Fra_ClassObjSetRepr( pClass[c], c? pClass[0] : NULL );
-    }
-}
-
-
-
-static inline Aig_Obj_t * Fra_ObjEqu( Aig_Obj_t ** ppEquivs, Aig_Obj_t * pObj )                       { return ppEquivs[pObj->Id];  }
-static inline void        Fra_ObjSetEqu( Aig_Obj_t ** ppEquivs, Aig_Obj_t * pObj, Aig_Obj_t * pNode ) { ppEquivs[pObj->Id] = pNode; }
-
-static inline Aig_Obj_t * Fra_ObjChild0Equ( Aig_Obj_t ** ppEquivs, Aig_Obj_t * pObj ) { return Aig_NotCond(Fra_ObjEqu(ppEquivs,Aig_ObjFanin0(pObj)), Aig_ObjFaninC0(pObj));  }
-static inline Aig_Obj_t * Fra_ObjChild1Equ( Aig_Obj_t ** ppEquivs, Aig_Obj_t * pObj ) { return Aig_NotCond(Fra_ObjEqu(ppEquivs,Aig_ObjFanin1(pObj)), Aig_ObjFaninC1(pObj));  }
-
-/**Function*************************************************************
-
-  Synopsis    [Add the node and its constraints to the new AIG.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-static inline void Fra_ClassesDeriveNode( Aig_Man_t * pManFraig, Aig_Obj_t * pObj, Aig_Obj_t ** ppEquivs )
-{
-    Aig_Obj_t * pObjNew, * pObjRepr, * pObjReprNew, * pMiter;//, * pObjNew2;
-    // skip nodes without representative
-    if ( (pObjRepr = Fra_ClassObjRepr(pObj)) == NULL )
-        return;
-    assert( pObjRepr->Id < pObj->Id );
-    // get the new node 
-    pObjNew = Fra_ObjEqu( ppEquivs, pObj );
-    // get the new node of the representative
-    pObjReprNew = Fra_ObjEqu( ppEquivs, pObjRepr );
-    // if this is the same node, no need to add constraints
-    if ( Aig_Regular(pObjNew) == Aig_Regular(pObjReprNew) )
-        return;
-    // these are different nodes - perform speculative reduction
-//    pObjNew2 = Aig_NotCond( pObjReprNew, pObj->fPhase ^ pObjRepr->fPhase );
-    // set the new node
-//    Fra_ObjSetEqu( ppEquivs, pObj, pObjNew2 );
-    // add the constraint
-    pMiter = Aig_Exor( pManFraig, Aig_Regular(pObjNew), Aig_Regular(pObjReprNew) );
-    pMiter = Aig_NotCond( pMiter, Aig_Regular(pMiter)->fPhase ^ Aig_IsComplement(pMiter) );
-    pMiter = Aig_Not( pMiter );
-    Aig_ObjCreatePo( pManFraig, pMiter );
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Derives AIG for the partitioned problem.]
-
-  Description []
-               
-  SideEffects [] 
-
-  SeeAlso     []
-
-***********************************************************************/
-Aig_Man_t * Fra_ClassesDeriveAig( Fra_Cla_t * p, int nFramesK )
-{
-    Aig_Man_t * pManFraig;
-    Aig_Obj_t * pObj, * pObjNew;
-    Aig_Obj_t ** pLatches, ** ppEquivs;
-    int i, k, f, nFramesAll = nFramesK + 1;
-    assert( Aig_ManRegNum(p->pAig) > 0 );
-    assert( Aig_ManRegNum(p->pAig) < Aig_ManPiNum(p->pAig) );
-    assert( nFramesK > 0 );
-    // start the fraig package
-    pManFraig = Aig_ManStart( Aig_ManObjNumMax(p->pAig) * nFramesAll );
-    pManFraig->pName = Aig_UtilStrsav( p->pAig->pName );
-    pManFraig->pSpec = Aig_UtilStrsav( p->pAig->pSpec );
-    // allocate place for the node mapping
-    ppEquivs = ABC_ALLOC( Aig_Obj_t *, Aig_ManObjNumMax(p->pAig) );
-    Fra_ObjSetEqu( ppEquivs, Aig_ManConst1(p->pAig), Aig_ManConst1(pManFraig) );
-    // create latches for the first frame
-    Aig_ManForEachLoSeq( p->pAig, pObj, i )
-        Fra_ObjSetEqu( ppEquivs, pObj, Aig_ObjCreatePi(pManFraig) );
-    // add timeframes
-    pLatches = ABC_ALLOC( Aig_Obj_t *, Aig_ManRegNum(p->pAig) );
-    for ( f = 0; f < nFramesAll; f++ )
-    {
-        // create PIs for this frame
-        Aig_ManForEachPiSeq( p->pAig, pObj, i )
-            Fra_ObjSetEqu( ppEquivs, pObj, Aig_ObjCreatePi(pManFraig) );
-        // set the constraints on the latch outputs
-        Aig_ManForEachLoSeq( p->pAig, pObj, i )
-            Fra_ClassesDeriveNode( pManFraig, pObj, ppEquivs );
-        // add internal nodes of this frame
-        Aig_ManForEachNode( p->pAig, pObj, i )
-        {
-            pObjNew = Aig_And( pManFraig, Fra_ObjChild0Equ(ppEquivs, pObj), Fra_ObjChild1Equ(ppEquivs, pObj) );
-            Fra_ObjSetEqu( ppEquivs, pObj, pObjNew );
-            Fra_ClassesDeriveNode( pManFraig, pObj, ppEquivs );
-        }
-        if ( f == nFramesAll - 1 )
-            break;
-        if ( f == nFramesAll - 2 )
-            pManFraig->nAsserts = Aig_ManPoNum(pManFraig);
-        // save the latch input values
-        k = 0;
-        Aig_ManForEachLiSeq( p->pAig, pObj, i )
-            pLatches[k++] = Fra_ObjChild0Equ( ppEquivs, pObj );
-        // insert them to the latch output values
-        k = 0;
-        Aig_ManForEachLoSeq( p->pAig, pObj, i )
-            Fra_ObjSetEqu( ppEquivs, pObj, pLatches[k++] );
-    }
-    ABC_FREE( pLatches );
-    ABC_FREE( ppEquivs );
-    // mark the asserts
-    assert( Aig_ManPoNum(pManFraig) % nFramesAll == 0 );
-printf( "Assert miters = %6d. Output miters = %6d.\n", 
-       pManFraig->nAsserts, Aig_ManPoNum(pManFraig) - pManFraig->nAsserts );
-    // remove dangling nodes
-    Aig_ManCleanup( pManFraig );
-    return pManFraig;
-}
-
-////////////////////////////////////////////////////////////////////////
-///                       END OF FILE                                ///
-////////////////////////////////////////////////////////////////////////
-
-
-ABC_NAMESPACE_IMPL_END
-