Command &esop to convert AIG into ESOP.

abclib.dsp

@@ -4195,6 +4195,10 @@ SOURCE=.\src\aig\gia\giaEra2.c
 # End Source File
 # Begin Source File
 
+SOURCE=.\src\aig\gia\giaEsop.c
+# End Source File
+# Begin Source File
+
 SOURCE=.\src\aig\gia\giaFadds.c
 # End Source File
 # Begin Source File

src/aig/gia/giaEsop.c

+/**CFile****************************************************************
+
+  FileName    [giaEsop.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [Scalable AIG package.]
+
+  Synopsis    [ESOP computation.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - June 20, 2005.]
+
+  Revision    [$Id: giaEsop.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "gia.h"
+#include "misc/extra/extra.h"
+#include "misc/vec/vecHsh.h"
+#include "misc/vec/vecWec.h"
+
+ABC_NAMESPACE_IMPL_START
+
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+typedef struct Eso_Man_t_ Eso_Man_t;
+struct Eso_Man_t_
+{
+    Gia_Man_t *     pGia;     // user's AIG
+    int             nVars;    // number of variables
+    int             Cube1;    // ID of const1 cube
+    Vec_Wec_t *     vEsops;   // ESOP for each node
+    Hsh_VecMan_t *  pHash;    // hash table for cubes
+    Vec_Wec_t *     vCubes;   // cover during minimization
+    // internal
+    Vec_Int_t *     vCube1;   // first cube
+    Vec_Int_t *     vCube2;   // second cube
+    Vec_Int_t *     vCube;    // resulting cube
+};
+
+static inline Vec_Int_t * Eso_ManCube( Eso_Man_t * p, int iCube ) { assert( iCube >= 0 ); return Hsh_VecReadEntry(p->pHash, iCube); }
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+    
+/**Function*************************************************************
+
+  Synopsis    [Computation manager.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Eso_Man_t * Eso_ManAlloc( Gia_Man_t * pGia )
+{
+    int i, n, Id;
+    Eso_Man_t * p = ABC_CALLOC( Eso_Man_t, 1 );
+    p->pGia   = pGia;
+    p->nVars  = Gia_ManCiNum(pGia);
+    p->Cube1  = ABC_INFINITY;
+    p->vEsops = Vec_WecStart( Gia_ManObjNum(pGia) );
+    p->pHash  = Hsh_VecManStart( 1000 );
+    p->vCubes = Vec_WecStart(Gia_ManCiNum(pGia)+1);
+    p->vCube1 = Vec_IntAlloc(Gia_ManCiNum(pGia));
+    p->vCube2 = Vec_IntAlloc(Gia_ManCiNum(pGia));
+    p->vCube  = Vec_IntAlloc(Gia_ManCiNum(pGia));
+    Gia_ManForEachCiId( pGia, Id, i )
+    {
+        for ( n = 0; n < 2; n++ )
+        {
+            Vec_IntFill( p->vCube, 1, Abc_Var2Lit(i, n) );
+            Hsh_VecManAdd( p->pHash, p->vCube );
+        }
+        Vec_IntPush( Vec_WecEntry(p->vEsops, Id), Abc_Var2Lit(i, 0) );
+    }
+    return p;
+}
+void Eso_ManStop( Eso_Man_t * p )
+{
+    Vec_WecFree( p->vEsops );
+    Hsh_VecManStop( p->pHash );
+    Vec_WecFree( p->vCubes );
+    Vec_IntFree( p->vCube1 );
+    Vec_IntFree( p->vCube2 );
+    Vec_IntFree( p->vCube );
+    ABC_FREE( p );
+}
+    
+
+/**Function*************************************************************
+
+  Synopsis    [Printing/transforming the cover.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Eso_ManCoverPrint( Eso_Man_t * p, Vec_Int_t * vEsop )
+{
+    Vec_Str_t * vStr;
+    Vec_Int_t * vCube;
+    int i, k, Lit, Cube;
+    if ( Vec_IntSize(vEsop) == 0 )
+    {
+        printf( "Const 0\n" );
+        return;
+    }
+    vStr = Vec_StrAlloc( p->nVars + 4 );
+    Vec_StrFill( vStr, p->nVars, '-' );
+    Vec_StrPush( vStr, ' ' );
+    Vec_StrPush( vStr, '1' );
+    Vec_StrPush( vStr, '\n' );
+    Vec_StrPush( vStr, '\0' );
+    assert( Vec_IntSize(vEsop) > 0 );
+    Vec_IntForEachEntry( vEsop, Cube, i )
+    {
+        if ( Cube == p->Cube1 )
+            printf( "%s", Vec_StrArray(vStr) );
+        else 
+        {
+            vCube = Eso_ManCube( p, Cube );
+            Vec_IntForEachEntry( vCube, Lit, k )
+                Vec_StrWriteEntry( vStr, Abc_Lit2Var(Lit), (char)(Abc_LitIsCompl(Lit)?'0':'1') );
+            printf( "%s", Vec_StrArray(vStr) );
+            Vec_IntForEachEntry( vCube, Lit, k )
+                Vec_StrWriteEntry( vStr, Abc_Lit2Var(Lit), '-' );
+        }
+    }
+    printf( "\n" );
+    Vec_StrFree( vStr );
+}
+Gia_Man_t * Eso_ManCoverConvert( Eso_Man_t * p, Vec_Ptr_t * vCover )
+{
+    Vec_Int_t * vEsop;
+    Gia_Man_t * pNew, * pTemp;
+    Gia_Obj_t * pObj;  int i;
+    pNew = Gia_ManStart( Gia_ManObjNum(p->pGia) );
+    pNew->pName = Abc_UtilStrsav( p->pGia->pName );
+    pNew->pSpec = Abc_UtilStrsav( p->pGia->pSpec );
+    Gia_ManHashAlloc( pNew );
+    Gia_ManConst0(p->pGia)->Value = 0;
+    Gia_ManForEachCi( p->pGia, pObj, i )
+        pObj->Value = Gia_ManAppendCi(pNew);
+    Vec_PtrForEachEntry( Vec_Int_t *, vCover, vEsop, i )
+    {
+        if ( Vec_IntSize(vEsop) > 0 )
+        {
+            int c, Cube, iRoot = 0;
+            Vec_IntForEachEntry( vEsop, Cube, c )
+            {
+                int k, Lit, iAnd = 1;
+                if ( Cube != p->Cube1 )
+                {
+                    Vec_Int_t * vCube = Eso_ManCube( p, Cube );
+                    Vec_IntForEachEntry( vCube, Lit, k )
+                        iAnd = Gia_ManHashAnd( pNew, iAnd, Lit + 2 );
+                }
+                iRoot = Gia_ManHashXor( pNew, iRoot, iAnd );
+            }
+            Gia_ManAppendCo( pNew, iRoot );
+        }
+        else
+            Gia_ManAppendCo( pNew, 0 );
+    }
+    // cleanup
+    pNew = Gia_ManCleanup( pTemp = pNew );
+    Gia_ManStop( pTemp );
+    return pNew;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Minimization.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Eso_ManFindDistOneLitEqual( int * pCube1, int * pCube2, int nLits ) // pCube1 and pCube2 both have nLits
+{
+    int i, iDiff = -1;
+    for ( i = 0; i < nLits; i++ )
+        if ( pCube1[i] != pCube2[i] )
+        {
+            if ( iDiff != -1 )
+                return -1;
+            if ( Abc_Lit2Var(pCube1[i]) != Abc_Lit2Var(pCube2[i]) )
+                return -1;
+            iDiff = i;
+        }
+    return iDiff;
+}
+int Eso_ManFindDistOneLitNotEqual( int * pCube1, int * pCube2, int nLits ) // pCube1 has nLits; pCube2 has nLits + 1
+{
+    int i, k, iDiff = -1;
+    for ( i = k = 0; i < nLits; i++, k++ )
+        if ( pCube1[i] != pCube2[k] )
+        {
+            if ( iDiff != -1 )
+                return -1;
+            iDiff = i;
+            i--;
+        }
+    if ( iDiff == -1 )
+        iDiff = nLits;
+    return iDiff;
+}
+void Eso_ManMinimizeAdd( Eso_Man_t * p, int Cube )
+{
+    int fMimimize = 1;
+    Vec_Int_t * vCube      = (Cube == p->Cube1) ? NULL : Eso_ManCube(p, Cube); 
+    int * pCube2, * pCube  = (Cube == p->Cube1) ? NULL : Vec_IntArray(vCube); 
+    int Cube2, nLits       = (Cube == p->Cube1) ? 0 : Vec_IntSize(vCube);
+    Vec_Int_t * vLevel     = Vec_WecEntry( p->vCubes, nLits );
+    int c, k, iLit, iPlace = Vec_IntFind( vLevel, Cube );
+    if ( iPlace >= 0 ) // identical found
+    {
+        Vec_IntDrop( vLevel, iPlace );
+        return;
+    }
+    if ( Cube == p->Cube1 ) // simple case
+    {
+        assert( Vec_IntSize(vLevel) == 0 );
+        Vec_IntPush( vLevel, Cube );
+        return;
+    }
+    // look for distance-1 in next bin
+    if ( fMimimize && nLits < p->nVars - 1 )
+    {
+        Vec_Int_t * vLevel = Vec_WecEntry( p->vCubes, nLits+1 );
+        Vec_IntForEachEntry( vLevel, Cube2, c )
+        {
+            pCube2 = Hsh_VecReadArray( p->pHash, Cube2 ); 
+            iLit = Eso_ManFindDistOneLitNotEqual( pCube, pCube2, nLits );
+            if ( iLit == -1 )
+                continue;
+            // remove this cube
+            Vec_IntDrop( vLevel, c );
+            // create new cube
+            Vec_IntClear( p->vCube );
+            for ( k = 0; k <= nLits; k++ )
+                Vec_IntPush( p->vCube, Abc_LitNotCond(pCube2[k], k == iLit) );
+            Cube = Hsh_VecManAdd( p->pHash, p->vCube );
+            // try to add new cube
+            Eso_ManMinimizeAdd( p, Cube );
+            return;
+        }
+    }
+    // look for distance-1 in the same bin
+    if ( fMimimize )
+    {
+        Vec_IntForEachEntry( vLevel, Cube2, c )
+        {
+            pCube2 = Hsh_VecReadArray( p->pHash, Cube2 ); 
+            iLit = Eso_ManFindDistOneLitEqual( pCube2, pCube, nLits );
+            if ( iLit == -1 )
+                continue;
+            // remove this cube
+            Vec_IntDrop( vLevel, c );
+            // create new cube
+            Vec_IntClear( p->vCube );
+            for ( k = 0; k < nLits; k++ )
+                if ( k != iLit )
+                    Vec_IntPush( p->vCube, pCube[k] );
+            if ( Vec_IntSize(p->vCube) == 0 )
+                Cube = p->Cube1;
+            else
+                Cube = Hsh_VecManAdd( p->pHash, p->vCube );
+            // try to add new cube
+            Eso_ManMinimizeAdd( p, Cube );
+            return;
+        }
+    }
+    assert( nLits > 0 );
+    if ( fMimimize && nLits > 0 )
+    {
+        // look for distance-1 in the previous bin
+        Vec_Int_t * vLevel = Vec_WecEntry( p->vCubes, nLits-1 );
+        // check for the case of one-literal cube
+        if ( nLits == 1 && Vec_IntSize(vLevel) == 1 )
+        {
+            Vec_IntDrop( vLevel, 0 );
+            Cube = Abc_LitNot( Cube );
+        }
+        else
+        Vec_IntForEachEntry( vLevel, Cube2, c )
+        {
+            pCube2 = Hsh_VecReadArray( p->pHash, Cube2 ); 
+            iLit = Eso_ManFindDistOneLitNotEqual( pCube2, pCube, nLits-1 );
+            if ( iLit == -1 )
+                continue;
+            // remove this cube
+            Vec_IntDrop( vLevel, c );
+            // create new cube
+            Vec_IntClear( p->vCube );
+            for ( k = 0; k < nLits; k++ )
+                Vec_IntPush( p->vCube, Abc_LitNotCond(pCube[k], k == iLit) );
+            Cube = Hsh_VecManAdd( p->pHash, p->vCube );
+            // try to add new cube
+            Eso_ManMinimizeAdd( p, Cube );
+            return;
+        }
+    }
+    // could not find - simply add this cube
+    Vec_IntPush( vLevel, Cube );
+}
+
+void Eso_ManMinimizeCopy( Eso_Man_t * p, Vec_Int_t * vEsop )
+{
+    Vec_Int_t * vLevel;
+    int i;
+    Vec_IntClear( vEsop );
+    Vec_WecForEachLevel( p->vCubes, vLevel, i )
+    {
+        Vec_IntAppend( vEsop, vLevel );
+        if ( i > 0 )
+        {
+            int k, Cube;
+            Vec_IntForEachEntry( vLevel, Cube, k )
+                assert( Vec_IntSize(Eso_ManCube(p, Cube)) == i );
+        }
+        Vec_IntClear( vLevel );
+    }
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Compute the produce of two covers.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Eso_ManComputeAnd( Eso_Man_t * p, Vec_Int_t * vCube1, Vec_Int_t * vCube2, Vec_Int_t * vCube )
+{
+    int * pBeg  = vCube->pArray;
+    int * pBeg1 = vCube1->pArray;
+    int * pBeg2 = vCube2->pArray;
+    int * pEnd1 = vCube1->pArray + vCube1->nSize;
+    int * pEnd2 = vCube2->pArray + vCube2->nSize;
+    while ( pBeg1 < pEnd1 && pBeg2 < pEnd2 )
+    {
+        if ( *pBeg1 == *pBeg2 )
+            *pBeg++ = *pBeg1++, pBeg2++;
+        else if ( Abc_Lit2Var(*pBeg1) == Abc_Lit2Var(*pBeg2) )
+            return -1;
+        else if ( *pBeg1 < *pBeg2 )
+            *pBeg++ = *pBeg1++;
+        else 
+            *pBeg++ = *pBeg2++;
+    }
+    while ( pBeg1 < pEnd1 )
+        *pBeg++ = *pBeg1++;
+    while ( pBeg2 < pEnd2 )
+        *pBeg++ = *pBeg2++;
+    vCube->nSize = pBeg - vCube->pArray;
+    assert( vCube->nSize <= vCube->nCap );
+    assert( vCube->nSize >= vCube1->nSize );
+    assert( vCube->nSize >= vCube2->nSize );
+    return Hsh_VecManAdd( p->pHash, vCube );
+}
+void Eso_ManComputeOne( Eso_Man_t * p, Vec_Int_t * vEsop1, Vec_Int_t * vEsop2, Vec_Int_t * vEsop )
+{
+    Vec_Int_t vCube1, vCube2;
+    int i, k, Cube1, Cube2, Cube;
+    Vec_IntClear( vEsop );
+    if ( Vec_IntSize(vEsop1) == 0 || Vec_IntSize(vEsop2) == 0 )
+        return;
+    Cube1 = Vec_IntEntry(vEsop1, 0);
+    Cube2 = Vec_IntEntry(vEsop2, 0);
+    Vec_IntForEachEntry( vEsop1, Cube1, i )
+    {
+        if ( Cube1 == p->Cube1 )
+        {
+            Vec_IntForEachEntry( vEsop2, Cube2, k )
+                Eso_ManMinimizeAdd( p, Cube2 );
+            continue;
+        }
+        Vec_IntForEachEntry( vEsop2, Cube2, k )
+        {
+            if ( Cube2 == p->Cube1 )
+            {
+                Eso_ManMinimizeAdd( p, Cube1 );
+                continue;
+            }
+            vCube1 = *Hsh_VecReadEntry( p->pHash, Cube1 );
+            vCube2 = *Hsh_VecReadEntry( p->pHash, Cube2 );
+            Cube = Eso_ManComputeAnd( p, &vCube1, &vCube2, p->vCube );
+            if ( Cube >= 0 )
+                Eso_ManMinimizeAdd( p, Cube );
+        }
+    }
+    Eso_ManMinimizeCopy( p, vEsop );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Complements the cover if needed, or just copy it.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Vec_Int_t * Eso_ManTransformOne( Eso_Man_t * p, Vec_Int_t * vEsop, int fCompl, Vec_Int_t * vRes )
+{
+    int i, Cube, Start = 0;
+    Vec_IntClear( vRes );
+    if ( fCompl )
+    {
+        if ( Vec_IntSize(vEsop) == 0 )
+            Vec_IntPush( vRes, p->Cube1 );
+        else
+        {
+            Cube = Vec_IntEntry(vEsop, 0);
+            if ( Cube == p->Cube1 )
+                Start = 1;
+            else if ( Cube < 2 * p->nVars )
+                Vec_IntPush( vRes, Abc_LitNot(Cube) ), Start = 1;
+            else
+                Vec_IntPush( vRes, p->Cube1 );
+        }
+    }
+    Vec_IntForEachEntryStart( vEsop, Cube, i, Start )
+        Vec_IntPush( vRes, Cube );
+    return vRes;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Computes ESOP from AIG.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Gia_Man_t * Eso_ManCompute( Gia_Man_t * pGia, int fVerbose )
+{
+    abctime clk = Abc_Clock();
+    Vec_Ptr_t * vCover;
+    Gia_Man_t * pNew;
+    Gia_Obj_t * pObj; int i, nCubes = 0, nCubesUsed = 0;
+    Vec_Int_t * vEsop1, * vEsop2, * vEsop;
+    Eso_Man_t * p = Eso_ManAlloc( pGia );
+    Gia_ManForEachAnd( pGia, pObj, i )
+    {
+        vEsop1 = Vec_WecEntry( p->vEsops, Gia_ObjFaninId0(pObj, i) );
+        vEsop2 = Vec_WecEntry( p->vEsops, Gia_ObjFaninId1(pObj, i) );
+        vEsop1 = Eso_ManTransformOne( p, vEsop1, Gia_ObjFaninC0(pObj), p->vCube1 );
+        vEsop2 = Eso_ManTransformOne( p, vEsop2, Gia_ObjFaninC1(pObj), p->vCube2 );
+        vEsop  = Vec_WecEntry( p->vEsops, i );
+        Eso_ManComputeOne( p, vEsop1, vEsop2, vEsop );
+        nCubes += Vec_IntSize(vEsop);
+    }
+    vCover = Vec_PtrAlloc( Gia_ManCoNum(pGia) );
+    Gia_ManForEachCo( pGia, pObj, i )
+    {
+        vEsop1 = Vec_WecEntry( p->vEsops, Gia_ObjFaninId0p(pGia, pObj) );
+        vEsop1 = Eso_ManTransformOne( p, vEsop1, Gia_ObjFaninC0(pObj), p->vCube1 );
+        printf( "Output %3d:  ESOP has %5d cubes\n", i, Vec_IntSize(vEsop1) );
+        if ( fVerbose )
+            Eso_ManCoverPrint( p, vEsop1 );
+        Vec_PtrPush( vCover, Vec_IntDup(vEsop1) );
+        nCubesUsed += Vec_IntSize(vEsop1);
+    }
+    printf( "Outs = %d.  Cubes = %d.  Used = %d.  Hashed = %d. ", 
+        Gia_ManCoNum(pGia), nCubes, nCubesUsed, Hsh_VecSize(p->pHash) );
+    Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
+    pNew = Eso_ManCoverConvert( p, vCover );
+    Vec_VecFree( (Vec_Vec_t *)vCover );
+    Eso_ManStop( p );
+    return pNew;
+}
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+
+ABC_NAMESPACE_IMPL_END
+

src/aig/gia/module.make

@@ -22,6 +22,7 @@ SRC +=    src/aig/gia/giaAig.c \
     src/aig/gia/giaEquiv.c \
     src/aig/gia/giaEra.c \
     src/aig/gia/giaEra2.c \
+    src/aig/gia/giaEsop.c \
     src/aig/gia/giaFadds.c \
     src/aig/gia/giaFalse.c \
     src/aig/gia/giaFanout.c \

src/base/abci/abc.c

@@ -464,6 +464,7 @@ static int Abc_CommandAbc9Bmci               ( Abc_Frame_t * pAbc, int argc, cha
 static int Abc_CommandAbc9PoXsim             ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandAbc9Demiter            ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandAbc9Fadds              ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandAbc9Esop               ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandAbc9Mfs                ( Abc_Frame_t * pAbc, int argc, char ** argv );
 //static int Abc_CommandAbc9PoPart2            ( Abc_Frame_t * pAbc, int argc, char ** argv );
 //static int Abc_CommandAbc9CexCut             ( Abc_Frame_t * pAbc, int argc, char ** argv );
@@ -1090,6 +1091,7 @@ void Abc_Init( Abc_Frame_t * pAbc )
     Cmd_CommandAdd( pAbc, "ABC9",         "&poxsim",       Abc_CommandAbc9PoXsim,       0 );
     Cmd_CommandAdd( pAbc, "ABC9",         "&demiter",      Abc_CommandAbc9Demiter,      0 );
     Cmd_CommandAdd( pAbc, "ABC9",         "&fadds",        Abc_CommandAbc9Fadds,        0 );
+    Cmd_CommandAdd( pAbc, "ABC9",         "&esop",         Abc_CommandAbc9Esop,         0 );
     Cmd_CommandAdd( pAbc, "ABC9",         "&mfs",          Abc_CommandAbc9Mfs,          0 );
 //    Cmd_CommandAdd( pAbc, "ABC9",         "&popart2",      Abc_CommandAbc9PoPart2,      0 );
 //    Cmd_CommandAdd( pAbc, "ABC9",         "&cexcut",       Abc_CommandAbc9CexCut,       0 );
@@ -39165,6 +39167,53 @@ usage:
   SeeAlso     []
 
 ***********************************************************************/
+int Abc_CommandAbc9Esop( Abc_Frame_t * pAbc, int argc, char ** argv )
+{
+    extern Gia_Man_t * Eso_ManCompute( Gia_Man_t * pGia, int fVerbose );
+    Gia_Man_t * pTemp;
+    int c, fVerbose = 0;
+    Extra_UtilGetoptReset();
+    while ( ( c = Extra_UtilGetopt( argc, argv, "vh" ) ) != EOF )
+    {
+        switch ( c )
+        {
+        case 'v':
+            fVerbose ^= 1;
+            break;
+        case 'h':
+            goto usage;
+        default:
+            goto usage;
+        }
+    }
+    if ( pAbc->pGia == NULL )
+    {
+        Abc_Print( -1, "Abc_CommandAbc9Esop(): There is no AIG.\n" );
+        return 0;
+    }
+    pTemp = Eso_ManCompute( pAbc->pGia, fVerbose );
+    Abc_FrameUpdateGia( pAbc, pTemp );
+    return 0;
+
+usage:
+    Abc_Print( -2, "usage: &esop [-vh]\n" );
+    Abc_Print( -2, "\t         derives Exclusive Sum of Products from AIG\n" );
+    Abc_Print( -2, "\t-v     : toggles printing verbose information [default = %s]\n",  fVerbose? "yes": "no" );
+    Abc_Print( -2, "\t-h     : print the command usage\n");
+    return 1;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
 int Abc_CommandAbc9Mfs( Abc_Frame_t * pAbc, int argc, char ** argv )
 {
     extern Gia_Man_t * Gia_ManPerformMfs( Gia_Man_t * p, Sfm_Par_t * pPars );

src/misc/vec/vecHsh.h

@@ -79,6 +79,8 @@ struct Hsh_VecMan_t_
     Vec_Int_t *  vData;       // data storage
     Vec_Int_t *  vMap;        // mapping entries into data;
     Vec_Int_t    vTemp;       // temporary array
+    Vec_Int_t    vTemp1;      // temporary array
+    Vec_Int_t    vTemp2;      // temporary array
 };
 
 ////////////////////////////////////////////////////////////////////////
@@ -305,6 +307,10 @@ static inline void Hsh_VecManStop( Hsh_VecMan_t * p )
     Vec_IntFree( p->vMap );
     ABC_FREE( p );
 }
+static inline int * Hsh_VecReadArray( Hsh_VecMan_t * p, int i )
+{
+    return (int*)Hsh_VecObj(p, i) + 2;
+}
 static inline Vec_Int_t * Hsh_VecReadEntry( Hsh_VecMan_t * p, int i )
 {
     Hsh_VecObj_t * pObj = Hsh_VecObj( p, i );
@@ -312,6 +318,20 @@ static inline Vec_Int_t * Hsh_VecReadEntry( Hsh_VecMan_t * p, int i )
     p->vTemp.pArray = (int*)pObj + 2;
     return &p->vTemp;
 }
+static inline Vec_Int_t * Hsh_VecReadEntry1( Hsh_VecMan_t * p, int i )
+{
+    Hsh_VecObj_t * pObj = Hsh_VecObj( p, i );
+    p->vTemp1.nSize = p->vTemp1.nCap = pObj->nSize;
+    p->vTemp1.pArray = (int*)pObj + 2;
+    return &p->vTemp1;
+}
+static inline Vec_Int_t * Hsh_VecReadEntry2( Hsh_VecMan_t * p, int i )
+{
+    Hsh_VecObj_t * pObj = Hsh_VecObj( p, i );
+    p->vTemp2.nSize = p->vTemp2.nCap = pObj->nSize;
+    p->vTemp2.pArray = (int*)pObj + 2;
+    return &p->vTemp2;
+}
 static inline int Hsh_VecSize( Hsh_VecMan_t * p )
 {
     return Vec_IntSize(p->vMap);

src/misc/vec/vecPtr.h

@@ -770,6 +770,26 @@ static inline void Vec_PtrRemove( Vec_Ptr_t * p, void * Entry )
 
 /**Function*************************************************************
 
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline void Vec_PtrDrop( Vec_Ptr_t * p, int i )
+{
+    int k;
+    assert( i >= 0 && i < Vec_PtrSize(p) );
+    p->nSize--;
+    for ( k = i; k < p->nSize; k++ )
+        p->pArray[k] = p->pArray[k+1];
+}
+
+/**Function*************************************************************
+
   Synopsis    [Interts entry at the index iHere. Shifts other entries.]
 
   Description []