Version abc90329

1 files changed, 615 insertions, 0 deletions

diff --git a/src/map/cov/covMinSop.c b/src/map/cov/covMinSop.c
new file mode 100644
index 00000000..731a6698
--- /dev/null
+++ b/src/map/cov/covMinSop.c
@@ -0,0 +1,615 @@
+/**CFile****************************************************************
+
+  FileName    [covMinSop.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [Mapping into network of SOPs/ESOPs.]
+
+  Synopsis    [SOP manipulation.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - June 20, 2005.]
+
+  Revision    [$Id: covMinSop.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "covInt.h"
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+static void Min_SopRewrite( Min_Man_t * p );
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Min_SopMinimize( Min_Man_t * p )
+{
+    int nCubesInit, nCubesOld, nIter;
+    if ( p->nCubes < 3 )
+        return;
+    nIter = 0;
+    nCubesInit = p->nCubes;
+    do {
+        nCubesOld = p->nCubes;
+        Min_SopRewrite( p );
+        nIter++;
+//    printf( "%d:%d->%d ", nIter, nCubesInit, p->nCubes );
+    }
+    while ( 100.0*(nCubesOld - p->nCubes)/nCubesOld > 3.0 );
+//    printf( "\n" );
+
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Min_SopRewrite( Min_Man_t * p )
+{
+    Min_Cube_t * pCube, ** ppPrev;
+    Min_Cube_t * pThis, ** ppPrevT;
+    Min_Cube_t * pTemp;
+    int v00, v01, v10, v11, Var0, Var1, Index, fCont0, fCont1, nCubesOld;
+    int nPairs = 0;
+/*    
+    {
+        Min_Cube_t * pCover;
+        pCover = Min_CoverCollect( p, p->nVars );
+printf( "\n\n" );
+Min_CoverWrite( stdout, pCover );
+        Min_CoverExpand( p, pCover );
+    }
+*/
+
+    // insert the bubble before the first cube
+    p->pBubble->pNext = p->ppStore[0];
+    p->ppStore[0] = p->pBubble;
+    p->pBubble->nLits = 0;
+
+    // go through the cubes
+    while ( 1 )
+    {
+        // get the index of the bubble
+        Index = p->pBubble->nLits;
+
+        // find the bubble
+        Min_CoverForEachCubePrev( p->ppStore[Index], pCube, ppPrev )
+            if ( pCube == p->pBubble )
+                break;
+        assert( pCube == p->pBubble );
+
+        // remove the bubble, get the next cube after the bubble
+        *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;
+                }
+        // stop if there is no more cubes
+        if ( pCube == NULL )
+            break;
+
+        // find the first dist2 cube
+        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;
+        // continue if there is no dist2 cube
+        if ( pThis == NULL )
+        {
+            // insert the bubble after the cube
+            p->pBubble->pNext = pCube->pNext;
+            pCube->pNext = p->pBubble;
+            p->pBubble->nLits = pCube->nLits;
+            continue;
+        }
+        nPairs++;
+/*
+printf( "\n" );
+Min_CubeWrite( stdout, pCube );
+Min_CubeWrite( stdout, pThis );
+*/
+        // remove the cubes, insert the bubble instead of pCube
+        *ppPrevT = pThis->pNext;
+        *ppPrev = p->pBubble;
+        p->pBubble->pNext = pCube->pNext;
+        p->pBubble->nLits = pCube->nLits;
+        p->nCubes -= 2;
+
+        assert( pCube != p->pBubble && pThis != p->pBubble );
+
+
+        // save the dist2 parameters
+        v00 = Min_CubeGetVar( pCube, Var0 );
+        v01 = Min_CubeGetVar( pCube, Var1 );
+        v10 = Min_CubeGetVar( pThis, Var0 );
+        v11 = Min_CubeGetVar( pThis, Var1 );
+        assert( v00 != v10 && v01 != v11 );
+        assert( v00 != 3   || v01 != 3 );
+        assert( v10 != 3   || v11 != 3 );
+
+//printf( "\n" );
+//Min_CubeWrite( stdout, pCube );
+//Min_CubeWrite( stdout, pThis );
+
+//printf( "\n" );
+//Min_CubeWrite( stdout, pCube );
+//Min_CubeWrite( stdout, pThis );
+
+        // consider the case when both cubes have non-empty literals
+        if ( v00 != 3 && v01 != 3 && v10 != 3 && v11 != 3 )
+        {
+            assert( v00 == (v10 ^ 3) );
+            assert( v01 == (v11 ^ 3) );
+            // create the temporary cube equal to the first corner
+            Min_CubeXorVar( pCube, Var0, 3 );
+            // check if this cube is contained
+            fCont0 = Min_CoverContainsCube( p, pCube );
+            // create the temporary cube equal to the first corner
+            Min_CubeXorVar( pCube, Var0, 3 );
+            Min_CubeXorVar( pCube, Var1, 3 );
+//printf( "\n" );
+//Min_CubeWrite( stdout, pCube );
+//Min_CubeWrite( stdout, pThis );
+            // check if this cube is contained
+            fCont1 = Min_CoverContainsCube( p, pCube );
+            // undo the change
+            Min_CubeXorVar( pCube, Var1, 3 );
+
+            // check if the cubes can be overwritten
+            if ( fCont0 && fCont1 )
+            {
+                // one of the cubes can be recycled, the other expanded and added
+                Min_CubeRecycle( p, pThis );
+                // remove the literals
+                Min_CubeXorVar( pCube, Var0, v00 ^ 3 );
+                Min_CubeXorVar( pCube, Var1, v01 ^ 3 );
+                pCube->nLits -= 2;
+                Min_SopAddCube( p, pCube );
+            }
+            else if ( fCont0 )
+            {
+                // expand both cubes and add them
+                Min_CubeXorVar( pCube, Var0, v00 ^ 3 );
+                pCube->nLits--;
+                Min_SopAddCube( p, pCube );
+                Min_CubeXorVar( pThis, Var1, v11 ^ 3 );
+                pThis->nLits--;
+                Min_SopAddCube( p, pThis );
+            }
+            else if ( fCont1 )
+            {
+                // expand both cubes and add them
+                Min_CubeXorVar( pCube, Var1, v01 ^ 3 );
+                pCube->nLits--;
+                Min_SopAddCube( p, pCube );
+                Min_CubeXorVar( pThis, Var0, v10 ^ 3 );
+                pThis->nLits--;
+                Min_SopAddCube( p, pThis );
+            }
+            else
+            {
+                Min_SopAddCube( p, pCube );
+                Min_SopAddCube( p, pThis );
+            }
+            // otherwise, no change is possible
+            continue;
+        }
+
+        // if one of them does not have DC lit, move it
+        if ( v00 != 3 && v01 != 3 )
+        {
+            assert( v10 == 3 || v11 == 3 );
+            pTemp = pCube; pCube = pThis; pThis = pTemp;
+            Index = v00; v00 = v10; v10 = Index;
+            Index = v01; v01 = v11; v11 = Index;
+        }
+
+        // make sure the first cube has first var DC
+        if ( v00 != 3 )
+        {
+            assert( v01 == 3 );
+            Index = Var0; Var0 = Var1; Var1 = Index;
+            Index = v00; v00 = v01; v01 = Index;
+            Index = v10; v10 = v11; v11 = Index;
+        }
+
+        // consider both cases: both have DC lit
+        if ( v00 == 3 && v11 == 3 )
+        {
+            assert( v01 != 3 && v10 != 3 );
+            // try the remaining minterm
+            // create the temporary cube equal to the first corner
+            Min_CubeXorVar( pCube, Var0, v10 );
+            Min_CubeXorVar( pCube, Var1, 3   );
+            pCube->nLits++;
+            // check if this cube is contained
+            fCont0 = Min_CoverContainsCube( p, pCube );
+            // undo the cube transformations
+            Min_CubeXorVar( pCube, Var0, v10 );
+            Min_CubeXorVar( pCube, Var1, 3   );
+            pCube->nLits--;
+            // check the case when both are covered
+            if ( fCont0 )
+            {
+                // one of the cubes can be recycled, the other expanded and added
+                Min_CubeRecycle( p, pThis );
+                // remove the literals
+                Min_CubeXorVar( pCube, Var1, v01 ^ 3 );
+                pCube->nLits--;
+                Min_SopAddCube( p, pCube );
+            }
+            else
+            {
+                // try two reduced cubes
+                Min_CubeXorVar( pCube, Var0, v10 );
+                pCube->nLits++;
+                // remember the cubes
+                nCubesOld = p->nCubes;
+                Min_SopAddCube( p, pCube );
+                // check if the cube is absorbed
+                if ( p->nCubes < nCubesOld + 1 )
+                { // absorbed - add the second cube
+                    Min_SopAddCube( p, pThis );
+                }
+                else
+                { // remove this cube, and try another one
+                    assert( pCube == p->ppStore[pCube->nLits] );
+                    p->ppStore[pCube->nLits] = pCube->pNext;
+                    p->nCubes--;
+
+                    // return the cube to the previous state
+                    Min_CubeXorVar( pCube, Var0, v10 );
+                    pCube->nLits--;
+
+                    // generate another reduced cube
+                    Min_CubeXorVar( pThis, Var1, v01 );
+                    pThis->nLits++;
+
+                    // add both cubes
+                    Min_SopAddCube( p, pCube );
+                    Min_SopAddCube( p, pThis );
+                }
+            }
+        }
+        else // the first cube has DC lit
+        {
+            assert( v01 != 3 && v10 != 3 && v11 != 3 );
+            // try the remaining minterm
+            // create the temporary cube equal to the minterm
+            Min_CubeXorVar( pThis, Var0, 3 );
+            // check if this cube is contained
+            fCont0 = Min_CoverContainsCube( p, pThis );
+            // undo the cube transformations
+            Min_CubeXorVar( pThis, Var0, 3 );
+            // check the case when both are covered
+            if ( fCont0 )
+            {
+                // one of the cubes can be recycled, the other expanded and added
+                Min_CubeRecycle( p, pThis );
+                // remove the literals
+                Min_CubeXorVar( pCube, Var1, v01 ^ 3 );
+                pCube->nLits--;
+                Min_SopAddCube( p, pCube );
+            }
+            else
+            {
+                // try reshaping the cubes
+                // reduce the first cube
+                Min_CubeXorVar( pCube, Var0, v10 );
+                pCube->nLits++;
+                // expand the second cube
+                Min_CubeXorVar( pThis, Var1, v11 ^ 3 );
+                pThis->nLits--;
+                // add both cubes
+                Min_SopAddCube( p, pCube );
+                Min_SopAddCube( p, pThis );
+            }
+        }
+    }
+//    printf( "Pairs = %d  ", nPairs );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Adds cube to the SOP cover stored in the manager.]
+
+  Description [Returns 0 if the cube is added or removed. Returns 1
+  if the cube is glued with some other cube and has to be added again.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Min_SopAddCubeInt( Min_Man_t * p, Min_Cube_t * pCube )
+{
+    Min_Cube_t * pThis, * pThis2, ** ppPrev;
+    int i;
+    // try to find the identical cube
+    Min_CoverForEachCube( p->ppStore[pCube->nLits], pThis )
+    {
+        if ( Min_CubesAreEqual( pCube, pThis ) )
+        {
+            Min_CubeRecycle( p, pCube );
+            return 0;
+        }
+    }
+    // try to find a containing cube
+    for ( i = 0; i < (int)pCube->nLits; i++ )
+    Min_CoverForEachCube( p->ppStore[i], pThis )
+    {
+        if ( pThis != p->pBubble && Min_CubeIsContained( pThis, pCube ) )
+        {
+            Min_CubeRecycle( p, pCube );
+            return 0;
+        }
+    }
+    // try to find distance one in the same bin
+    Min_CoverForEachCubePrev( p->ppStore[pCube->nLits], pThis, ppPrev )
+    {
+        if ( Min_CubesDistOne( pCube, pThis, NULL ) )
+        {
+            *ppPrev = pThis->pNext;
+            Min_CubesTransformOr( pCube, pThis );
+            pCube->nLits--;
+            Min_CubeRecycle( p, pThis );
+            p->nCubes--;
+            return 1;
+        }
+    }
+
+    // clean the other cubes using this one
+    for ( i = pCube->nLits + 1; i <= (int)pCube->nVars; i++ )
+    {
+        ppPrev = &p->ppStore[i];
+        Min_CoverForEachCubeSafe( p->ppStore[i], pThis, pThis2 )
+        {
+            if ( pThis != p->pBubble && Min_CubeIsContained( pCube, pThis ) )
+            {
+                *ppPrev = pThis->pNext;
+                Min_CubeRecycle( p, pThis );
+                p->nCubes--;
+            }
+            else
+                ppPrev = &pThis->pNext;
+        }
+    }
+
+    // add the cube
+    pCube->pNext = p->ppStore[pCube->nLits];
+    p->ppStore[pCube->nLits] = pCube;
+    p->nCubes++;
+    return 0;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Adds the cube to storage.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Min_SopAddCube( Min_Man_t * p, Min_Cube_t * pCube )
+{
+    assert( Min_CubeCheck( pCube ) );
+    assert( pCube != p->pBubble );
+    assert( (int)pCube->nLits == Min_CubeCountLits(pCube) );
+    while ( Min_SopAddCubeInt( p, pCube ) );
+}
+
+
+
+
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Min_SopContain( Min_Man_t * p )
+{
+    Min_Cube_t * pCube, * pCube2, ** ppPrev;
+    int i, k;
+    for ( i = 0; i <= p->nVars; i++ )
+    {
+        Min_CoverForEachCube( p->ppStore[i], pCube )
+        Min_CoverForEachCubePrev( pCube->pNext, pCube2, ppPrev )
+        {
+            if ( !Min_CubesAreEqual( pCube, pCube2 ) )
+                continue;
+            *ppPrev = pCube2->pNext;
+            Min_CubeRecycle( p, pCube2 );
+            p->nCubes--;
+        }
+        for ( k = i + 1; k <= p->nVars; k++ )
+        Min_CoverForEachCubePrev( p->ppStore[k], pCube2, ppPrev )
+        {
+            if ( !Min_CubeIsContained( pCube, pCube2 ) )
+                continue;
+            *ppPrev = pCube2->pNext;
+            Min_CubeRecycle( p, pCube2 );
+            p->nCubes--;
+        }
+    }
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Min_SopDist1Merge( Min_Man_t * p )
+{
+    Min_Cube_t * pCube, * pCube2, * pCubeNew;
+    int i;
+    for ( i = p->nVars; i >= 0; i-- )
+    {
+        Min_CoverForEachCube( p->ppStore[i], pCube )
+        Min_CoverForEachCube( pCube->pNext, pCube2 )
+        {
+            assert( pCube->nLits == pCube2->nLits );
+            if ( !Min_CubesDistOne( pCube, pCube2, NULL ) )
+                continue;
+            pCubeNew = Min_CubesXor( p, pCube, pCube2 );
+            assert( pCubeNew->nLits == pCube->nLits - 1 );
+            pCubeNew->pNext = p->ppStore[pCubeNew->nLits];
+            p->ppStore[pCubeNew->nLits] = pCubeNew;
+            p->nCubes++;
+        }
+    }
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Min_Cube_t * Min_SopComplement( Min_Man_t * p, Min_Cube_t * pSharp )
+{
+     Vec_Int_t * vVars;
+     Min_Cube_t * pCover, * pCube, * pNext, * pReady, * pThis, ** ppPrev;
+     int Num, Value, i;
+
+     // get the variables
+     vVars = Vec_IntAlloc( 100 );
+    // create the tautology cube
+     pCover = Min_CubeAlloc( p );
+     // sharp it with all cubes
+     Min_CoverForEachCube( pSharp, pCube )
+     Min_CoverForEachCubePrev( pCover, pThis, ppPrev )
+     {
+        if ( Min_CubesDisjoint( pThis, pCube ) )
+            continue;
+        // remember the next pointer
+        pNext = pThis->pNext;
+        // get the variables, in which pThis is '-' while pCube is fixed
+        Min_CoverGetDisjVars( pThis, pCube, vVars );
+        // generate the disjoint cubes
+        pReady = pThis;
+        Vec_IntForEachEntryReverse( vVars, Num, i )
+        {
+            // correct the literal
+            Min_CubeXorVar( pReady, vVars->pArray[i], 3 );
+            if ( i == 0 )
+                break;
+            // create the new cube and clean this value
+            Value = Min_CubeGetVar( pReady, vVars->pArray[i] );
+            pReady = Min_CubeDup( p, pReady );
+            Min_CubeXorVar( pReady, vVars->pArray[i], 3 ^ Value );
+            // add to the cover
+            *ppPrev = pReady;
+            ppPrev = &pReady->pNext;
+        }
+        pThis = pReady;
+        pThis->pNext = pNext;
+     }
+     Vec_IntFree( vVars );
+
+     // perform dist-1 merge and contain
+     Min_CoverExpandRemoveEqual( p, pCover );
+     Min_SopDist1Merge( p );
+     Min_SopContain( p );
+     return Min_CoverCollect( p, p->nVars );
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Min_SopCheck( Min_Man_t * p )
+{
+    Min_Cube_t * pCube, * pThis;
+    int i;
+
+    pCube = Min_CubeAlloc( p );
+    Min_CubeXorBit( pCube, 2*0+1 );
+    Min_CubeXorBit( pCube, 2*1+1 );
+    Min_CubeXorBit( pCube, 2*2+0 );
+    Min_CubeXorBit( pCube, 2*3+0 );
+    Min_CubeXorBit( pCube, 2*4+0 );
+    Min_CubeXorBit( pCube, 2*5+1 );
+    Min_CubeXorBit( pCube, 2*6+1 );
+    pCube->nLits = 7;
+
+//    Min_CubeWrite( stdout, pCube );
+
+    // check that the cubes contain it
+    for ( i = 0; i <= p->nVars; i++ )
+        Min_CoverForEachCube( p->ppStore[i], pThis )
+            if ( pThis != p->pBubble && Min_CubeIsContained( pThis, pCube ) )
+            {
+                Min_CubeRecycle( p, pCube );
+                return 1;
+            }
+    Min_CubeRecycle( p, pCube );
+    return 0;
+}
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+