Improvements to LMS code.

8 files changed, 962 insertions, 66 deletions

diff --git a/abclib.dsp b/abclib.dsp
index c729baa9..51a06e45 100644
--- a/abclib.dsp
+++ b/abclib.dsp
@@ -391,6 +391,10 @@ SOURCE=.\src\base\abci\abcRec2.c
 # End Source File
 # Begin Source File
 
+SOURCE=.\src\base\abci\abcRec3.c
+# End Source File
+# Begin Source File
+
 SOURCE=.\src\base\abci\abcReconv.c
 # End Source File
 # Begin Source File
diff --git a/src/base/abc/abc.h b/src/base/abc/abc.h
index f8e16cd6..22a91bb3 100644
--- a/src/base/abc/abc.h
+++ b/src/base/abc/abc.h
@@ -798,6 +798,16 @@ extern ABC_DLL void               Abc_NtkRecLibMerge2(Gia_Man_t * pGia);
 extern ABC_DLL int                Abc_NtkRecIsRunning2();
 extern ABC_DLL int                Abc_NtkRecIsInTrimMode2();
 extern ABC_DLL void               Abc_NtkRecFilter2(int nLimit);
+/*=== abcRec3.c ==========================================================*/
+extern ABC_DLL void               Abc_NtkRecStart3( Gia_Man_t *p, int nVars, int nCuts, int fTrim );
+extern ABC_DLL void               Abc_NtkRecStop3();
+extern ABC_DLL void               Abc_NtkRecAdd3( Abc_Ntk_t * pNtk, int fUseSOPB );
+extern ABC_DLL void               Abc_NtkRecPs3(int fPrintLib);
+extern ABC_DLL Gia_Man_t *        Abc_NtkRecGetGia3();
+extern ABC_DLL int                Abc_NtkRecIsRunning3();
+//extern ABC_DLL int                Abc_NtkRecIsInTrimMode3();
+//extern ABC_DLL void               Abc_NtkRecLibMerge3(Gia_Man_t * pGia);
+//extern ABC_DLL void               Abc_NtkRecFilter3(int nLimit);
 /*=== abcReconv.c ==========================================================*/
 extern ABC_DLL Abc_ManCut_t *     Abc_NtkManCutStart( int nNodeSizeMax, int nConeSizeMax, int nNodeFanStop, int nConeFanStop );
 extern ABC_DLL void               Abc_NtkManCutStop( Abc_ManCut_t * p );
diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c
index ed78f04e..497008a6 100644
--- a/src/base/abci/abc.c
+++ b/src/base/abci/abc.c
@@ -201,20 +201,26 @@ static int Abc_CommandFraigDress             ( Abc_Frame_t * pAbc, int argc, cha
 
 static int Abc_CommandRecStart               ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandRecStop                ( Abc_Frame_t * pAbc, int argc, char ** argv );
-static int Abc_CommandRecAdd                 ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandRecPs                  ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandRecAdd                 ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandRecUse                 ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandRecFilter              ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandRecMerge               ( Abc_Frame_t * pAbc, int argc, char ** argv );
 
 static int Abc_CommandRecStart2              ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandRecStop2               ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandRecPs2                 ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandRecAdd2                ( Abc_Frame_t * pAbc, int argc, char ** argv );
-static int Abc_CommandRecStop2               ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandRecDump2               ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandRecMerge2              ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandRecFilter2             ( Abc_Frame_t * pAbc, int argc, char ** argv );
 
+static int Abc_CommandRecStart3              ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandRecStop3               ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandRecPs3                 ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandRecAdd3                ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandRecDump3               ( Abc_Frame_t * pAbc, int argc, char ** argv );
+
 static int Abc_CommandMap                    ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandAmap                   ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandUnmap                  ( Abc_Frame_t * pAbc, int argc, char ** argv );
@@ -656,13 +662,19 @@ void Abc_Init( Abc_Frame_t * pAbc )
     Cmd_CommandAdd( pAbc, "Choicing",     "rec_filter",    Abc_CommandRecFilter,        1 );
     Cmd_CommandAdd( pAbc, "Choicing",     "rec_merge",     Abc_CommandRecMerge,         1 );
 
-    Cmd_CommandAdd( pAbc, "Choicing",     "rec_start2",     Abc_CommandRecStart2,         0 );
-    Cmd_CommandAdd( pAbc, "Choicing",     "rec_stop2",      Abc_CommandRecStop2,          0 );
-    Cmd_CommandAdd( pAbc, "Choicing",     "rec_add2",       Abc_CommandRecAdd2,           0 );
-    Cmd_CommandAdd( pAbc, "Choicing",     "rec_ps2",        Abc_CommandRecPs2,            0 );
-    Cmd_CommandAdd( pAbc, "Choicing",     "rec_dump2",       Abc_CommandRecDump2,         1 );
-    Cmd_CommandAdd( pAbc, "Choicing",     "rec_filter2",    Abc_CommandRecFilter2,        1 );
-    Cmd_CommandAdd( pAbc, "Choicing",     "rec_merge2",     Abc_CommandRecMerge2,         1 );
+    Cmd_CommandAdd( pAbc, "Choicing",     "rec_start2",    Abc_CommandRecStart2,        0 );
+    Cmd_CommandAdd( pAbc, "Choicing",     "rec_stop2",     Abc_CommandRecStop2,         0 );
+    Cmd_CommandAdd( pAbc, "Choicing",     "rec_ps2",       Abc_CommandRecPs2,           0 );
+    Cmd_CommandAdd( pAbc, "Choicing",     "rec_add2",      Abc_CommandRecAdd2,          0 );
+    Cmd_CommandAdd( pAbc, "Choicing",     "rec_dump2",     Abc_CommandRecDump2,         1 );
+    Cmd_CommandAdd( pAbc, "Choicing",     "rec_filter2",   Abc_CommandRecFilter2,       1 );
+    Cmd_CommandAdd( pAbc, "Choicing",     "rec_merge2",    Abc_CommandRecMerge2,        1 );
+
+    Cmd_CommandAdd( pAbc, "Choicing",     "rec_start3",    Abc_CommandRecStart3,        0 );
+    Cmd_CommandAdd( pAbc, "Choicing",     "rec_stop3",     Abc_CommandRecStop3,         0 );
+    Cmd_CommandAdd( pAbc, "Choicing",     "rec_ps3",       Abc_CommandRecPs3,           0 );
+    Cmd_CommandAdd( pAbc, "Choicing",     "rec_add3",      Abc_CommandRecAdd3,          0 );
+    Cmd_CommandAdd( pAbc, "Choicing",     "rec_dump3",     Abc_CommandRecDump3,         1 );
 
     Cmd_CommandAdd( pAbc, "SC mapping",   "map",           Abc_CommandMap,              1 );
     Cmd_CommandAdd( pAbc, "SC mapping",   "amap",          Abc_CommandAmap,             1 );
@@ -12317,19 +12329,18 @@ usage:
   SeeAlso     []
 
 ***********************************************************************/
-int Abc_CommandRecAdd( Abc_Frame_t * pAbc, int argc, char ** argv )
+int Abc_CommandRecPs( Abc_Frame_t * pAbc, int argc, char ** argv )
 {
-    Abc_Ntk_t * pNtk = Abc_FrameReadNtk(pAbc);
-    int c;
-    int fUseSOPB = 0;
+//    Abc_Ntk_t * pNtk = Abc_FrameReadNtk(pAbc);
+    int c, fPrintLib = 0;
     // set defaults
     Extra_UtilGetoptReset();
-    while ( ( c = Extra_UtilGetopt( argc, argv, "gh" ) ) != EOF )
+    while ( ( c = Extra_UtilGetopt( argc, argv, "ph" ) ) != EOF )
     {
         switch ( c )
         {
-        case 'g':
-            fUseSOPB = 1;
+        case 'p':
+            fPrintLib ^= 1;
             break;
         case 'h':
             goto usage;
@@ -12337,22 +12348,17 @@ int Abc_CommandRecAdd( Abc_Frame_t * pAbc, int argc, char ** argv )
             goto usage;
         }
     }
-    if ( !Abc_NtkIsStrash(pNtk) )
-    {
-        Abc_Print( -1, "This command works for AIGs.\n" );
-        return 0;
-    }
     if ( !Abc_NtkRecIsRunning() )
     {
-        Abc_Print( -1, "This command works for AIGs after calling \"rec_start\".\n" );
+        Abc_Print( -1, "This command works for AIGs only after calling \"rec_start\".\n" );
         return 0;
     }
-    Abc_NtkRecAdd( pNtk, fUseSOPB);
+    Abc_NtkRecPs(fPrintLib);
     return 0;
 
 usage:
-    Abc_Print( -2, "usage: rec_add [-h]\n" );
-    Abc_Print( -2, "\t        adds subgraphs from the current network to the set\n" );
+    Abc_Print( -2, "usage: rec_ps [-h]\n" );
+    Abc_Print( -2, "\t        prints statistics about the recorded AIG subgraphs\n" );
     Abc_Print( -2, "\t-h    : print the command usage\n");
     return 1;
 }
@@ -12368,18 +12374,19 @@ usage:
   SeeAlso     []
 
 ***********************************************************************/
-int Abc_CommandRecPs( Abc_Frame_t * pAbc, int argc, char ** argv )
+int Abc_CommandRecAdd( Abc_Frame_t * pAbc, int argc, char ** argv )
 {
-//    Abc_Ntk_t * pNtk = Abc_FrameReadNtk(pAbc);
-    int c, fPrintLib = 0;
+    Abc_Ntk_t * pNtk = Abc_FrameReadNtk(pAbc);
+    int c;
+    int fUseSOPB = 0;
     // set defaults
     Extra_UtilGetoptReset();
-    while ( ( c = Extra_UtilGetopt( argc, argv, "ph" ) ) != EOF )
+    while ( ( c = Extra_UtilGetopt( argc, argv, "gh" ) ) != EOF )
     {
         switch ( c )
         {
-        case 'p':
-            fPrintLib ^= 1;
+        case 'g':
+            fUseSOPB = 1;
             break;
         case 'h':
             goto usage;
@@ -12387,17 +12394,22 @@ int Abc_CommandRecPs( Abc_Frame_t * pAbc, int argc, char ** argv )
             goto usage;
         }
     }
+    if ( !Abc_NtkIsStrash(pNtk) )
+    {
+        Abc_Print( -1, "This command works for AIGs.\n" );
+        return 0;
+    }
     if ( !Abc_NtkRecIsRunning() )
     {
-        Abc_Print( -1, "This command works for AIGs only after calling \"rec_start\".\n" );
+        Abc_Print( -1, "This command works for AIGs after calling \"rec_start\".\n" );
         return 0;
     }
-    Abc_NtkRecPs(fPrintLib);
+    Abc_NtkRecAdd( pNtk, fUseSOPB);
     return 0;
 
 usage:
-    Abc_Print( -2, "usage: rec_ps [-h]\n" );
-    Abc_Print( -2, "\t        prints statistics about the recorded AIG subgraphs\n" );
+    Abc_Print( -2, "usage: rec_add [-h]\n" );
+    Abc_Print( -2, "\t        adds subgraphs from the current network to the set\n" );
     Abc_Print( -2, "\t-h    : print the command usage\n");
     return 1;
 }
@@ -12733,19 +12745,18 @@ usage:
   SeeAlso     []
 
 ***********************************************************************/
-int Abc_CommandRecAdd2( Abc_Frame_t * pAbc, int argc, char ** argv )
+int Abc_CommandRecPs2( Abc_Frame_t * pAbc, int argc, char ** argv )
 {
-    Abc_Ntk_t * pNtk = Abc_FrameReadNtk(pAbc);
-    int c;
-    int fUseSOPB = 0;
+//    Abc_Ntk_t * pNtk = Abc_FrameReadNtk(pAbc);
+    int c, fPrintLib = 0;
     // set defaults
     Extra_UtilGetoptReset();
-    while ( ( c = Extra_UtilGetopt( argc, argv, "gh" ) ) != EOF )
+    while ( ( c = Extra_UtilGetopt( argc, argv, "ph" ) ) != EOF )
     {
         switch ( c )
         {
-        case 'g':
-            fUseSOPB = 1;
+        case 'p':
+            fPrintLib ^= 1;
             break;
         case 'h':
             goto usage;
@@ -12753,22 +12764,17 @@ int Abc_CommandRecAdd2( Abc_Frame_t * pAbc, int argc, char ** argv )
             goto usage;
         }
     }
-    if ( !Abc_NtkIsStrash(pNtk) )
-    {
-        Abc_Print( -1, "This command works for AIGs.\n" );
-        return 0;
-    }
     if ( !Abc_NtkRecIsRunning2() )
     {
-        Abc_Print( -1, "This command works for AIGs after calling \"rec_start2\".\n" );
+        Abc_Print( -1, "This command works for AIGs only after calling \"rec_start2\".\n" );
         return 0;
     }
-    Abc_NtkRecAdd2( pNtk, fUseSOPB);
+    Abc_NtkRecPs2(fPrintLib);
     return 0;
 
 usage:
-    Abc_Print( -2, "usage: rec_add2 [-h]\n" );
-    Abc_Print( -2, "\t        adds subgraphs from the current network to the set\n" );
+    Abc_Print( -2, "usage: rec_ps2 [-h]\n" );
+    Abc_Print( -2, "\t        prints statistics about the recorded AIG subgraphs\n" );
     Abc_Print( -2, "\t-h    : print the command usage\n");
     return 1;
 }
@@ -12785,18 +12791,19 @@ usage:
   SeeAlso     []
 
 ***********************************************************************/
-int Abc_CommandRecPs2( Abc_Frame_t * pAbc, int argc, char ** argv )
+int Abc_CommandRecAdd2( Abc_Frame_t * pAbc, int argc, char ** argv )
 {
-//    Abc_Ntk_t * pNtk = Abc_FrameReadNtk(pAbc);
-    int c, fPrintLib = 0;
+    Abc_Ntk_t * pNtk = Abc_FrameReadNtk(pAbc);
+    int c;
+    int fUseSOPB = 0;
     // set defaults
     Extra_UtilGetoptReset();
-    while ( ( c = Extra_UtilGetopt( argc, argv, "ph" ) ) != EOF )
+    while ( ( c = Extra_UtilGetopt( argc, argv, "gh" ) ) != EOF )
     {
         switch ( c )
         {
-        case 'p':
-            fPrintLib ^= 1;
+        case 'g':
+            fUseSOPB = 1;
             break;
         case 'h':
             goto usage;
@@ -12804,17 +12811,22 @@ int Abc_CommandRecPs2( Abc_Frame_t * pAbc, int argc, char ** argv )
             goto usage;
         }
     }
+    if ( !Abc_NtkIsStrash(pNtk) )
+    {
+        Abc_Print( -1, "This command works for AIGs.\n" );
+        return 0;
+    }
     if ( !Abc_NtkRecIsRunning2() )
     {
-        Abc_Print( -1, "This command works for AIGs only after calling \"rec_start2\".\n" );
+        Abc_Print( -1, "This command works for AIGs after calling \"rec_start2\".\n" );
         return 0;
     }
-    Abc_NtkRecPs2(fPrintLib);
+    Abc_NtkRecAdd2( pNtk, fUseSOPB);
     return 0;
 
 usage:
-    Abc_Print( -2, "usage: rec_ps2 [-h]\n" );
-    Abc_Print( -2, "\t        prints statistics about the recorded AIG subgraphs\n" );
+    Abc_Print( -2, "usage: rec_add2 [-h]\n" );
+    Abc_Print( -2, "\t        adds subgraphs from the current network to the set\n" );
     Abc_Print( -2, "\t-h    : print the command usage\n");
     return 1;
 }
@@ -13023,6 +13035,318 @@ usage:
 }
 
 
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Abc_CommandRecStart3( Abc_Frame_t * pAbc, int argc, char ** argv )
+{
+    char * FileName, * pTemp;
+    char ** pArgvNew;
+    int c, nArgcNew;
+    FILE * pFile;
+    Gia_Man_t * pGia = NULL;
+    int nVars = 6;
+    int nCuts = 32;
+    int fTrim = 0;
+    Extra_UtilGetoptReset();
+    while ( ( c = Extra_UtilGetopt( argc, argv, "KCth" ) ) != EOF )
+    {
+        switch ( c )
+        {
+        case 'K':
+            if ( globalUtilOptind >= argc )
+            {
+                Abc_Print( -1, "Command line switch \"-K\" should be followed by an integer.\n" );
+                goto usage;
+            }
+            nVars = atoi(argv[globalUtilOptind]);
+            globalUtilOptind++;
+            if ( nVars < 1 ) 
+                goto usage;
+            break;
+        case 'C':
+            if ( globalUtilOptind >= argc )
+            {
+                Abc_Print( -1, "Command line switch \"-C\" should be followed by an integer.\n" );
+                goto usage;
+            }
+            nCuts = atoi(argv[globalUtilOptind]);
+            globalUtilOptind++;
+            if ( nCuts < 1 ) 
+                goto usage;
+            break;
+        case 't':
+            fTrim ^= 1;
+            break;
+        case 'h':
+            goto usage;
+        default:
+            goto usage;
+        }
+    }
+    if ( !(nVars >= 3 && nVars <= 16) )
+    {
+        Abc_Print( -1, "The range of allowed values is 3 <= K <= 16.\n" );
+        return 0;
+    }
+    if ( Abc_NtkRecIsRunning3() )
+    {
+        Abc_Print( -1, "The AIG subgraph recording is already started.\n" );
+        return 0;
+    }
+    pArgvNew = argv + globalUtilOptind;
+    nArgcNew = argc - globalUtilOptind;
+    if ( nArgcNew != 1 )
+        Abc_Print( 1, "File name is not given on the command line. Start a new record.\n" );
+    else
+    {   
+        // get the input file name
+        FileName = pArgvNew[0];
+        // fix the wrong symbol
+        for ( pTemp = FileName; *pTemp; pTemp++ )
+            if ( *pTemp == '>' )
+                *pTemp = '\\';
+        if ( (pFile = fopen( FileName, "r" )) == NULL )
+        {
+            Abc_Print( -1, "Cannot open input file \"%s\". ", FileName );
+            if ( (FileName = Extra_FileGetSimilarName( FileName, ".aig", NULL, NULL, NULL, NULL )) )
+                Abc_Print( 1, "Did you mean \"%s\"?", FileName );
+            Abc_Print( 1, "\n" );
+            return 1;
+        }
+        fclose( pFile );
+        pGia = Gia_ReadAiger( FileName, 1, 0 );
+        if ( pGia == NULL )
+        {
+            Abc_Print( -1, "Reading AIGER has failed.\n" );
+            return 0;
+        }
+    }
+    Abc_NtkRecStart3( pGia, nVars, nCuts, fTrim );
+    return 0;
+
+usage:
+    Abc_Print( -2, "usage: rec_start3 [-K num] [-C num] [-th]\n" );
+    Abc_Print( -2, "\t         starts recording AIG subgraphs (should be called for\n" );
+    Abc_Print( -2, "\t         an empty network or after reading in a previous record)\n" );
+    Abc_Print( -2, "\t-K num : the largest number of inputs [default = %d]\n", nVars );
+    Abc_Print( -2, "\t-C num : the max number of cuts used at a node (0 < num < 2^12) [default = %d]\n", nCuts );
+    Abc_Print( -2, "\t-t     : toggles the use of trimming [default = %s]\n", fTrim? "yes": "no" );
+    Abc_Print( -2, "\t-h     : print the command usage\n");
+    return 1;
+}
+
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Abc_CommandRecStop3( Abc_Frame_t * pAbc, int argc, char ** argv )
+{
+    int c;
+    Extra_UtilGetoptReset();
+    while ( ( c = Extra_UtilGetopt( argc, argv, "dh" ) ) != EOF )
+    {
+        switch ( c )
+        {
+        case 'h':
+            goto usage;
+        default:
+            goto usage;
+        }
+    }
+    if ( !Abc_NtkRecIsRunning3() )
+    {
+        Abc_Print( -1, "This command works only after calling \"rec_start3\".\n" );
+        return 0;
+    }
+    Abc_NtkRecStop3();
+    return 0;
+
+usage:
+    Abc_Print( -2, "usage: rec_stop3 [-h]\n" );
+    Abc_Print( -2, "\t        cleans the internal storage for AIG subgraphs\n" );
+    Abc_Print( -2, "\t-h    : print the command usage\n");
+    return 1;
+}
+
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Abc_CommandRecPs3( Abc_Frame_t * pAbc, int argc, char ** argv )
+{
+    int c, fPrintLib = 0;
+    Extra_UtilGetoptReset();
+    while ( ( c = Extra_UtilGetopt( argc, argv, "ph" ) ) != EOF )
+    {
+        switch ( c )
+        {
+        case 'p':
+            fPrintLib ^= 1;
+            break;
+        case 'h':
+            goto usage;
+        default:
+            goto usage;
+        }
+    }
+    if ( !Abc_NtkRecIsRunning3() )
+    {
+        Abc_Print( -1, "This command works for AIGs only after calling \"rec_start2\".\n" );
+        return 0;
+    }
+    Abc_NtkRecPs3(fPrintLib);
+    return 0;
+
+usage:
+    Abc_Print( -2, "usage: rec_ps3 [-h]\n" );
+    Abc_Print( -2, "\t        prints statistics about the recorded AIG subgraphs\n" );
+    Abc_Print( -2, "\t-h    : print the command usage\n");
+    return 1;
+}
+
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Abc_CommandRecAdd3( Abc_Frame_t * pAbc, int argc, char ** argv )
+{
+    Abc_Ntk_t * pNtk = Abc_FrameReadNtk(pAbc);
+    int c;
+    int fUseSOPB = 0;
+    // set defaults
+    Extra_UtilGetoptReset();
+    while ( ( c = Extra_UtilGetopt( argc, argv, "gh" ) ) != EOF )
+    {
+        switch ( c )
+        {
+        case 'g':
+            fUseSOPB = 1;
+            break;
+        case 'h':
+            goto usage;
+        default:
+            goto usage;
+        }
+    }
+    if ( !Abc_NtkIsStrash(pNtk) )
+    {
+        Abc_Print( -1, "This command works for AIGs.\n" );
+        return 0;
+    }
+    if ( !Abc_NtkRecIsRunning3() )
+    {
+        Abc_Print( -1, "This command works for AIGs after calling \"rec_start2\".\n" );
+        return 0;
+    }
+    Abc_NtkRecAdd3( pNtk, fUseSOPB );
+    return 0;
+
+usage:
+    Abc_Print( -2, "usage: rec_add3 [-h]\n" );
+    Abc_Print( -2, "\t        adds subgraphs from the current network to the set\n" );
+    Abc_Print( -2, "\t-h    : print the command usage\n");
+    return 1;
+}
+
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Abc_CommandRecDump3( Abc_Frame_t * pAbc, int argc, char ** argv )
+{
+    char * FileName;
+    char ** pArgvNew;
+    int nArgcNew;
+    Gia_Man_t * pGia;
+    int c;
+
+    Extra_UtilGetoptReset();
+    while ( ( c = Extra_UtilGetopt( argc, argv, "h" ) ) != EOF )
+    {
+        switch ( c )
+        {
+        case 'h':
+            goto usage;
+        default:
+            goto usage;
+        }
+    }
+    if ( !Abc_NtkRecIsRunning3() )
+    {
+        Abc_Print( -1, "The AIG subgraph recording is not started.\n" );
+        return 1;
+    }
+
+    pGia = Abc_NtkRecGetGia3();
+    pArgvNew = argv + globalUtilOptind;
+    nArgcNew = argc - globalUtilOptind;
+    if ( nArgcNew != 1 )
+    {
+        Abc_Print( -1, "File name is not given on the command line.\n" );
+        return 1;
+    }
+    else if( Gia_ManPoNum(pGia) == 0 )
+    {
+        Abc_Print( 0, "No structure in the library.\n" );
+        return 1;
+    }
+    else
+    {   
+        // get the input file name
+        FileName = pArgvNew[0];
+        Gia_WriteAiger( pGia, FileName, 0, 0 );
+    }   
+    return 0;
+
+usage:
+    Abc_Print( -2, "usage: rec_dump3 [-h] <file>\n" );
+    Abc_Print( -2, "\t-h     : print the command usage\n");
+    return 1;
+}
+
+
 /**Function*************************************************************
 
   Synopsis    []
diff --git a/src/base/abci/abcRec3.c b/src/base/abci/abcRec3.c
new file mode 100644
index 00000000..0e3fd214
--- /dev/null
+++ b/src/base/abci/abcRec3.c
@@ -0,0 +1,450 @@
+/**CFile****************************************************************
+
+  FileName    [abcRec2.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [Network and node package.]
+
+  Synopsis    [Record of semi-canonical AIG subgraphs.]
+
+  Author      [Allan Yang, Alan Mishchenko]
+  
+  Affiliation [Fudan University in Shanghai, UC Berkeley]
+
+  Date        [Ver. 1.0. Started - June 20, 2005.]
+
+  Revision    [$Id: abcRec.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "base/abc/abc.h"
+#include "map/if/if.h"
+#include "bool/kit/kit.h"
+#include "aig/gia/giaAig.h"
+#include "misc/vec/vecMem.h"
+#include "bool/lucky/lucky.h"
+
+ABC_NAMESPACE_IMPL_START
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+typedef struct Lms_Man_t_ Lms_Man_t;
+struct Lms_Man_t_
+{
+    // parameters
+    int               nVars;        // the number of variables
+    int               nWords;       // the number of TT words
+    int               nCuts;        // the max number of cuts to use
+    int               fFuncOnly;    // record only functions
+    // internal data
+    Gia_Man_t *       pGia;         // the record
+    Vec_Mem_t *       vTtMem;       // truth tables of primary outputs
+    Vec_Int_t *       vTruthPo;     // for each semi-canonical class, last PO where this truth table was seen
+    // subgraph attributes (1-to-1 correspondence with POs of Gia)
+    Vec_Int_t *       vTruthIds;    // truth table IDs of this PO
+    Vec_Int_t *       vEquivs;      // link to the previous PO of the same functional class
+    Vec_Wrd_t *       vDelays;      // pin-to-pin delays of this PO
+    Vec_Str_t *       vCosts;       // number of AND gates in this PO
+    // sugraph usage statistics
+//    Vec_Int_t *       vFreqs;       // frequencies
+    // temporaries
+    Vec_Ptr_t *       vNodes;       // the temporary nodes
+    Vec_Int_t *       vLabels;      // temporary storage for AIG node labels
+    word              pTemp1[1024]; // copy of the truth table
+    word              pTemp2[1024]; // copy of the truth table
+    // statistics 
+    int               nTried;
+    int               nFilterSize;
+    int               nFilterRedund;
+    int               nFilterVolume;
+    int               nFilterTruth;
+    int               nFilterError;
+    int               nFilterSame;
+    int               nAdded;
+    int               nAddedFuncs;
+    // runtime
+    clock_t           timeCollect;
+    clock_t           timeCanon;
+    clock_t           timeBuild;
+    clock_t           timeCheck;
+    clock_t           timeInsert;
+    clock_t           timeOther;
+    clock_t           timeTotal;
+};
+
+static Lms_Man_t * s_pMan = NULL;
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Abc_NtkRecIsRunning3()
+{
+    return s_pMan != NULL;
+}
+Gia_Man_t * Abc_NtkRecGetGia3()
+{
+    return s_pMan->pGia;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Lms_Man_t * Lms_ManStart( int nVars, int nCuts, int fFuncOnly, int fVerbose )
+{
+    Lms_Man_t * p;
+    int i;
+    p = ABC_CALLOC( Lms_Man_t, 1 );
+    // parameters
+    p->nVars = nVars;
+    p->nCuts = nCuts;
+    p->nWords = Abc_Truth6WordNum( nVars );
+    p->fFuncOnly = fFuncOnly;
+    // GIA
+    p->pGia = Gia_ManStart( 10000 );
+    p->pGia->pName = Abc_UtilStrsav( "record" );
+    for ( i = 0; i < nVars; i++ )
+        Gia_ManAppendCi( p->pGia );
+    // truth tables
+    p->vTtMem = Vec_MemAlloc( p->nWords, 12 ); // 32 KB/page for 6-var functions
+    Vec_MemHashAlloc( p->vTtMem, 10000 );
+    p->vTruthPo  = Vec_IntAlloc( 1000 );
+    // subgraph attributes
+    p->vTruthIds = Vec_IntAlloc( 1000 );
+    p->vEquivs   = Vec_IntAlloc( 1000 );
+    p->vDelays   = Vec_WrdAlloc( 1000 );
+    p->vCosts    = Vec_StrAlloc( 1000 );
+    // sugraph usage statistics
+//    p->vFreqs    = Vec_IntAlloc( 1000 );
+    // temporaries
+    p->vNodes    = Vec_PtrAlloc( 1000 );
+    p->vLabels   = Vec_IntAlloc( 1000 );
+    return p;    
+}
+void Lms_ManStop( Lms_Man_t * p )
+{
+    // temporaries
+    Vec_IntFree( p->vLabels );
+    Vec_PtrFree( p->vNodes );
+    // subgraph attributes
+    Vec_IntFree( p->vEquivs );
+    Vec_WrdFree( p->vDelays );
+    Vec_StrFree( p->vCosts );
+    Vec_IntFree( p->vTruthPo );
+    // sugraph usage statistics
+//    Vec_IntFree( p->vFreqs );
+    // truth tables
+    Vec_IntFree( p->vTruthIds );
+    Vec_MemHashFree( p->vTtMem );
+    Vec_MemFree( p->vTtMem );
+    // GIA
+    Gia_ManStop( p->pGia );
+    ABC_FREE( p );
+}
+
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Abc_NtkRecStart3( Gia_Man_t * p, int nVars, int nCuts, int fTrim )
+{
+    assert( s_pMan == NULL );
+    if ( p == NULL )
+        s_pMan = Lms_ManStart( nVars, nCuts, 0, 0 );
+    else
+        s_pMan = NULL;
+}
+
+void Abc_NtkRecStop3()
+{
+    assert( s_pMan != NULL );
+    Lms_ManStop( s_pMan );
+    s_pMan = NULL;
+}
+
+void Abc_NtkRecPs3(int fPrintLib)
+{
+    Lms_Man_t * p = s_pMan;
+
+    printf( "Subgraphs tried                             = %10d. (%6.2f %%)\n", p->nTried,        !p->nTried? 0 : 100.0*p->nTried/p->nTried );
+    printf( "Subgraphs filtered by support size          = %10d. (%6.2f %%)\n", p->nFilterSize,   !p->nTried? 0 : 100.0*p->nFilterSize/p->nTried );
+    printf( "Subgraphs filtered by structural redundancy = %10d. (%6.2f %%)\n", p->nFilterRedund, !p->nTried? 0 : 100.0*p->nFilterRedund/p->nTried );
+    printf( "Subgraphs filtered by volume                = %10d. (%6.2f %%)\n", p->nFilterVolume, !p->nTried? 0 : 100.0*p->nFilterVolume/p->nTried );
+    printf( "Subgraphs filtered by TT redundancy         = %10d. (%6.2f %%)\n", p->nFilterTruth,  !p->nTried? 0 : 100.0*p->nFilterTruth/p->nTried );
+    printf( "Subgraphs filtered by error                 = %10d. (%6.2f %%)\n", p->nFilterError,  !p->nTried? 0 : 100.0*p->nFilterError/p->nTried );
+    printf( "Subgraphs filtered by isomorphism           = %10d. (%6.2f %%)\n", p->nFilterSame,   !p->nTried? 0 : 100.0*p->nFilterSame/p->nTried );
+    printf( "Subgraphs added                             = %10d. (%6.2f %%)\n", p->nAdded,        !p->nTried? 0 : 100.0*p->nAdded/p->nTried );
+    printf( "Functions added                             = %10d. (%6.2f %%)\n", p->nAddedFuncs,   !p->nTried? 0 : 100.0*p->nAddedFuncs/p->nTried );
+
+    p->timeOther = p->timeTotal 
+                        - p->timeCollect 
+                        - p->timeCanon
+                        - p->timeBuild
+                        - p->timeCheck
+                        - p->timeInsert;
+
+    ABC_PRTP( "Runtime: Collect", p->timeCollect, p->timeTotal );
+    ABC_PRTP( "Runtime: Canon  ", p->timeCanon,   p->timeTotal );
+    ABC_PRTP( "Runtime: Build  ", p->timeBuild,   p->timeTotal );
+    ABC_PRTP( "Runtime: Check  ", p->timeCheck,   p->timeTotal );
+    ABC_PRTP( "Runtime: Insert ", p->timeInsert,  p->timeTotal );
+    ABC_PRTP( "Runtime: Other  ", p->timeOther,   p->timeTotal );
+    ABC_PRTP( "Runtime: TOTAL  ", p->timeTotal,   p->timeTotal );
+}
+
+
+/**Function*************************************************************
+
+  Synopsis    [stretch the truthtable to have more input variables.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static void Abc_TtStretch( word * pInOut, int nVarS, int nVarB )
+{
+    int w, i, step, nWords;
+    if ( nVarS == nVarB )
+        return;
+    assert( nVarS < nVarB );
+    step = Abc_Truth6WordNum(nVarS);
+    nWords = Abc_Truth6WordNum(nVarB);
+    if ( step == nWords )
+        return;
+    assert( step < nWords );
+    for ( w = 0; w < nWords; w += step )
+        for ( i = 0; i < step; i++ )
+            pInOut[w + i] = pInOut[i];              
+}
+
+
+/**Function*************************************************************
+
+  Synopsis    [Adds the cut function to the internal storage.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Abc_NtkRecAddCut3( If_Man_t * pIfMan, If_Obj_t * pRoot, If_Cut_t * pCut )
+{
+    char pCanonPerm[16];
+    unsigned uCanonPhase;
+    int i, Index, iFanin0, iFanin1;
+    int nLeaves = If_CutLeaveNum(pCut);
+    Vec_Ptr_t * vNodes = s_pMan->vNodes;
+    Gia_Man_t * pGia = s_pMan->pGia;
+    Gia_Obj_t * pDriver;
+    If_Obj_t * pIfObj;
+    unsigned * pTruth;
+    clock_t clk;
+    s_pMan->nTried++;
+
+    // skip small cuts
+    assert( s_pMan->nVars == (int)pCut->nLimit );
+    if ( nLeaves < 2 )
+    {
+        s_pMan->nFilterSize++;
+        return 1;
+    }
+
+    // collect internal nodes and skip redundant cuts
+clk = clock();
+    If_CutTraverse( pIfMan, pRoot, pCut, vNodes );
+s_pMan->timeCollect += clock() - clk;
+
+    // semi-canonicize truth table
+clk = clock();
+    for ( i = 0; i < Abc_MaxInt(nLeaves, 6); i++ )
+        pCanonPerm[i] = i;
+    memcpy( s_pMan->pTemp1, If_CutTruthW(pCut), s_pMan->nWords * sizeof(word) );
+//    uCanonPhase = luckyCanonicizer_final_fast( s_pMan->pTemp1, nLeaves, pCanonPerm );
+    uCanonPhase = Kit_TruthSemiCanonicize( (unsigned *)s_pMan->pTemp1, (unsigned *)s_pMan->pTemp2, nLeaves, pCanonPerm );
+    if ( nLeaves < 6 )
+        s_pMan->pTemp1[0] = (s_pMan->pTemp1[0] & 0xFFFFFFFF) | (s_pMan->pTemp1[0] << 32);
+    Abc_TtStretch( If_CutTruthW(pCut), nLeaves, s_pMan->nVars );
+s_pMan->timeCanon += clock() - clk;
+    // pCanonPerm and uCanonPhase show what was the variable corresponding to each var in the current truth
+
+clk = clock();
+    // map cut leaves into elementary variables of GIA
+    for ( i = 0; i < nLeaves; i++ )
+    {
+//        printf( "Leaf  " );
+//        If_ObjPrint( If_ManObj( pIfMan, pCut->pLeaves[pCanonPerm[i]] ) );
+        If_ManObj( pIfMan, pCut->pLeaves[pCanonPerm[i]] )->iCopy = Abc_Var2Lit( Gia_ObjId(pGia, Gia_ManPi(pGia, i)), (uCanonPhase >> i) & 1 );
+    }
+    // build internal nodes
+//    printf( "\n" );
+    assert( Vec_PtrSize(vNodes) > 0 );
+    Vec_PtrForEachEntryStart( If_Obj_t *, vNodes, pIfObj, i, nLeaves )
+    {
+//        If_ObjPrint( pIfObj );
+        if ( If_ObjIsCi(pIfObj) )
+        {
+//printf( "Seeing PI in %d.\n", Vec_WrdSize(s_pMan->vDelays) );
+            pIfObj->iCopy = 0;
+            continue;
+        }
+        iFanin0 = Abc_LitNotCond( If_ObjFanin0(pIfObj)->iCopy, If_ObjFaninC0(pIfObj) );
+        iFanin1 = Abc_LitNotCond( If_ObjFanin1(pIfObj)->iCopy, If_ObjFaninC1(pIfObj) );
+        pIfObj->iCopy = Gia_ManHashAnd( pGia, iFanin0, iFanin1 );
+    }
+s_pMan->timeBuild += clock() - clk;
+
+    // check if this node is already driving a PO
+    pDriver = Gia_ManObj(pGia, Abc_Lit2Var(pIfObj->iCopy));
+    if ( pDriver->fMark1 )
+    {
+        s_pMan->nFilterSame++;
+        return 1;
+    }
+
+    // create output
+    assert( If_ObjIsAnd(pIfObj) );
+    Gia_ManAppendCo( pGia, Abc_LitNotCond( pIfObj->iCopy, (uCanonPhase >> nLeaves) & 1 ) );
+    // mark the driver
+    pDriver = Gia_ManObj(pGia, Abc_Lit2Var(pIfObj->iCopy));
+    pDriver->fMark1 = 1;
+
+    // verify truth table
+clk = clock();
+    pTruth = Gia_ObjComputeTruthTable( pGia, Gia_ManPo(pGia, Gia_ManPoNum(pGia)-1) );
+    if ( memcmp( s_pMan->pTemp1, pTruth, s_pMan->nWords * sizeof(word) ) != 0 )
+    {
+/*
+        Kit_DsdPrintFromTruth( pTruth, nLeaves ); printf( "\n" );
+        Kit_DsdPrintFromTruth( (unsigned *)s_pMan->pTemp1, nLeaves ); printf( "\n" );
+        printf( "Truth table verification has failed.\n" );
+*/
+        Vec_IntPush( s_pMan->vTruthIds, -1 ); // truth table IDs
+        Vec_IntPush( s_pMan->vEquivs, -1 );   // truth table IDs
+        Vec_WrdPush( s_pMan->vDelays, 0 );
+        Vec_StrPush( s_pMan->vCosts, 0 );
+        s_pMan->nFilterTruth++;
+        return 1;
+    }
+s_pMan->timeCheck += clock() - clk;
+
+    // add the resulting truth table to the hash table 
+clk = clock();
+    s_pMan->nAdded++;
+    Index = Vec_MemHashInsert( s_pMan->vTtMem, s_pMan->pTemp1 );
+    Vec_IntPush( s_pMan->vTruthIds, Index ); // truth table IDs
+    assert( Gia_ManPoNum(pGia) == Vec_IntSize(s_pMan->vTruthIds) );
+    if ( Index < Vec_IntSize(s_pMan->vTruthPo) ) // old ID -- add to linked list
+    {
+        Vec_IntPush( s_pMan->vEquivs, Vec_IntEntry(s_pMan->vTruthPo, Index) );
+        Vec_IntWriteEntry( s_pMan->vTruthPo, Index, Gia_ManPoNum(pGia) - 1 );
+    }
+    else
+    {
+        assert( Index == Vec_IntSize(s_pMan->vTruthPo) );
+        Vec_IntPush( s_pMan->vTruthPo, Gia_ManPoNum(pGia) - 1 );
+        Vec_IntPush( s_pMan->vEquivs, -1 );
+        s_pMan->nAddedFuncs++;
+    }
+    Vec_WrdPush( s_pMan->vDelays, 0 );
+    Vec_StrPush( s_pMan->vCosts, 0 );
+s_pMan->timeInsert += clock() - clk;
+    return 1;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Abc_NtkRecAdd3( Abc_Ntk_t * pNtk, int fUseSOPB )
+{
+    extern Abc_Ntk_t * Abc_NtkIf( Abc_Ntk_t * pNtk, If_Par_t * pPars );
+    If_Par_t Pars, * pPars = &Pars;
+    Abc_Ntk_t * pNtkNew;
+    int clk = clock();
+    if ( Abc_NtkGetChoiceNum( pNtk ) )
+        printf( "Performing recoding structures with choices.\n" );
+    // create hash table if not available
+    if ( s_pMan->pGia->pHTable == NULL )
+        Gia_ManHashStart( s_pMan->pGia );
+
+    // set defaults
+    memset( pPars, 0, sizeof(If_Par_t) );
+    // user-controlable paramters
+    pPars->nLutSize    =  s_pMan->nVars;
+    pPars->nCutsMax    =  s_pMan->nCuts;
+    pPars->DelayTarget = -1;
+    pPars->Epsilon     =  (float)0.005;
+    pPars->fArea       =  1;
+    // internal parameters
+    if ( fUseSOPB )
+    {
+        pPars->fTruth      =  1;
+        pPars->fCutMin     =  0;
+        pPars->fUsePerm    =  1; 
+        pPars->fDelayOpt   =  1;
+    }
+    else
+    {
+        pPars->fTruth      =  1;
+        pPars->fCutMin     =  1;
+        pPars->fUsePerm    =  0; 
+        pPars->fDelayOpt   =  0;
+    }
+    pPars->fSkipCutFilter = 0;
+    pPars->pFuncCost   =  NULL;
+    pPars->pFuncUser   =  Abc_NtkRecAddCut3;
+    // perform recording
+    pNtkNew = Abc_NtkIf( pNtk, pPars );
+    Abc_NtkDelete( pNtkNew );
+s_pMan->timeTotal += clock() - clk;
+}
+
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+
+ABC_NAMESPACE_IMPL_END
\ No newline at end of file
diff --git a/src/base/abci/module.make b/src/base/abci/module.make
index d96afbd1..90bdb419 100644
--- a/src/base/abci/module.make
+++ b/src/base/abci/module.make
@@ -46,6 +46,7 @@ SRC +=    src/base/abci/abc.c \
     src/base/abci/abcQuant.c \
     src/base/abci/abcRec.c \
     src/base/abci/abcRec2.c \
+    src/base/abci/abcRec3.c \
     src/base/abci/abcReconv.c \
     src/base/abci/abcReach.c \
     src/base/abci/abcRefactor.c \
diff --git a/src/map/if/if.h b/src/map/if/if.h
index 5c877c9d..7928245f 100644
--- a/src/map/if/if.h
+++ b/src/map/if/if.h
@@ -528,6 +528,7 @@ extern Vec_Int_t *     If_ManCollectMappingInt( If_Man_t * p );
 
 extern int             If_ManCountSpecialPos( If_Man_t * p );
 extern void            If_CutTraverse( If_Man_t * p, If_Obj_t * pRoot, If_Cut_t * pCut, Vec_Ptr_t * vNodes );
+extern void            If_ObjPrint( If_Obj_t * pObj );
 
 /*=== abcRec.c ============================================================*/
 extern int             If_CutDelayRecCost(If_Man_t* p, If_Cut_t* pCut, If_Obj_t * pObj);
diff --git a/src/map/if/ifUtil.c b/src/map/if/ifUtil.c
index 33d984c3..b8b03d70 100644
--- a/src/map/if/ifUtil.c
+++ b/src/map/if/ifUtil.c
@@ -820,6 +820,39 @@ void If_CutTraverseTest( If_Man_t * p, If_Obj_t * pRoot, If_Cut_t * pCut )
     Vec_PtrFree( vNodes );
 }
 
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void If_ObjPrint( If_Obj_t * pObj )
+{
+    if ( pObj == NULL )
+    {
+        printf( "Object is NULL." );
+        return;
+    }
+    printf( "Obj %4d : ", If_ObjId(pObj) );
+    if ( If_ObjIsConst1(pObj) )
+        printf( "constant 1" );
+    else if ( If_ObjIsCi(pObj) )
+        printf( "PI" );
+    else if ( If_ObjIsCo(pObj) )
+        printf( "PO( %4d%s )", If_ObjId(If_ObjFanin0(pObj)), (If_ObjFaninC0(pObj)? "\'" : " ") );
+    else
+        printf( "AND( %4d%s, %4d%s )", 
+            If_ObjId(If_ObjFanin0(pObj)), (If_ObjFaninC0(pObj)? "\'" : " "), 
+            If_ObjId(If_ObjFanin1(pObj)), (If_ObjFaninC1(pObj)? "\'" : " ") );
+    printf( " (refs = %3d)", pObj->nVisitsCopy );
+    printf( "\n" );
+}
+
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////
diff --git a/src/misc/vec/vecMem.h b/src/misc/vec/vecMem.h
index 229c53a2..6367a272 100644
--- a/src/misc/vec/vecMem.h
+++ b/src/misc/vec/vecMem.h
@@ -57,14 +57,16 @@ struct Vec_Mem_t_
     int              nPageAlloc;  // number of pages currently allocated
     int              iPage;       // the number of a page currently used   
     word **          ppPages;     // memory pages
+    Vec_Int_t *      vTable;      // hash table
+    Vec_Int_t *      vNexts;      // next pointers
 };
 
 ////////////////////////////////////////////////////////////////////////
 ///                      MACRO DEFINITIONS                           ///
 ////////////////////////////////////////////////////////////////////////
 
-#define Vec_MemForEachEntry( vVec, pEntry, i )                                              \
-    for ( i = 0; (i < Vec_MemEntryNum(vVec)) && ((pEntry) = Vec_MemReadEntry(vVec, i)); i++ )
+#define Vec_MemForEachEntry( p, pEntry, i )                                              \
+    for ( i = 0; (i < Vec_MemEntryNum(p)) && ((pEntry) = Vec_MemReadEntry(p, i)); i++ )
 
 ////////////////////////////////////////////////////////////////////////
 ///                     FUNCTION DEFINITIONS                         ///
@@ -266,12 +268,12 @@ static inline void Vec_MemShrink( Vec_Mem_t * p, int nEntriesNew )
   SeeAlso     []
 
 ***********************************************************************/
-static inline void Vec_MemPrint( Vec_Mem_t * vVec )
+static inline void Vec_MemPrint( Vec_Mem_t * p )
 {
     word * pEntry;
     int i;
-    printf( "Memory vector has %d entries: ", Vec_MemEntryNum(vVec) );
-    Vec_MemForEachEntry( vVec, pEntry, i )
+    printf( "Memory vector has %d entries: ", Vec_MemEntryNum(p) );
+    Vec_MemForEachEntry( p, pEntry, i )
     {
         printf( "%3d : ", i );
         // add printout here
@@ -279,6 +281,77 @@ static inline void Vec_MemPrint( Vec_Mem_t * vVec )
     }
 }
 
+/**Function*************************************************************
+
+  Synopsis    [Hashing entries in the memory vector.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline void Vec_MemHashAlloc( Vec_Mem_t * p, int nTableSize )
+{
+    assert( p->vTable == NULL && p->vNexts == NULL );
+    p->vTable = Vec_IntStartFull( Abc_PrimeCudd(nTableSize) );
+    p->vNexts = Vec_IntAlloc( nTableSize );
+}
+static inline void Vec_MemHashFree( Vec_Mem_t * p )
+{
+    Vec_IntFreeP( &p->vTable );
+    Vec_IntFreeP( &p->vNexts );
+}
+static inline unsigned Vec_MemHashKey( Vec_Mem_t * p, word * pEntry )
+{
+    static int s_Primes[8] = { 1699, 4177, 5147, 5647, 6343, 7103, 7873, 8147 };
+    int i, nData = 2 * p->nEntrySize;
+    unsigned * pData = (unsigned *)pEntry;
+    unsigned uHash = 0;
+    for ( i = 0; i < nData; i++ )
+        uHash += pData[i] * s_Primes[i & 0x7];
+    return uHash % Vec_IntSize(p->vTable);
+}
+static int * Vec_MemHashLookup( Vec_Mem_t * p, word * pEntry )
+{
+    int * pSpot = Vec_IntEntryP( p->vTable, Vec_MemHashKey(p, pEntry) );
+    for ( ; *pSpot != -1; pSpot = Vec_IntEntryP(p->vNexts, *pSpot) )
+        if ( !memcmp( Vec_MemReadEntry(p, *pSpot), pEntry, sizeof(word) * p->nEntrySize ) ) // equal
+            return pSpot;
+    return pSpot;
+}
+static void Vec_MemHashResize( Vec_Mem_t * p )
+{
+    word * pEntry;
+    int i, * pSpot;
+    Vec_IntFill( p->vTable, Abc_PrimeCudd(2 * Vec_IntSize(p->vTable)), -1 );
+    Vec_IntClear( p->vNexts );
+    Vec_MemForEachEntry( p, pEntry, i )
+    {
+        pSpot = Vec_MemHashLookup( p, pEntry );
+        assert( *pSpot == -1 );
+        *pSpot = Vec_IntSize(p->vNexts);
+        Vec_IntPush( p->vNexts, -1 );
+    }
+    assert( p->nEntries == Vec_IntSize(p->vNexts) );
+}
+static int Vec_MemHashInsert( Vec_Mem_t * p, word * pEntry )
+{
+    int * pSpot;
+    if ( p->nEntries > Vec_IntSize(p->vTable) )
+        Vec_MemHashResize( p );
+    pSpot = Vec_MemHashLookup( p, pEntry );
+    if ( *pSpot == -1 )
+    {
+        *pSpot = Vec_IntSize(p->vNexts);
+        Vec_IntPush( p->vNexts, -1 );
+        Vec_MemPush( p, pEntry );
+        assert( p->nEntries == Vec_IntSize(p->vNexts) );
+    }
+    return *pSpot;
+}
+
 
 ABC_NAMESPACE_HEADER_END