Adding commands to save/load best network.

6 files changed, 342 insertions, 9 deletions

diff --git a/src/aig/gia/gia.h b/src/aig/gia/gia.h
index fa8a6026..0ac1c740 100644
--- a/src/aig/gia/gia.h
+++ b/src/aig/gia/gia.h
@@ -1067,6 +1067,7 @@ extern Gia_Man_t *         Gia_ManDupLastPis( Gia_Man_t * p, int nLastPis );
 extern Gia_Man_t *         Gia_ManDupFlip( Gia_Man_t * p, int * pInitState );
 extern Gia_Man_t *         Gia_ManDupCycled( Gia_Man_t * pAig, Abc_Cex_t * pCex, int nFrames );
 extern Gia_Man_t *         Gia_ManDup( Gia_Man_t * p );  
+extern Gia_Man_t *         Gia_ManDupWithAttributes( Gia_Man_t * p );  
 extern Gia_Man_t *         Gia_ManDupZero( Gia_Man_t * p );
 extern Gia_Man_t *         Gia_ManDupPerm( Gia_Man_t * p, Vec_Int_t * vPiPerm );
 extern Gia_Man_t *         Gia_ManDupPermFlop( Gia_Man_t * p, Vec_Int_t * vFfPerm );
@@ -1180,6 +1181,7 @@ extern int                 Gia_ManLutFaninCount( Gia_Man_t * p );
 extern int                 Gia_ManLutSizeMax( Gia_Man_t * p );
 extern int                 Gia_ManLutNum( Gia_Man_t * p );
 extern int                 Gia_ManLutLevel( Gia_Man_t * p );
+extern void                Gia_ManLutParams( Gia_Man_t * p, int * pnCurLuts, int * pnCurEdges, int * pnCurLevels );
 extern void                Gia_ManSetRefsMapped( Gia_Man_t * p );
 extern void                Gia_ManSetIfParsDefault( void * pIfPars );
 extern void                Gia_ManMappingVerify( Gia_Man_t * p );
@@ -1313,6 +1315,7 @@ extern Gia_Man_t *         Gia_ManDupNormalize( Gia_Man_t * p );
 extern Gia_Man_t *         Gia_ManDupUnnormalize( Gia_Man_t * p );
 extern Gia_Man_t *         Gia_ManDupCollapse( Gia_Man_t * p, Gia_Man_t * pBoxes, Vec_Int_t * vBoxPres );
 extern int                 Gia_ManLevelWithBoxes( Gia_Man_t * p );
+extern int                 Gia_ManLutLevelWithBoxes( Gia_Man_t * p );
 extern int                 Gia_ManVerifyWithBoxes( Gia_Man_t * pGia, void * pParsInit );
 extern void *              Gia_ManUpdateTimMan( Gia_Man_t * p, Vec_Int_t * vBoxPres );
 extern Gia_Man_t *         Gia_ManUpdateExtraAig( void * pTime, Gia_Man_t * pAig, Vec_Int_t * vBoxPres );
diff --git a/src/aig/gia/giaDup.c b/src/aig/gia/giaDup.c
index b54bdee0..37deb7fd 100644
--- a/src/aig/gia/giaDup.c
+++ b/src/aig/gia/giaDup.c
@@ -546,6 +546,19 @@ Gia_Man_t * Gia_ManDup( Gia_Man_t * p )
         pNew->pCexSeq = Abc_CexDup( p->pCexSeq, Gia_ManRegNum(p) );
     return pNew;
 }
+Gia_Man_t * Gia_ManDupWithAttributes( Gia_Man_t * p )
+{
+    Gia_Man_t * pNew = Gia_ManDup(p);
+    Gia_ManTransferMapping( pNew, p );
+    Gia_ManTransferPacking( pNew, p );
+    if ( p->pManTime )
+        pNew->pManTime = Tim_ManDup( (Tim_Man_t *)p->pManTime, 0 );
+    if ( p->pAigExtra )
+        pNew->pAigExtra = Gia_ManDup( p->pAigExtra );
+    if ( p->nAnd2Delay )
+        pNew->nAnd2Delay = p->nAnd2Delay;
+    return pNew;
+}
 
 /**Function*************************************************************
 
diff --git a/src/aig/gia/giaIf.c b/src/aig/gia/giaIf.c
index 6a2520eb..050966b1 100644
--- a/src/aig/gia/giaIf.c
+++ b/src/aig/gia/giaIf.c
@@ -183,6 +183,56 @@ int Gia_ManLutLevel( Gia_Man_t * p )
 
 /**Function*************************************************************
 
+  Synopsis    [Prints mapping statistics.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Gia_ManLutParams( Gia_Man_t * p, int * pnCurLuts, int * pnCurEdges, int * pnCurLevels )
+{
+    if ( p->pManTime && Tim_ManBoxNum((Tim_Man_t *)p->pManTime) )
+    {
+        int i;
+        *pnCurLuts = 0;
+        *pnCurEdges = 0;
+        Gia_ManForEachLut( p, i )
+        {
+            (*pnCurLuts)++;
+            (*pnCurEdges) += Gia_ObjLutSize(p, i);
+        }
+        *pnCurLevels = Gia_ManLutLevelWithBoxes( p );
+    }
+    else
+    {
+        Gia_Obj_t * pObj;
+        int i, k, iFan;
+        int * pLevels = ABC_CALLOC( int, Gia_ManObjNum(p) );
+        *pnCurLuts = 0;
+        *pnCurEdges = 0;
+        Gia_ManForEachLut( p, i )
+        {
+            int Level = 0;
+            (*pnCurLuts)++;
+            (*pnCurEdges) += Gia_ObjLutSize(p, i);
+            Gia_LutForEachFanin( p, i, iFan, k )
+                if ( Level < pLevels[iFan] )
+                    Level = pLevels[iFan];
+            pLevels[i] = Level + 1;
+        }
+        *pnCurLevels = 0;
+        Gia_ManForEachCo( p, pObj, k )
+            if ( *pnCurLevels < pLevels[Gia_ObjFaninId0p(p, pObj)] )
+                *pnCurLevels = pLevels[Gia_ObjFaninId0p(p, pObj)];
+        ABC_FREE( pLevels );
+    }
+}
+
+/**Function*************************************************************
+
   Synopsis    [Assigns levels.]
 
   Description []
@@ -395,7 +445,9 @@ void Gia_ManPrintMappingStats( Gia_Man_t * p, char * pDumpFile )
     Abc_Print( 1, "lev =%5d ",   LevelMax );
     Abc_Print( 1, "(%.2f)  ",    (float)Ave / Gia_ManCoNum(p) );
     SetConsoleTextAttribute( hConsole, 7 );  // normal
-    Abc_Print( 1, "over =%5.1f %%  ", 100.0 * Gia_ManComputeOverlap(p) / Gia_ManAndNum(p) );
+//    Abc_Print( 1, "over =%5.1f %%  ", 100.0 * Gia_ManComputeOverlap(p) / Gia_ManAndNum(p) );
+    if ( p->pManTime && Tim_ManBoxNum((Tim_Man_t *)p->pManTime) )
+        Abc_Print( 1, "levB =%5d  ", Gia_ManLutLevelWithBoxes(p) );
     Abc_Print( 1, "mem =%5.2f MB", 4.0*(Gia_ManObjNum(p) + 2*nLuts + nFanins)/(1<<20) );
     Abc_Print( 1, "\n" );
     }
@@ -405,7 +457,9 @@ void Gia_ManPrintMappingStats( Gia_Man_t * p, char * pDumpFile )
     Abc_Print( 1, "%sedge =%8d%s  ", "\033[1;32m", nFanins,  "\033[0m" );  // green
     Abc_Print( 1, "%slev =%5d%s ",   "\033[1;31m", LevelMax, "\033[0m" );  // red
     Abc_Print( 1, "%s(%.2f)%s  ",    "\033[1;31m", (float)Ave / Gia_ManCoNum(p), "\033[0m" );
-    Abc_Print( 1, "over =%5.1f %%  ", 100.0 * Gia_ManComputeOverlap(p) / Gia_ManAndNum(p) );
+//    Abc_Print( 1, "over =%5.1f %%  ", 100.0 * Gia_ManComputeOverlap(p) / Gia_ManAndNum(p) );
+    if ( p->pManTime && Tim_ManBoxNum((Tim_Man_t *)p->pManTime) )
+        Abc_Print( 1, "levB =%5d  ", Gia_ManLutLevelWithBoxes(p) );
     Abc_Print( 1, "mem =%5.2f MB", 4.0*(Gia_ManObjNum(p) + 2*nLuts + nFanins)/(1<<20) );
     Abc_Print( 1, "\n" );
 #endif
diff --git a/src/aig/gia/giaTim.c b/src/aig/gia/giaTim.c
index 0e6a9252..290cae7d 100644
--- a/src/aig/gia/giaTim.c
+++ b/src/aig/gia/giaTim.c
@@ -486,6 +486,110 @@ int Gia_ManLevelWithBoxes( Gia_Man_t * p )
 
 /**Function*************************************************************
 
+  Synopsis    [Computes level with boxes.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Gia_ManLutLevelWithBoxes_rec( Gia_Man_t * p, Gia_Obj_t * pObj )
+{
+    int iObj, k, iFan, Level = 0;
+    if ( Gia_ObjIsTravIdCurrent(p, pObj) )
+        return 0;
+    Gia_ObjSetTravIdCurrent(p, pObj);
+    if ( Gia_ObjIsCi(pObj) )
+        return 1;
+    assert( Gia_ObjIsAnd(pObj) );
+    iObj = Gia_ObjId( p, pObj );
+    Gia_LutForEachFanin( p, iObj, iFan, k )
+    {
+        if ( Gia_ManLutLevelWithBoxes_rec( p, Gia_ManObj(p, iFan) ) )
+            return 1;
+        Level = Abc_MaxInt( Level, Gia_ObjLevelId(p, iFan) );
+    }
+    Gia_ObjSetLevelId( p, iObj, Level + 1 );
+    return 0;
+}
+int Gia_ManLutLevelWithBoxes( Gia_Man_t * p )
+{
+//    int nAnd2Delay = p->nAnd2Delay ? p->nAnd2Delay : 1;
+    Tim_Man_t * pManTime = (Tim_Man_t *)p->pManTime;
+    Gia_Obj_t * pObj, * pObjIn;
+    int i, k, j, curCi, curCo, LevelMax;
+    assert( Gia_ManRegNum(p) == 0 );
+    // copy const and real PIs
+    Gia_ManCleanLevels( p, Gia_ManObjNum(p) );
+    Gia_ObjSetLevel( p, Gia_ManConst0(p), 0 );
+    Gia_ManIncrementTravId( p );
+    Gia_ObjSetTravIdCurrent( p, Gia_ManConst0(p) );
+    for ( i = 0; i < Tim_ManPiNum(pManTime); i++ )
+    {
+        pObj = Gia_ManPi( p, i );
+//        Gia_ObjSetLevel( p, pObj, Tim_ManGetCiArrival(pManTime, i) / nAnd2Delay );
+        Gia_ObjSetLevel( p, pObj, 0 );
+        Gia_ObjSetTravIdCurrent( p, pObj );
+    }
+    // create logic for each box
+    curCi = Tim_ManPiNum(pManTime);
+    curCo = 0;
+    for ( i = 0; i < Tim_ManBoxNum(pManTime); i++ )
+    {
+        int nBoxInputs  = Tim_ManBoxInputNum( pManTime, i );
+        int nBoxOutputs = Tim_ManBoxOutputNum( pManTime, i );
+        float * pDelayTable = Tim_ManBoxDelayTable( pManTime, i );
+        // compute level for TFI of box inputs
+        for ( k = 0; k < nBoxInputs; k++ )
+        {
+            pObj = Gia_ManPo( p, curCo + k );
+            if ( Gia_ManLutLevelWithBoxes_rec( p, Gia_ObjFanin0(pObj) ) )
+            {
+                printf( "Boxes are not in a topological order. Switching to level computation without boxes.\n" );
+                return Gia_ManLevelNum( p );
+            }
+            // set box input level
+            Gia_ObjSetCoLevel( p, pObj );
+        }
+        // compute level for box outputs
+        for ( k = 0; k < nBoxOutputs; k++ )
+        {
+            pObj = Gia_ManPi( p, curCi + k );
+            Gia_ObjSetTravIdCurrent( p, pObj );
+            // evaluate delay of this output
+            LevelMax = 0;
+            assert( nBoxInputs == (int)pDelayTable[1] );
+            for ( j = 0; j < nBoxInputs && (pObjIn = Gia_ManPo(p, curCo + j)); j++ )
+                if ( (int)pDelayTable[3+k*nBoxInputs+j] != -ABC_INFINITY )
+//                    LevelMax = Abc_MaxInt( LevelMax, Gia_ObjLevel(p, pObjIn) + ((int)pDelayTable[3+k*nBoxInputs+j] / nAnd2Delay) );
+                    LevelMax = Abc_MaxInt( LevelMax, Gia_ObjLevel(p, pObjIn) + 1 );
+            // set box output level
+            Gia_ObjSetLevel( p, pObj, LevelMax );
+        }
+        curCo += nBoxInputs;
+        curCi += nBoxOutputs;
+    }
+    // add remaining nodes
+    p->nLevels = 0;
+    for ( i = Tim_ManCoNum(pManTime) - Tim_ManPoNum(pManTime); i < Tim_ManCoNum(pManTime); i++ )
+    {
+        pObj = Gia_ManPo( p, i );
+        Gia_ManLutLevelWithBoxes_rec( p, Gia_ObjFanin0(pObj) );
+        Gia_ObjSetCoLevel( p, pObj );
+        p->nLevels = Abc_MaxInt( p->nLevels, Gia_ObjLevel(p, pObj) );
+    }
+    curCo += Tim_ManPoNum(pManTime);
+    // verify counts
+    assert( curCi == Gia_ManPiNum(p) );
+    assert( curCo == Gia_ManPoNum(p) );
+//    printf( "Max level is %d.\n", p->nLevels );
+    return p->nLevels;
+}
+
+/**Function*************************************************************
+
   Synopsis    [Verify XAIG against its spec.]
 
   Description []
diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c
index 51d1e878..019f7011 100644
--- a/src/base/abci/abc.c
+++ b/src/base/abci/abc.c
@@ -318,6 +318,8 @@ static int Abc_CommandTraceCheck             ( Abc_Frame_t * pAbc, int argc, cha
 
 static int Abc_CommandAbc9Get                ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandAbc9Put                ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandAbc9Save               ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandAbc9Load               ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandAbc9Read               ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandAbc9ReadBlif           ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandAbc9ReadCBlif          ( Abc_Frame_t * pAbc, int argc, char ** argv );
@@ -903,6 +905,8 @@ void Abc_Init( Abc_Frame_t * pAbc )
 
     Cmd_CommandAdd( pAbc, "ABC9",         "&get",          Abc_CommandAbc9Get,          0 );
     Cmd_CommandAdd( pAbc, "ABC9",         "&put",          Abc_CommandAbc9Put,          0 );
+    Cmd_CommandAdd( pAbc, "ABC9",         "&save",         Abc_CommandAbc9Save,         0 );
+    Cmd_CommandAdd( pAbc, "ABC9",         "&load",         Abc_CommandAbc9Load,         0 );
     Cmd_CommandAdd( pAbc, "ABC9",         "&r",            Abc_CommandAbc9Read,         0 );
     Cmd_CommandAdd( pAbc, "ABC9",         "&read_blif",    Abc_CommandAbc9ReadBlif,     0 );
     Cmd_CommandAdd( pAbc, "ABC9",         "&read_cblif",   Abc_CommandAbc9ReadCBlif,    0 );
@@ -1091,6 +1095,8 @@ void Abc_End( Abc_Frame_t * pAbc )
         Gia_ManStop( Abc_FrameGetGlobalFrame()->pGia );
     if ( Abc_FrameGetGlobalFrame()->pGia2 )
         Gia_ManStop( Abc_FrameGetGlobalFrame()->pGia2 );
+    if ( Abc_FrameGetGlobalFrame()->pGiaBest )
+        Gia_ManStop( Abc_FrameGetGlobalFrame()->pGiaBest );
     if ( Abc_NtkRecIsRunning3() )
         Abc_NtkRecStop3();
 }
@@ -25420,6 +25426,129 @@ usage:
 
 /**Function*************************************************************
 
+  Synopsis    [Compares to versions of the design and finds the best.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline int Gia_ManCompareWithBest( Gia_Man_t * pBest, Gia_Man_t * p, int * pnBestLuts, int * pnBestEdges, int * pnBestLevels )
+{
+    int nCurLuts, nCurEdges, nCurLevels;
+    Gia_ManLutParams( p, &nCurLuts, &nCurEdges, &nCurLevels );
+    if ( pBest == NULL ||
+         Gia_ManPiNum(pBest) != Gia_ManPiNum(p) || 
+         Gia_ManPoNum(pBest) != Gia_ManPoNum(p) || 
+         Gia_ManRegNum(pBest) != Gia_ManRegNum(p) ||
+         strcmp(Gia_ManName(pBest), Gia_ManName(p)) ||
+        (*pnBestLevels > nCurLevels) ||
+        (*pnBestLevels == nCurLevels && *pnBestLuts > nCurLuts) ||
+        (*pnBestLevels == nCurLevels && *pnBestLuts == nCurLuts && *pnBestEdges > nCurEdges) )
+    {
+        *pnBestLuts = nCurLuts;
+        *pnBestEdges = nCurEdges;
+        *pnBestLevels = nCurLevels;
+        return 1;
+    }
+    return 0;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Abc_CommandAbc9Save( Abc_Frame_t * pAbc, int argc, char ** argv )
+{
+    int c;
+    Extra_UtilGetoptReset();
+    while ( ( c = Extra_UtilGetopt( argc, argv, "h" ) ) != EOF )
+    {
+        switch ( c )
+        {
+        case 'h':
+            goto usage;
+        default:
+            goto usage;
+        }
+    }
+    if ( pAbc->pGia == NULL )
+    {
+        Abc_Print( -1, "Empty network.\n" );
+        return 1;
+    }
+    if ( !Gia_ManHasMapping(pAbc->pGia) )
+    {
+        Abc_Print( -1, "GIA has not mapping.\n" );
+        return 1;
+    }
+    if ( !Gia_ManCompareWithBest( pAbc->pGiaBest, pAbc->pGia, &pAbc->nBestLuts, &pAbc->nBestEdges, &pAbc->nBestLevels ) )
+        return 0;
+    // save the design as best
+    Gia_ManStopP( &pAbc->pGiaBest );
+    pAbc->pGiaBest = Gia_ManDupWithAttributes( pAbc->pGia );
+    return 0; 
+
+usage:
+    Abc_Print( -2, "usage: &save [-h]\n" );
+    Abc_Print( -2, "\t        compares and possibly saves AIG with mapping\n" );
+    Abc_Print( -2, "\t-h    : print the command usage\n");
+    return 1;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Abc_CommandAbc9Load( Abc_Frame_t * pAbc, int argc, char ** argv )
+{
+    int c;
+    Extra_UtilGetoptReset();
+    while ( ( c = Extra_UtilGetopt( argc, argv, "h" ) ) != EOF )
+    {
+        switch ( c )
+        {
+        case 'h':
+            goto usage;
+        default:
+            goto usage;
+        }
+    }
+    // restore from best
+    if ( pAbc->pGiaBest == NULL )
+    {
+        Abc_Print( -1, "Abc_CommandAbc9Load(): There is no best design saved.\n" );
+        return 1;
+    }
+    Gia_ManStopP( &pAbc->pGia );
+    pAbc->pGia = Gia_ManDupWithAttributes( pAbc->pGiaBest );
+    return 0;
+
+usage:
+    Abc_Print( -2, "usage: &load [-h]\n" );
+    Abc_Print( -2, "\t        loads previously saved AIG with mapping" );
+    Abc_Print( -2, "\t-h    : print the command usage\n");
+    return 1;
+}
+
+/**Function*************************************************************
+
   Synopsis    []
 
   Description []
@@ -25507,10 +25636,10 @@ usage:
 int Abc_CommandAbc9Ps( Abc_Frame_t * pAbc, int argc, char ** argv )
 {
     Gps_Par_t Pars, * pPars = &Pars;
-    int c;
+    int c, fBest = 0;
     memset( pPars, 0, sizeof(Gps_Par_t) );
     Extra_UtilGetoptReset();
-    while ( ( c = Extra_UtilGetopt( argc, argv, "Dtpcnlmash" ) ) != EOF )
+    while ( ( c = Extra_UtilGetopt( argc, argv, "Dtpcnlmasbh" ) ) != EOF )
     {
         switch ( c )
         {
@@ -25547,22 +25676,37 @@ int Abc_CommandAbc9Ps( Abc_Frame_t * pAbc, int argc, char ** argv )
             pPars->pDumpFile = argv[globalUtilOptind];
             globalUtilOptind++;
             break;
+        case 'b':
+            fBest ^= 1;
+            break;
         case 'h':
             goto usage;
         default:
             goto usage;
         }
     }
-    if ( pAbc->pGia == NULL )
+    if ( fBest )
     {
-        Abc_Print( -1, "Abc_CommandAbc9Ps(): There is no AIG.\n" );
-        return 1;
+        if ( pAbc->pGiaBest == NULL )
+        {
+            Abc_Print( -1, "Abc_CommandAbc9Ps(): There is no AIG.\n" );
+            return 1;
+        }
+        Gia_ManPrintStats( pAbc->pGiaBest, pPars );
+    }
+    else
+    {
+        if ( pAbc->pGia == NULL )
+        {
+            Abc_Print( -1, "Abc_CommandAbc9Ps(): There is no AIG.\n" );
+            return 1;
+        }
+        Gia_ManPrintStats( pAbc->pGia, pPars );
     }
-    Gia_ManPrintStats( pAbc->pGia, pPars );
     return 0;
 
 usage:
-    Abc_Print( -2, "usage: &ps [-tpcnlmash] [-D file]\n" );
+    Abc_Print( -2, "usage: &ps [-tpcnlmasbh] [-D file]\n" );
     Abc_Print( -2, "\t          prints stats of the current AIG\n" );
     Abc_Print( -2, "\t-t      : toggle printing BMC tents [default = %s]\n",                pPars->fTents? "yes": "no" );
     Abc_Print( -2, "\t-p      : toggle printing switching activity [default = %s]\n",       pPars->fSwitch? "yes": "no" );
@@ -25572,6 +25716,7 @@ usage:
     Abc_Print( -2, "\t-m      : toggle printing MUX/XOR statistics [default = %s]\n",       pPars->fMuxXor? "yes": "no" );
     Abc_Print( -2, "\t-a      : toggle printing miter statistics [default = %s]\n",         pPars->fMiter? "yes": "no" );
     Abc_Print( -2, "\t-s      : skip mapping statistics even if mapped [default = %s]\n",   pPars->fSkipMap? "yes": "no" );
+    Abc_Print( -2, "\t-b      : toggle printing saved AIG statistics [default = %s]\n",     fBest? "yes": "no" );
     Abc_Print( -2, "\t-D file : file name to dump statistics [default = none]\n" );
     Abc_Print( -2, "\t-h      : print the command usage\n");
     return 1;
@@ -30646,6 +30791,11 @@ int Abc_CommandAbc9If( Abc_Frame_t * pAbc, int argc, char ** argv )
         Abc_Print( -1, "Empty GIA network.\n" );
         return 1;
     }
+    if ( Gia_ManHasMapping(pAbc->pGia) )
+    {
+        Abc_Print( -1, "Current AIG has mapping. Run \"&st\".\n" );
+        return 1;
+    }
 
     if ( pPars->nLutSize == -1 )
     {
@@ -31650,6 +31800,11 @@ int Abc_CommandAbc9Lf( Abc_Frame_t * pAbc, int argc, char ** argv )
         Abc_Print( -1, "Empty GIA network.\n" );
         return 1;
     }
+    if ( Gia_ManHasMapping(pAbc->pGia) )
+    {
+        Abc_Print( -1, "Current AIG has mapping. Run \"&st\".\n" );
+        return 1;
+    }
     if ( pPars->nLutSizeMux && pPars->fUseMux7 )
     {
         Abc_Print( -1, "Flags \"-M\" and \"-u\" are incompatible.\n" );
diff --git a/src/base/main/mainInt.h b/src/base/main/mainInt.h
index 73844c2b..c8276eeb 100644
--- a/src/base/main/mainInt.h
+++ b/src/base/main/mainInt.h
@@ -103,6 +103,10 @@ struct Abc_Frame_t_
     // new code
     Gia_Man_t *     pGia;          // alternative current network as a light-weight AIG
     Gia_Man_t *     pGia2;         // copy of the above
+    Gia_Man_t *     pGiaBest;      // copy of the above
+    int             nBestLuts;     // best LUT count
+    int             nBestEdges;    // best edge count
+    int             nBestLevels;   // best level count
     Abc_Cex_t *     pCex;          // a counter-example to fail the current network
     Abc_Cex_t *     pCex2;         // copy of the above
     Vec_Ptr_t *     vCexVec;       // a vector of counter-examples if more than one PO fails