abc/src/map/cov/covMinEsop.c
/**Function*************************************************************

  Synopsis    [Performs one round of rewriting using distance 2 cubes.]

  Description [The weakness of this procedure is that it tries each cube
  with only one distance-2 cube. If this pair does not lead to improvement
  the cube is inserted into the cover anyhow, and we try another pair.
  A possible improvement would be to try this cube with all distance-2
  cubes, until an improvement is found, or until all such cubes are tried.]
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
Function
Synopsis    [Performs one round of rewriting using distance 2 cubes.]

Description [The weakness of this procedure is that it tries each cube
with only one distance-2 cube. If this pair does not lead to improvement
the cube is inserted into the cover anyhow, and we try another pair.
A possible improvement would be to try this cube with all distance-2
cubes, until an improvement is found, or until all such cubes are tried.]




Function Synopsis [ Performs one round of rewriting using distance 2 cubes . ] Description [ The weakness of this procedure is that it tries each cube with only one distance - 2 cube . If this pair does not lead to improvement the cube is inserted into the cover anyhow and we try another pair . A possible improvement would be to try this cube with all distance - 2 cubes until an improvement is found or until all such cubes are tried . ]
void Min_EsopRewrite( Min_Man_t * p )
{
    Min_Cube_t * pCube, ** ppPrev;
    Min_Cube_t * pThis, ** ppPrevT;
    int v00, v01, v10, v11, Var0, Var1, Index, nCubesOld;
    int nPairs = 0;
    p->pBubble->pNext = p->ppStore[0];
    p->ppStore[0] = p->pBubble;
    p->pBubble->nLits = 0;
    while ( 1 )
    {
        Index = p->pBubble->nLits;
        Min_CoverForEachCubePrev( p->ppStore[Index], pCube, ppPrev )
            if ( pCube == p->pBubble )
                break;
        assert( pCube == p->pBubble );
        *ppPrev = p->pBubble->pNext;
        pCube = p->pBubble->pNext;
        if ( pCube == NULL )
            for ( Index++; Index <= p->nVars; Index++ )
                if ( p->ppStore[Index] )
                {
                    ppPrev = &(p->ppStore[Index]);
                    pCube = p->ppStore[Index];
                    break;
                }
        if ( pCube == NULL )
            break;
        Min_CoverForEachCubePrev( pCube->pNext, pThis, ppPrevT )
            if ( Min_CubesDistTwo( pCube, pThis, &Var0, &Var1 ) )
                break;
        if ( pThis == NULL && Index < p->nVars )
        Min_CoverForEachCubePrev( p->ppStore[Index+1], pThis, ppPrevT )
            if ( Min_CubesDistTwo( pCube, pThis, &Var0, &Var1 ) )
                break;
        if ( pThis == NULL && Index < p->nVars - 1 )
        Min_CoverForEachCubePrev( p->ppStore[Index+2], pThis, ppPrevT )
            if ( Min_CubesDistTwo( pCube, pThis, &Var0, &Var1 ) )
                break;
        if ( pThis == NULL )
        {
            p->pBubble->pNext = pCube->pNext;
            pCube->pNext = p->pBubble;
            p->pBubble->nLits = pCube->nLits;
            continue;
        }
        nPairs++;
        *ppPrevT = pThis->pNext;
        *ppPrev = p->pBubble;
        p->pBubble->pNext = pCube->pNext;
        p->pBubble->nLits = pCube->nLits;
        p->nCubes -= 2;
        v00 = Min_CubeGetVar( pCube, Var0 );
        v01 = Min_CubeGetVar( pCube, Var1 );
        v10 = Min_CubeGetVar( pThis, Var0 );
        v11 = Min_CubeGetVar( pThis, Var1 );
        Min_CubeXorVar( pCube, Var0, v10 );
        pCube->nLits -= (v00 != 3);
        pCube->nLits += ((v00 ^ v10) != 3);
        Min_CubeXorVar( pThis, Var1, v01 );
        pThis->nLits -= (v11 != 3);
        pThis->nLits += ((v01 ^ v11) != 3);
        nCubesOld = p->nCubes;
        Min_EsopAddCube( p, pCube );
        Min_EsopAddCube( p, pThis );
        if ( p->nCubes < nCubesOld + 2 )
            continue;
        assert( pThis == p->ppStore[pThis->nLits] );
        p->ppStore[pThis->nLits] = pThis->pNext;
        assert( pCube == p->ppStore[pCube->nLits] );
        p->ppStore[pCube->nLits] = pCube->pNext;
        p->nCubes -= 2;
        Min_CubeXorVar( pCube, Var0, v10 );
        pCube->nLits -= ((v00 ^ v10) != 3);
        pCube->nLits += (v00 != 3);
        Min_CubeXorVar( pCube, Var1, v11 );
        pCube->nLits -= (v01 != 3);
        pCube->nLits += ((v01 ^ v11) != 3);
        Min_CubeXorVar( pThis, Var0, v00 );
        pThis->nLits -= (v10 != 3);
        pThis->nLits += ((v00 ^ v10) != 3);
        Min_CubeXorVar( pThis, Var1, v01 );
        pThis->nLits -= ((v01 ^ v11) != 3);
        pThis->nLits += (v11 != 3);
        Min_EsopAddCube( p, pCube );
        Min_EsopAddCube( p, pThis );
    }
}
void Min_EsopRewrite ( Min_Man_t * p ) { Min_Cube_t * pCube , * * ppPrev ; Min_Cube_t * pThis , * * ppPrevT ; int v00 , v01 , v10 , v11 , Var0 , Var1 , Index , nCubesOld ; int nPairs = 0 ; p -> pBubble -> pNext = p -> ppStore [ 0 ] ; p -> ppStore [ 0 ] = p -> pBubble ; p -> pBubble -> nLits = 0 ; while ( 1 ) { Index = p -> pBubble -> nLits ; Min_CoverForEachCubePrev ( p -> ppStore [ Index ] , pCube , ppPrev ) if ( pCube == p -> pBubble ) break ; assert ( pCube == p -> pBubble ) ; * ppPrev = p -> pBubble -> pNext ; pCube = p -> pBubble -> pNext ; if ( pCube == NULL ) for ( Index ++ ; Index <= p -> nVars ; Index ++ ) if ( p -> ppStore [ Index ] ) { ppPrev = & ( p -> ppStore [ Index ] ) ; pCube = p -> ppStore [ Index ] ; break ; } if ( pCube == NULL ) break ; Min_CoverForEachCubePrev ( pCube -> pNext , pThis , ppPrevT ) if ( Min_CubesDistTwo ( pCube , pThis , & Var0 , & Var1 ) ) break ; if ( pThis == NULL && Index < p -> nVars ) Min_CoverForEachCubePrev ( p -> ppStore [ Index + 1 ] , pThis , ppPrevT ) if ( Min_CubesDistTwo ( pCube , pThis , & Var0 , & Var1 ) ) break ; if ( pThis == NULL && Index < p -> nVars - 1 ) Min_CoverForEachCubePrev ( p -> ppStore [ Index + 2 ] , pThis , ppPrevT ) if ( Min_CubesDistTwo ( pCube , pThis , & Var0 , & Var1 ) ) break ; if ( pThis == NULL ) { p -> pBubble -> pNext = pCube -> pNext ; pCube -> pNext = p -> pBubble ; p -> pBubble -> nLits = pCube -> nLits ; continue ; } nPairs ++ ; * ppPrevT = pThis -> pNext ; * ppPrev = p -> pBubble ; p -> pBubble -> pNext = pCube -> pNext ; p -> pBubble -> nLits = pCube -> nLits ; p -> nCubes -= 2 ; v00 = Min_CubeGetVar ( pCube , Var0 ) ; v01 = Min_CubeGetVar ( pCube , Var1 ) ; v10 = Min_CubeGetVar ( pThis , Var0 ) ; v11 = Min_CubeGetVar ( pThis , Var1 ) ; Min_CubeXorVar ( pCube , Var0 , v10 ) ; pCube -> nLits -= ( v00 != 3 ) ; pCube -> nLits += ( ( v00 ^ v10 ) != 3 ) ; Min_CubeXorVar ( pThis , Var1 , v01 ) ; pThis -> nLits -= ( v11 != 3 ) ; pThis -> nLits += ( ( v01 ^ v11 ) != 3 ) ; nCubesOld = p -> nCubes ; Min_EsopAddCube ( p , pCube ) ; Min_EsopAddCube ( p , pThis ) ; if ( p -> nCubes < nCubesOld + 2 ) continue ; assert ( pThis == p -> ppStore [ pThis -> nLits ] ) ; p -> ppStore [ pThis -> nLits ] = pThis -> pNext ; assert ( pCube == p -> ppStore [ pCube -> nLits ] ) ; p -> ppStore [ pCube -> nLits ] = pCube -> pNext ; p -> nCubes -= 2 ; Min_CubeXorVar ( pCube , Var0 , v10 ) ; pCube -> nLits -= ( ( v00 ^ v10 ) != 3 ) ; pCube -> nLits += ( v00 != 3 ) ; Min_CubeXorVar ( pCube , Var1 , v11 ) ; pCube -> nLits -= ( v01 != 3 ) ; pCube -> nLits += ( ( v01 ^ v11 ) != 3 ) ; Min_CubeXorVar ( pThis , Var0 , v00 ) ; pThis -> nLits -= ( v10 != 3 ) ; pThis -> nLits += ( ( v00 ^ v10 ) != 3 ) ; Min_CubeXorVar ( pThis , Var1 , v01 ) ; pThis -> nLits -= ( ( v01 ^ v11 ) != 3 ) ; pThis -> nLits += ( v11 != 3 ) ; Min_EsopAddCube ( p , pCube ) ; Min_EsopAddCube ( p , pThis ) ; } }
Function
Synopsis    [Performs one round of rewriting using distance 2 cubes.]
Function Synopsis [ Performs one round of rewriting using distance 2 cubes . ]
// insert the bubble before the first cube // go through the cubes // get the index of the bubble // find the bubble // remove the bubble, get the next cube after the bubble // stop if there is no more cubes // find the first dist2 cube // continue if there is no dist2 cube // insert the bubble after the cube // remove the cubes, insert the bubble instead of pCube // Exorlink-2: // A{v00}     B{v01}      +  A{v10}     B{v11}     = // A{v00+v10} B{v01}      +  A{v10}     B{v01+v11} = // A{v00}     B{v01+v11}  +  A{v00+v10} B{v11} // save the dist2 parameters //printf( "\n" ); //Min_CubeWrite( stdout, pCube ); //Min_CubeWrite( stdout, pThis ); // derive the first pair of resulting cubes // add the cubes // check if the cubes were absorbed // pull out both cubes // derive the second pair of resulting cubes // add them anyhow //    printf( "Pairs = %d  ", nPairs );