Experiments with iterative synthesis.

7 files changed, 264 insertions, 42 deletions

diff --git a/src/aig/gia/giaDeep.c b/src/aig/gia/giaDeep.c
index f8b2930e..aa9e9cb2 100644
--- a/src/aig/gia/giaDeep.c
+++ b/src/aig/gia/giaDeep.c
@@ -19,14 +19,14 @@
 ***********************************************************************/
 
 #include "gia.h"
+#include "base/main/main.h"
+#include "base/cmd/cmd.h"
 
 ABC_NAMESPACE_IMPL_START
 
-
 ////////////////////////////////////////////////////////////////////////
 ///                        DECLARATIONS                              ///
 ////////////////////////////////////////////////////////////////////////
- 
 
 ////////////////////////////////////////////////////////////////////////
 ///                     FUNCTION DEFINITIONS                         ///
@@ -43,9 +43,108 @@ ABC_NAMESPACE_IMPL_START
   SeeAlso     []
 
 ***********************************************************************/
-Gia_Man_t * Gia_ManDeepSyn( Gia_Man_t * pGia, int TimeOut, int nAnds, int Seed, int fVerbose )
+Gia_Man_t * Gia_ManDeepSynOne( int nNoImpr, int TimeOut, int nAnds, int Seed, int fUseTwo, int fVerbose )
+{
+    abctime nTimeToStop = TimeOut ? Abc_Clock() + TimeOut * CLOCKS_PER_SEC : 0;
+    abctime clkStart    = Abc_Clock();
+    int s, i, IterMax   = 100000, nAndsMin = -1, iIterLast = -1;
+    Gia_Man_t * pTemp   = Abc_FrameReadGia(Abc_FrameGetGlobalFrame());
+    Gia_Man_t * pNew    = Gia_ManDup( pTemp );
+    Abc_Random(1);
+    for ( s = 0; s < 10+Seed; s++ )
+        Abc_Random(0);
+    for ( i = 0; i < IterMax; i++ )
+    {
+        unsigned Rand = Abc_Random(0);
+        int fDch = Rand & 1;
+        //int fCom = (Rand >> 1) & 3;
+        int fCom = (Rand >> 1) & 1;
+        int fFx  = (Rand >> 2) & 1;
+        int KLut = fUseTwo ? 2 + (i % 5) : 3 + (i % 4);
+        int fChange = 0;
+        char Command[1000];
+        char * pComp = NULL;
+        if ( fCom == 3 )
+            pComp = "; &put; compress2rs; compress2rs; compress2rs; &get";
+        else if ( fCom == 2 )
+            pComp = "; &put; compress2rs; compress2rs; &get";
+        else if ( fCom == 1 )
+            pComp = "; &put; compress2rs; &get";
+        else if ( fCom == 0 )
+            pComp = "; &dc2";
+        sprintf( Command, "&dch%s; &if -a -K %d; &mfs -e -W 20 -L 20%s%s",
+            fDch ? " -f" : "", KLut, fFx ? "; &fx" : "", pComp );
+        if ( Cmd_CommandExecute(Abc_FrameGetGlobalFrame(), Command) )
+        {
+            Abc_Print( 1, "Something did not work out with the command \"%s\".\n", Command );
+            return NULL;
+        }
+        pTemp = Abc_FrameReadGia(Abc_FrameGetGlobalFrame());
+        if ( Gia_ManAndNum(pNew) > Gia_ManAndNum(pTemp) )
+        {
+            Gia_ManStop( pNew );
+            pNew = Gia_ManDup( pTemp );
+            fChange = 1;
+            iIterLast = i;
+        }
+        else if ( Gia_ManAndNum(pNew) + Gia_ManAndNum(pNew)/10 < Gia_ManAndNum(pTemp) ) 
+        {
+            //printf( "Updating\n" );
+            //Abc_FrameUpdateGia( Abc_FrameGetGlobalFrame(), Gia_ManDup(pNew) );
+        }
+        if ( fChange && fVerbose )
+        {
+            printf( "Iter %6d : ", i );
+            printf( "Time %8.2f sec : ", (float)1.0*(Abc_Clock() - clkStart)/CLOCKS_PER_SEC );
+            printf( "And = %6d  ", Gia_ManAndNum(pNew) );
+            printf( "Lev = %3d  ", Gia_ManLevelNum(pNew) );
+            if ( fChange ) 
+                printf( "<== best : " );
+            else if ( fVerbose )
+                printf( "           " );
+            printf( "%s", Command );
+            printf( "\n" );
+        }
+        if ( nTimeToStop && Abc_Clock() > nTimeToStop )
+        {
+            printf( "Runtime limit (%d sec) is reached after %d iterations.\n", TimeOut, i );
+            break;
+        }
+        if ( i - iIterLast > nNoImpr )
+        {
+            printf( "Completed %d iterations without improvement in %.2f seconds.\n", 
+                nNoImpr, (float)1.0*(Abc_Clock() - clkStart)/CLOCKS_PER_SEC );
+            break;
+        }
+    }
+    if ( i == IterMax )
+        printf( "Iteration limit (%d iters) is reached after %.2f seconds.\n", IterMax, (float)1.0*(Abc_Clock() - clkStart)/CLOCKS_PER_SEC );
+    else if ( nAnds && nAndsMin <= nAnds )
+        printf( "Quality goal (%d nodes <= %d nodes) is achieved after %d iterations and %.2f seconds.\n", 
+            nAndsMin, nAnds, i, (float)1.0*(Abc_Clock() - clkStart)/CLOCKS_PER_SEC );
+    return pNew;
+}
+Gia_Man_t * Gia_ManDeepSyn( Gia_Man_t * pGia, int nIters, int nNoImpr, int TimeOut, int nAnds, int Seed, int fUseTwo, int fVerbose )
 {
-    return NULL;
+    Gia_Man_t * pInit = Gia_ManDup(pGia);
+    Gia_Man_t * pBest = Gia_ManDup(pGia);
+    Gia_Man_t * pThis;
+    int i;
+    for ( i = 0; i < nIters; i++ )
+    {
+        Abc_FrameUpdateGia( Abc_FrameGetGlobalFrame(), Gia_ManDup(pInit) );
+        pThis = Gia_ManDeepSynOne( nNoImpr, TimeOut, nAnds, Seed+i, fUseTwo, fVerbose );
+        if ( Gia_ManAndNum(pBest) > Gia_ManAndNum(pThis) ) 
+        {
+            Gia_ManStop( pBest );
+            pBest = pThis;
+        }
+        else 
+            Gia_ManStop( pThis );
+        
+    }
+    Gia_ManStop( pInit );
+    return pBest;
 }
 
 ////////////////////////////////////////////////////////////////////////
diff --git a/src/aig/gia/giaSimBase.c b/src/aig/gia/giaSimBase.c
index efa4c187..f12cc83f 100644
--- a/src/aig/gia/giaSimBase.c
+++ b/src/aig/gia/giaSimBase.c
@@ -113,7 +113,13 @@ static inline void Gia_ManSimPatSimPo( Gia_Man_t * p, int i, Gia_Obj_t * pObj, i
     word * pSims0  = pSims + nWords*Gia_ObjFaninId0(pObj, i);
     word * pSims2  = pSims + nWords*i; int w;
     for ( w = 0; w < nWords; w++ )
-        pSims2[w] = (pSims0[w] ^ Diff0);
+        pSims2[w]  = (pSims0[w] ^ Diff0);
+}
+static inline void Gia_ManSimPatSimNot( Gia_Man_t * p, int i, Gia_Obj_t * pObj, int nWords, Vec_Wrd_t * vSims )
+{
+    word * pSims   = Vec_WrdArray(vSims) + nWords*i; int w;
+    for ( w = 0; w < nWords; w++ )
+        pSims[w]   = ~pSims[w];
 }
 Vec_Wrd_t * Gia_ManSimPatSim( Gia_Man_t * pGia )
 {
@@ -128,6 +134,20 @@ Vec_Wrd_t * Gia_ManSimPatSim( Gia_Man_t * pGia )
         Gia_ManSimPatSimPo( pGia, Gia_ObjId(pGia, pObj), pObj, nWords, vSims );
     return vSims;
 }
+void Gia_ManSimPatResim( Gia_Man_t * pGia, Vec_Int_t * vObjs, int nWords, Vec_Wrd_t * vSims )
+{
+    Gia_Obj_t * pObj; int i;
+    Gia_ManForEachObjVec( vObjs, pGia, pObj, i )
+        if ( i == 0 )
+            Gia_ManSimPatSimNot( pGia, Gia_ObjId(pGia, pObj), pObj, nWords, vSims );
+        else if ( Gia_ObjIsAnd(pObj) )
+            Gia_ManSimPatSimAnd( pGia, Gia_ObjId(pGia, pObj), pObj, nWords, vSims );
+        else if ( !Gia_ObjIsCo(pObj) ) assert(0);
+}
+void Gia_ManSimPatWrite( char * pFileName, Vec_Wrd_t * vSimsIn, int nWords )
+{
+    Vec_WrdDumpHex( pFileName, vSimsIn, nWords, 0 );
+}
 
 /**Function*************************************************************
 
diff --git a/src/base/abc/abcUtil.c b/src/base/abc/abcUtil.c
index 1f0c9725..922b34ae 100644
--- a/src/base/abc/abcUtil.c
+++ b/src/base/abc/abcUtil.c
@@ -3122,7 +3122,8 @@ Vec_Wec_t * Abc_SopSynthesize( Vec_Ptr_t * vSops )
     Abc_Obj_t * pObj, * pFanin;
     int i, k, iNode = 0;
     Abc_FrameReplaceCurrentNetwork( Abc_FrameReadGlobalFrame(), pNtk );
-    Cmd_CommandExecute( Abc_FrameGetGlobalFrame(), "fx; strash; balance; dc2; map -a" );
+    //Cmd_CommandExecute( Abc_FrameGetGlobalFrame(), "fx; strash; balance; dc2; map -a" );
+    Cmd_CommandExecute( Abc_FrameGetGlobalFrame(), "st; collapse; sop; fx; strash; &get; &ps; &deepsyn -I 4 -J 50 -T 5 -S 111 -t; &ps; &put; map -a" );
     pNtkNew = Abc_FrameReadNtk( Abc_FrameReadGlobalFrame() );
     vRes = Vec_WecStart( Abc_NtkPiNum(pNtkNew) + Abc_NtkNodeNum(pNtkNew) + Abc_NtkPoNum(pNtkNew) );
     Abc_NtkForEachPi( pNtkNew, pObj, i )
diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c
index 52bd1050..7b4db87a 100644
--- a/src/base/abci/abc.c
+++ b/src/base/abci/abc.c
@@ -7063,11 +7063,11 @@ usage:
 ***********************************************************************/
 int Abc_CommandRunEco( Abc_Frame_t * pAbc, int argc, char ** argv )
 {
-    extern void Acb_NtkRunEco( char * pFileNames[4], int fCheck, int fRandom, int fVerbose, int fVeryVerbose );
+    extern void Acb_NtkRunEco( char * pFileNames[4], int fCheck, int fRandom, int fInputs, int fVerbose, int fVeryVerbose );
     char * pFileNames[4] = {NULL};
-    int c, fCheck = 0, fRandom = 0, fVerbose = 0, fVeryVerbose = 0;
+    int c, fCheck = 0, fRandom = 0, fInputs = 0, fVerbose = 0, fVeryVerbose = 0;
     Extra_UtilGetoptReset();
-    while ( ( c = Extra_UtilGetopt( argc, argv, "crvwh" ) ) != EOF )
+    while ( ( c = Extra_UtilGetopt( argc, argv, "crivwh" ) ) != EOF )
     {
         switch ( c )
         {
@@ -7077,6 +7077,9 @@ int Abc_CommandRunEco( Abc_Frame_t * pAbc, int argc, char ** argv )
         case 'r':
             fRandom ^= 1;
             break;
+        case 'i':
+            fInputs ^= 1;
+            break;
         case 'v':
             fVerbose ^= 1;
             break;
@@ -7108,11 +7111,11 @@ int Abc_CommandRunEco( Abc_Frame_t * pAbc, int argc, char ** argv )
             fclose( pFile );
         pFileNames[c] = argv[globalUtilOptind+c];
     }
-    Acb_NtkRunEco( pFileNames, fCheck, fRandom, fVerbose, fVeryVerbose );
+    Acb_NtkRunEco( pFileNames, fCheck, fRandom, fInputs, fVerbose, fVeryVerbose );
     return 0;
 
 usage:
-    Abc_Print( -2, "usage: runeco [-crvwh] <implementation> <specification> <weights>\n" );
+    Abc_Print( -2, "usage: runeco [-crivwh] <implementation> <specification> <weights>\n" );
     Abc_Print( -2, "\t         performs computation of patch functions during ECO,\n" );
     Abc_Print( -2, "\t         as described in the following paper: A. Q. Dao et al\n" );
     Abc_Print( -2, "\t         \"Efficient computation of ECO patch functions\", Proc. DAC\'18\n" );
@@ -7122,6 +7125,7 @@ usage:
     Abc_Print( -2, "\t         \"runeco unit1/F.v unit1/G.v unit1/weight.txt; cec -n out.v unit1/G.v\")\n" );
     Abc_Print( -2, "\t-c     : toggle checking that the problem has a solution [default = %s]\n", fCheck? "yes": "no" );
     Abc_Print( -2, "\t-r     : toggle using random permutation of support variables [default = %s]\n", fRandom? "yes": "no" );
+    Abc_Print( -2, "\t-i     : toggle using primary inputs as support variables [default = %s]\n", fInputs? "yes": "no" );
     Abc_Print( -2, "\t-v     : toggle printing verbose information [default = %s]\n", fVerbose? "yes": "no" );
     Abc_Print( -2, "\t-w     : toggle printing more verbose information [default = %s]\n", fVeryVerbose? "yes": "no" );
     Abc_Print( -2, "\t-h     : print the command usage\n");
@@ -7190,11 +7194,11 @@ usage:
 ***********************************************************************/
 int Abc_CommandRunSim( Abc_Frame_t * pAbc, int argc, char ** argv )
 {
-    extern void Acb_NtkRunSim( char * pFileName[4], int nWords, int nBeam, int LevL, int LevU, int fOrder, int fFancy, int fUseBuf, int fRandom, int fUseWeights, int fVerbose, int fVeryVerbose );
+    extern void Acb_NtkRunSim( char * pFileName[4], int nWords, int nBeam, int LevL, int LevU, int fOrder, int fFancy, int fUseBuf, int fRandom, int fUseWeights, int fInputs, int fVerbose, int fVeryVerbose );
     char * pFileNames[4] = {NULL, NULL, "out.v", NULL};
-    int c, nWords = 8, nBeam = 4, LevL = -1, LevU = -1, fOrder = 0, fFancy = 0, fUseBuf = 0, fRandom = 0, fUseWeights = 0, fVerbose = 0, fVeryVerbose = 0;
+    int c, nWords = 8, nBeam = 4, LevL = -1, LevU = -1, fOrder = 0, fFancy = 0, fUseBuf = 0, fRandom = 0, fUseWeights = 0, fInputs = 0, fVerbose = 0, fVeryVerbose = 0;
     Extra_UtilGetoptReset();
-    while ( ( c = Extra_UtilGetopt( argc, argv, "WBLUofbruvwh" ) ) != EOF )
+    while ( ( c = Extra_UtilGetopt( argc, argv, "WBLUofbruivwh" ) ) != EOF )
     {
         switch ( c )
         {
@@ -7257,6 +7261,9 @@ int Abc_CommandRunSim( Abc_Frame_t * pAbc, int argc, char ** argv )
         case 'u':
             fUseWeights ^= 1;
             break;
+        case 'i':
+            fInputs ^= 1;
+            break;
         case 'v':
             fVerbose ^= 1;
             break;
@@ -7288,11 +7295,11 @@ int Abc_CommandRunSim( Abc_Frame_t * pAbc, int argc, char ** argv )
         else
             fclose( pFile );
     }
-    Acb_NtkRunSim( pFileNames, nWords, nBeam, LevL, LevU, fOrder, fFancy, fUseBuf, fRandom, fUseWeights, fVerbose, fVeryVerbose );
+    Acb_NtkRunSim( pFileNames, nWords, nBeam, LevL, LevU, fOrder, fFancy, fUseBuf, fRandom, fUseWeights, fInputs, fVerbose, fVeryVerbose );
     return 0;
 
 usage:
-    Abc_Print( -2, "usage: runsim [-WBLU] [-ofbruvwh] [-N <num>] <file1> <file2> <file3>\n" );
+    Abc_Print( -2, "usage: runsim [-WBLU] [-ofbruivwh] [-N <num>] <file1> <file2> <file3>\n" );
     Abc_Print( -2, "\t           experimental simulation command\n" );
     Abc_Print( -2, "\t-W <num> : the number of words of simulation info [default = %d]\n", nWords );
     Abc_Print( -2, "\t-B <num> : the beam width parameter [default = %d]\n", nBeam );
@@ -7303,6 +7310,7 @@ usage:
     Abc_Print( -2, "\t-b       : toggle using buffers [default = %s]\n",                   fUseBuf? "yes": "no" );
     Abc_Print( -2, "\t-r       : toggle using random permutation of support variables [default = %s]\n",      fRandom? "yes": "no" );
     Abc_Print( -2, "\t-u       : toggle using topological info to select support variables [default = %s]\n", fUseWeights? "yes": "no" );
+    Abc_Print( -2, "\t-i       : toggle using primary inputs as support variables [default = %s]\n",          fInputs? "yes": "no" );
     Abc_Print( -2, "\t-v       : toggle printing verbose information [default = %s]\n",                       fVerbose? "yes": "no" );
     Abc_Print( -2, "\t-w       : toggle printing more verbose information [default = %s]\n",                  fVeryVerbose? "yes": "no" );
     Abc_Print( -2, "\t-h       : print the command usage\n");
@@ -46327,13 +46335,35 @@ usage:
 ***********************************************************************/
 int Abc_CommandAbc9DeepSyn( Abc_Frame_t * pAbc, int argc, char ** argv )
 {
-    extern Gia_Man_t * Gia_ManDeepSyn( Gia_Man_t * pGia, int TimeOut, int nAnds, int Seed, int fVerbose );
-    Gia_Man_t * pTemp; int c, TimeOut = 0, nAnds = 0, Seed = 0, fVerbose = 0;
+    extern Gia_Man_t * Gia_ManDeepSyn( Gia_Man_t * pGia, int nIters, int nNoImpr, int TimeOut, int nAnds, int Seed, int fUseTwo, int fVerbose );
+    Gia_Man_t * pTemp; int c, nIters = 1, nNoImpr = ABC_INFINITY, TimeOut = 0, nAnds = 0, Seed = 0, fUseTwo = 0, fVerbose = 0;
     Extra_UtilGetoptReset();
-    while ( ( c = Extra_UtilGetopt( argc, argv, "TASvh" ) ) != EOF )
+    while ( ( c = Extra_UtilGetopt( argc, argv, "IJTAStvh" ) ) != EOF )
     {
         switch ( c )
         {
+        case 'I':
+            if ( globalUtilOptind >= argc )
+            {
+                Abc_Print( -1, "Command line switch \"-I\" should be followed by an integer.\n" );
+                goto usage;
+            }
+            nIters = atoi(argv[globalUtilOptind]);
+            globalUtilOptind++;
+            if ( nIters < 0 )
+                goto usage;
+            break;
+        case 'J':
+            if ( globalUtilOptind >= argc )
+            {
+                Abc_Print( -1, "Command line switch \"-J\" should be followed by an integer.\n" );
+                goto usage;
+            }
+            nNoImpr = atoi(argv[globalUtilOptind]);
+            globalUtilOptind++;
+            if ( nNoImpr < 0 )
+                goto usage;
+            break;
         case 'T':
             if ( globalUtilOptind >= argc )
             {
@@ -46367,6 +46397,9 @@ int Abc_CommandAbc9DeepSyn( Abc_Frame_t * pAbc, int argc, char ** argv )
             if ( Seed < 0 )
                 goto usage;
             break;
+        case 't':
+            fUseTwo ^= 1;
+            break;
         case 'v':
             fVerbose ^= 1;
             break;
@@ -46381,16 +46414,19 @@ int Abc_CommandAbc9DeepSyn( Abc_Frame_t * pAbc, int argc, char ** argv )
         Abc_Print( -1, "Abc_CommandAbc9DeepSyn(): There is no AIG.\n" );
         return 0;
     }
-    pTemp = Gia_ManDeepSyn( pAbc->pGia, TimeOut, nAnds, Seed, fVerbose );
+    pTemp = Gia_ManDeepSyn( pAbc->pGia, nIters, nNoImpr, TimeOut, nAnds, Seed, fUseTwo, fVerbose );
     Abc_FrameUpdateGia( pAbc, pTemp );
     return 0;
 
 usage:
-    Abc_Print( -2, "usage: &deepsyn [-TAS <num>] [-vh]\n" );
+    Abc_Print( -2, "usage: &deepsyn [-IJTAS <num>] [-tvh]\n" );
     Abc_Print( -2, "\t           performs synthesis\n" );
+    Abc_Print( -2, "\t-I <num> : the number of iterations [default = %d]\n",                   nIters  );
+    Abc_Print( -2, "\t-J <num> : the number of steps without improvements [default = %d]\n",   nNoImpr  );
     Abc_Print( -2, "\t-T <num> : the timeout in seconds (0 = no timeout) [default = %d]\n",    TimeOut );
     Abc_Print( -2, "\t-A <num> : the number of nodes to stop (0 = no limit) [default = %d]\n", nAnds   );
-    Abc_Print( -2, "\t-S <num> : user-specified random seed (0 <= num <= 100) [default = %d]\n", Seed   );
+    Abc_Print( -2, "\t-S <num> : user-specified random seed (0 <= num <= 100) [default = %d]\n", Seed  );
+    Abc_Print( -2, "\t-t       : toggle using two-input LUTs [default = %s]\n",                fUseTwo? "yes": "no" );
     Abc_Print( -2, "\t-v       : toggle printing optimization summary [default = %s]\n",       fVerbose? "yes": "no" );
     Abc_Print( -2, "\t-h       : print the command usage\n");
     return 1;
diff --git a/src/base/acb/acbFunc.c b/src/base/acb/acbFunc.c
index eced70e7..6d5bdaad 100644
--- a/src/base/acb/acbFunc.c
+++ b/src/base/acb/acbFunc.c
@@ -145,15 +145,28 @@ char * pLibStr[25] = {
     "GATE zero       0       O=CONST0;\n"
     "GATE one        0       O=CONST1;\n"
 };
-void Acb_IntallLibrary()
+char * pLibStr2[25] = {
+    "GATE buf        1       O=a;            PIN * INV 1 999 1.0 0.0 1.0 0.0\n"
+    "GATE inv        1       O=!a;           PIN * INV 1 999 1.0 0.0 1.0 0.0\n"
+    "GATE and2       1       O=a*b;          PIN * INV 1 999 1.0 0.0 1.0 0.0\n"
+    "GATE or2        1       O=a+b;          PIN * INV 1 999 1.0 0.0 1.0 0.0\n"
+    "GATE nand2      1       O=!(a*b);       PIN * INV 1 999 1.0 0.0 1.0 0.0\n"
+    "GATE nor2       1       O=!(a+b);       PIN * INV 1 999 1.0 0.0 1.0 0.0\n"
+    "GATE xor        1       O=!a*b+a*!b;    PIN * INV 1 999 1.0 0.0 1.0 0.0\n"
+    "GATE xnor       1       O=a*b+!a*!b;    PIN * INV 1 999 1.0 0.0 1.0 0.0\n"
+    "GATE zero       0       O=CONST0;\n"
+    "GATE one        0       O=CONST1;\n"
+};
+void Acb_IntallLibrary( int f2Ins )
 {
     extern Mio_Library_t * Mio_LibraryReadBuffer( char * pBuffer, int fExtendedFormat, st__table * tExcludeGate, int fVerbose );
     Mio_Library_t * pLib;
     int i;
     // create library string
     Vec_Str_t * vLibStr = Vec_StrAlloc( 1000 );
-    for ( i = 0; pLibStr[i]; i++ )
-        Vec_StrAppend( vLibStr, pLibStr[i] );
+    char ** ppLibStr = f2Ins ? pLibStr2 : pLibStr;
+    for ( i = 0; ppLibStr[i]; i++ )
+        Vec_StrAppend( vLibStr, ppLibStr[i] );
     Vec_StrPush( vLibStr, '\0' );
     // create library
     pLib = Mio_LibraryReadBuffer( Vec_StrArray(vLibStr), 0, NULL, 0 );
@@ -2600,7 +2613,7 @@ Vec_Ptr_t * Acb_TransformPatchFunctions( Vec_Ptr_t * vSops, Vec_Wec_t * vSupps,
   SeeAlso     []
 
 ***********************************************************************/
-int Acb_NtkEcoPerform( Acb_Ntk_t * pNtkF, Acb_Ntk_t * pNtkG, char * pFileName[4], int fCisOnly, int fCheck, int fVerbose, int fVeryVerbose )
+int Acb_NtkEcoPerform( Acb_Ntk_t * pNtkF, Acb_Ntk_t * pNtkG, char * pFileName[4], int fCisOnly, int fInputs, int fCheck, int fVerbose, int fVeryVerbose )
 {
     extern Gia_Man_t * Abc_SopSynthesizeOne( char * pSop, int fClp );
 
@@ -2615,7 +2628,7 @@ int Acb_NtkEcoPerform( Acb_Ntk_t * pNtkF, Acb_Ntk_t * pNtkG, char * pFileName[4]
     Vec_Int_t * vSuppF  = Acb_NtkFindSupp( pNtkF, vRoots );
     Vec_Int_t * vSuppG  = Acb_NtkFindSupp( pNtkG, vRoots );
     Vec_Int_t * vSupp   = Vec_IntTwoMerge( vSuppF, vSuppG );
-    Vec_Int_t * vDivs   = fCisOnly ? Acb_NtkFindDivsCis( pNtkF, vSupp ) : Acb_NtkFindDivs( pNtkF, vSupp, vBlock, fVerbose );
+    Vec_Int_t * vDivs   = (fCisOnly || fInputs) ? Acb_NtkFindDivsCis( pNtkF, vSupp ) : Acb_NtkFindDivs( pNtkF, vSupp, vBlock, fVerbose );
     Vec_Int_t * vNodesF = Acb_NtkFindNodes( pNtkF, vRoots, vDivs );
     Vec_Int_t * vNodesG = Acb_NtkFindNodes( pNtkG, vRoots, NULL );
 
@@ -2829,7 +2842,7 @@ void Acb_NtkTestRun2( char * pFileNames[3], int fVerbose )
     Acb_Ntk_t * pNtk = Acb_VerilogSimpleRead( pFileNames[0], pFileNames[2] );
     Acb_VerilogSimpleWrite( pNtk, pFileNameOut );
     Acb_ManFree( pNtk->pDesign );
-    Acb_IntallLibrary();
+    Acb_IntallLibrary( 0 );
 }
 
 /**Function*************************************************************
@@ -2843,7 +2856,7 @@ void Acb_NtkTestRun2( char * pFileNames[3], int fVerbose )
   SeeAlso     []
 
 ***********************************************************************/
-void Acb_NtkRunEco( char * pFileNames[4], int fCheck, int fRandom, int fVerbose, int fVeryVerbose )
+void Acb_NtkRunEco( char * pFileNames[4], int fCheck, int fRandom, int fInputs, int fVerbose, int fVeryVerbose )
 {
     char Command[1000]; int Result = 1;
     Acb_Ntk_t * pNtkF = Acb_VerilogSimpleRead( pFileNames[0], pFileNames[2] );
@@ -2863,12 +2876,12 @@ void Acb_NtkRunEco( char * pFileNames[4], int fCheck, int fRandom, int fVerbose,
     assert( Acb_NtkCiNum(pNtkF) == Acb_NtkCiNum(pNtkG) );
     assert( Acb_NtkCoNum(pNtkF) == Acb_NtkCoNum(pNtkG) );
 
-    Acb_IntallLibrary();
+    Acb_IntallLibrary( Abc_FrameReadSignalNames() != NULL );
 
-    if ( !Acb_NtkEcoPerform( pNtkF, pNtkG, pFileNames, 0, fCheck, fVerbose, fVeryVerbose ) )
+    if ( !Acb_NtkEcoPerform( pNtkF, pNtkG, pFileNames, 0, fInputs, fCheck, fVerbose, fVeryVerbose ) )
     {
 //        printf( "General computation timed out. Trying inputs only.\n\n" );
-//        if ( !Acb_NtkEcoPerform( pNtkF, pNtkG, pFileNames, 1, fCheck, fVerbose, fVeryVerbose ) )
+//        if ( !Acb_NtkEcoPerform( pNtkF, pNtkG, pFileNames, 1, fInputs, fCheck, fVerbose, fVeryVerbose ) )
 //            printf( "Input-only computation also timed out.\n\n" );
         printf( "Computation did not succeed.\n" );
         Result = 0;
diff --git a/src/base/acb/acbUtil.c b/src/base/acb/acbUtil.c
index d707d136..dab8239d 100644
--- a/src/base/acb/acbUtil.c
+++ b/src/base/acb/acbUtil.c
@@ -167,17 +167,35 @@ int Acb_NtkCountPoDrivers( Acb_Ntk_t * p, Vec_Int_t * vObjs )
   SeeAlso     []
 
 ***********************************************************************/
-int Acb_NtkNodeDeref_rec( Vec_Int_t * vRefs, Acb_Ntk_t * p, int iObj )
+int Acb_NtkNodeDeref_rec( Vec_Int_t * vRefs, Acb_Ntk_t * p, int iObj, int nGates[5] )
 {
     int i, Fanin, * pFanins, Counter = 1;
     if ( Acb_ObjIsCi(p, iObj) )
         return 0;
+    if ( nGates )
+    {
+        int nFan = Acb_ObjFaninNum(p, iObj);
+        int Type = Acb_ObjType( p, iObj );
+        if ( Type == ABC_OPER_CONST_F ) 
+            nGates[0]++;
+        else if ( Type == ABC_OPER_CONST_T ) 
+            nGates[1]++;
+        else if ( Type == ABC_OPER_BIT_BUF || Type == ABC_OPER_CO ) 
+            nGates[2]++;
+        else if ( Type == ABC_OPER_BIT_INV ) 
+            nGates[3]++;
+        else
+        {
+            assert( nFan >= 2 );
+            nGates[4] += Acb_ObjFaninNum(p, iObj)-1;
+        }
+    }
     Acb_ObjForEachFaninFast( p, iObj, pFanins, Fanin, i )
     {
         assert( Vec_IntEntry(vRefs, Fanin) > 0 );
         Vec_IntAddToEntry( vRefs, Fanin, -1 );
         if ( Vec_IntEntry(vRefs, Fanin) == 0 )
-            Counter += Acb_NtkNodeDeref_rec( vRefs, p, Fanin );
+            Counter += Acb_NtkNodeDeref_rec( vRefs, p, Fanin, nGates );
     }
     return Counter;
 }
@@ -220,10 +238,10 @@ int Acb_NtkFindMffcSize( Acb_Ntk_t * p, Vec_Int_t * vObjsRefed, Vec_Int_t * vObj
         Acb_ObjForEachFaninFast( p, iObj, pFanins, Fanin, i )
             Vec_IntAddToEntry( vRefs, Fanin, 1 );
     Vec_IntForEachEntry( vObjsRefed, iObj, i )
-        Acb_NtkNodeRef_rec( vRefs, p, iObj, NULL );
+        Vec_IntAddToEntry( vRefs, iObj, 1 );
     Vec_IntForEachEntry( vObjsDerefed, iObj, i )
-        if ( Vec_IntEntry(vRefs, iObj) == 0 )
-            Count2 += Acb_NtkNodeRef_rec( vRefs, p, iObj, nGates );
+        //if ( Vec_IntEntry(vRefs, iObj) != 0 || Acb_ObjIsCo(p, iObj) )
+            Count2 += Acb_NtkNodeDeref_rec( vRefs, p, iObj, nGates );
     Vec_IntFree( vRefs );
     return Count2;
 }
@@ -1133,7 +1151,7 @@ void Acb_Ntk4CollectRing( Acb_Ntk_t * pNtk, Vec_Int_t * vStart, Vec_Int_t * vRes
 }
 void Acb_Ntk4DumpWeightsInt( Acb_Ntk_t * pNtk, Vec_Int_t * vObjs, char * pFileName )
 {
-    int i, iObj;//, Weight;
+    int i, iObj, Count = 0;//, Weight;
     Vec_Int_t * vDists, * vStart, * vNexts;
     FILE * pFile = fopen( pFileName, "wb" );
     if ( pFile == NULL )
@@ -1165,15 +1183,30 @@ void Acb_Ntk4DumpWeightsInt( Acb_Ntk_t * pNtk, Vec_Int_t * vObjs, char * pFileNa
 //    Vec_IntForEachEntry( vDists, Weight, i )
 //        if ( Weight && Acb_ObjNameStr(pNtk, i)[0] != '1' )
 //            fprintf( pFile, "%s %d\n", Acb_ObjNameStr(pNtk, i), 10000+Weight );
+/*
+    // mark reachable
+    Vec_IntClear( &pNtk->vArray0 );
+    Acb_NtkIncTravId( pNtk );
+    Acb_NtkForEachCo( pNtk, iObj, i )
+        if ( !Vec_IntEntry(vStatus, i) )
+            Acb_ObjCollectTfi_rec( pNtk, iObj, 0 );
+*/
     Acb_NtkForEachObj( pNtk, iObj )
     {
         char * pName = Acb_ObjNameStr(pNtk, iObj);
         int Weight = Vec_IntEntry(vDists, iObj);
         if ( Weight == 0 )
             Weight = 10000;
+/*
+        if ( !Acb_ObjSetTravIdCur(pNtk, iObj) )
+        {
+            Count++;
+            continue;
+        }
+*/
         fprintf( pFile, "%s %d\n", pName, 100000+Weight );
     }
-
+    //printf( "Skipped %d nodes.\n", Count );
     Vec_IntFree( vDists );
     fclose( pFile );
 }
@@ -1205,13 +1238,13 @@ void Acb_Ntk4DumpWeights( char * pFileNameIn, Vec_Ptr_t * vObjNames, char * pFil
   SeeAlso     []
 
 ***********************************************************************/
-void Acb_NtkRunSim( char * pFileName[4], int nWords, int nBeam, int LevL, int LevU, int fOrder, int fFancy, int fUseBuf, int fRandom, int fUseWeights, int fVerbose, int fVeryVerbose )
+void Acb_NtkRunSim( char * pFileName[4], int nWords, int nBeam, int LevL, int LevU, int fOrder, int fFancy, int fUseBuf, int fRandom, int fUseWeights, int fInputs, int fVerbose, int fVeryVerbose )
 {
     extern int Gia_Sim4Try( char * pFileName0, char * pFileName1, char * pFileName2, int nWords, int nBeam, int LevL, int LevU, int fOrder, int fFancy, int fUseBuf, int fVerbose );
-    extern void Acb_NtkRunEco( char * pFileNames[4], int fCheck, int fRandom, int fVerbose, int fVeryVerbose );
+    extern void Acb_NtkRunEco( char * pFileNames[4], int fCheck, int fRandom, int fInputs, int fVerbose, int fVeryVerbose );
     char * pFileNames[4] = { pFileName[2], pFileName[1], fUseWeights ? (char *)"weights.txt" : NULL, pFileName[2] };
     if ( Gia_Sim4Try( pFileName[0], pFileName[1], pFileName[2], nWords, nBeam, LevL, LevU, fOrder, fFancy, fUseBuf, fVerbose ) )
-        Acb_NtkRunEco( pFileNames, 1, fRandom, fVerbose, fVeryVerbose );
+        Acb_NtkRunEco( pFileNames, 1, fRandom, fInputs, fVerbose, fVeryVerbose );
 } 
 
 
diff --git a/src/misc/vec/vecInt.h b/src/misc/vec/vecInt.h
index 01fb3175..5e545698 100644
--- a/src/misc/vec/vecInt.h
+++ b/src/misc/vec/vecInt.h
@@ -1279,6 +1279,26 @@ static inline int Vec_IntCountZero( Vec_Int_t * p )
 
 /**Function*************************************************************
 
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline int Vec_IntAddPositive( Vec_Int_t * p ) 
+{
+    int i, Counter = 0;
+    for ( i = 0; i < p->nSize; i++ )
+        if ( p->pArray[i] > 0 )
+            Counter += p->pArray[i];
+    return Counter;
+}
+
+/**Function*************************************************************
+
   Synopsis    [Checks if two vectors are equal.]
 
   Description []