abc/src/aig/aig/aigPartSat.c
/**Function*************************************************************

  Synopsis    [Derives AIGs for each partition.]

  Description [The first argument is a original AIG. The second argument
  is the array mapping each AND-node's ID into the 0-based number of its
  partition. The last argument is the array of arrays (one for each new AIG) 
  mapping the index of each terminal in the new AIG (the index of each 
  terminal is derived by ordering PIs followed by POs in their natural order) 
  into the ID of the corresponding node in the original AIG. The returned 
  value is the array of AIGs representing the partitions.]
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
Function
Synopsis    [Derives AIGs for each partition.]

Description [The first argument is a original AIG. The second argument
is the array mapping each AND-node's ID into the 0-based number of its
partition. The last argument is the array of arrays (one for each new AIG)
mapping the index of each terminal in the new AIG (the index of each
terminal is derived by ordering PIs followed by POs in their natural order)
into the ID of the corresponding node in the original AIG. The returned
value is the array of AIGs representing the partitions.]




Function Synopsis [ Derives AIGs for each partition . ] Description [ The first argument is a original AIG . The second argument is the array mapping each AND - node ' s ID into the 0 - based number of its partition . The last argument is the array of arrays ( one for each new AIG ) mapping the index of each terminal in the new AIG ( the index of each terminal is derived by ordering PIs followed by POs in their natural order ) into the ID of the corresponding node in the original AIG . The returned value is the array of AIGs representing the partitions . ]
Vec_Ptr_t * Aig_ManPartSplit( Aig_Man_t * p, Vec_Int_t * vNode2Part, Vec_Ptr_t ** pvPio2Id, Vec_Ptr_t ** pvPart2Pos )
{
    Vec_Vec_t * vGroups, * vPart2Pos;
    Vec_Ptr_t * vAigs, * vPio2Id, * vNodes;
    Vec_Int_t * vPio2IdOne;
    Aig_Man_t * pAig;
    Aig_Obj_t * pObj, * pDriver;
    int i, nodePart, nParts;
    vAigs = Vec_PtrAlloc( 100 );
    vPio2Id = Vec_PtrAlloc( 100 );
    nParts = Vec_IntFindMax(vNode2Part) + 1;
    assert( nParts > 0 );
    vGroups = Vec_VecAlloc( nParts );
    Vec_IntForEachEntry( vNode2Part, nodePart, i )
    {
        pObj = Aig_ManObj( p, i );
        if ( Aig_ObjIsNode(pObj) )
            Vec_VecPush( vGroups, nodePart, pObj );
    }
    Aig_ManForEachCo( p, pObj, i )
    {
        pDriver = Aig_ObjFanin0(pObj);
        if ( Aig_ObjIsCi(pDriver) )
        {
            if ( Aig_ObjFaninC0(pObj) )
                pDriver->fMarkA = 1; 
            else
                pDriver->fMarkB = 1; 
        }
    }
    Vec_VecForEachLevel( vGroups, vNodes, i )
    {
        if ( Vec_PtrSize(vNodes) == 0 )
        {
            printf( "Aig_ManPartSplit(): Skipping partition # %d without nodes (warning).\n", i );
            continue;
        }
        pAig = Aig_ManPartSplitOne( p, vNodes, &vPio2IdOne );
        Vec_PtrPush( vPio2Id, vPio2IdOne );
        Vec_PtrPush( vAigs, pAig );
    }
    Vec_VecFree( vGroups );
    vPart2Pos = Vec_VecStart( Vec_PtrSize(vAigs) );
    Aig_ManForEachCo( p, pObj, i )
    {
        pDriver = Aig_ObjFanin0(pObj);
        if ( Aig_ObjIsCi(pDriver) )
            pDriver->fMarkA = pDriver->fMarkB = 0;
        else
            Vec_VecPush( vPart2Pos, Vec_IntEntry(vNode2Part, Aig_ObjFaninId0(pObj)), pObj );
    }
    *pvPio2Id = vPio2Id;
    *pvPart2Pos = (Vec_Ptr_t *)vPart2Pos;
    return vAigs;
}
Vec_Ptr_t * Aig_ManPartSplit ( Aig_Man_t * p , Vec_Int_t * vNode2Part , Vec_Ptr_t * * pvPio2Id , Vec_Ptr_t * * pvPart2Pos ) { Vec_Vec_t * vGroups , * vPart2Pos ; Vec_Ptr_t * vAigs , * vPio2Id , * vNodes ; Vec_Int_t * vPio2IdOne ; Aig_Man_t * pAig ; Aig_Obj_t * pObj , * pDriver ; int i , nodePart , nParts ; vAigs = Vec_PtrAlloc ( 100 ) ; vPio2Id = Vec_PtrAlloc ( 100 ) ; nParts = Vec_IntFindMax ( vNode2Part ) + 1 ; assert ( nParts > 0 ) ; vGroups = Vec_VecAlloc ( nParts ) ; Vec_IntForEachEntry ( vNode2Part , nodePart , i ) { pObj = Aig_ManObj ( p , i ) ; if ( Aig_ObjIsNode ( pObj ) ) Vec_VecPush ( vGroups , nodePart , pObj ) ; } Aig_ManForEachCo ( p , pObj , i ) { pDriver = Aig_ObjFanin0 ( pObj ) ; if ( Aig_ObjIsCi ( pDriver ) ) { if ( Aig_ObjFaninC0 ( pObj ) ) pDriver -> fMarkA = 1 ; else pDriver -> fMarkB = 1 ; } } Vec_VecForEachLevel ( vGroups , vNodes , i ) { if ( Vec_PtrSize ( vNodes ) == 0 ) { printf ( " \n " , i ) ; continue ; } pAig = Aig_ManPartSplitOne ( p , vNodes , & vPio2IdOne ) ; Vec_PtrPush ( vPio2Id , vPio2IdOne ) ; Vec_PtrPush ( vAigs , pAig ) ; } Vec_VecFree ( vGroups ) ; vPart2Pos = Vec_VecStart ( Vec_PtrSize ( vAigs ) ) ; Aig_ManForEachCo ( p , pObj , i ) { pDriver = Aig_ObjFanin0 ( pObj ) ; if ( Aig_ObjIsCi ( pDriver ) ) pDriver -> fMarkA = pDriver -> fMarkB = 0 ; else Vec_VecPush ( vPart2Pos , Vec_IntEntry ( vNode2Part , Aig_ObjFaninId0 ( pObj ) ) , pObj ) ; } * pvPio2Id = vPio2Id ; * pvPart2Pos = ( Vec_Ptr_t * ) vPart2Pos ; return vAigs ; }
Function
Synopsis    [Derives AIGs for each partition.]
Function Synopsis [ Derives AIGs for each partition . ]
// put all nodes into levels according to their partition // label PIs that should be restricted to some values // const0 PI // const1 PI // create partitions // divide POs according to their partitions