User-controlable SAT sweeper.

4 files changed, 161 insertions, 122 deletions

diff --git a/src/aig/gia/gia.h b/src/aig/gia/gia.h
index 946b80c5..6ba68a55 100644
--- a/src/aig/gia/gia.h
+++ b/src/aig/gia/gia.h
@@ -1010,8 +1010,8 @@ extern Vec_Int_t *         Gia_SweeperCondVector( Gia_Man_t * p );
 extern int                 Gia_SweeperCondCheckUnsat( Gia_Man_t * p );
 extern int                 Gia_SweeperCheckEquiv( Gia_Man_t * p, int ProbeId1, int ProbeId2 );
 extern Gia_Man_t *         Gia_SweeperExtractUserLogic( Gia_Man_t * p, Vec_Int_t * vProbeIds, Vec_Ptr_t * vInNames, Vec_Ptr_t * vOutNames );
-extern Vec_Int_t *         Gia_SweeperGraft( Gia_Man_t * pDst, Vec_Int_t * vProbes, Gia_Man_t * pSrc );
 extern Gia_Man_t *         Gia_SweeperCleanup( Gia_Man_t * p, char * pCommLime );
+extern Vec_Int_t *         Gia_SweeperGraft( Gia_Man_t * pDst, Vec_Int_t * vProbes, Gia_Man_t * pSrc );
 extern Vec_Int_t *         Gia_SweeperFraig( Gia_Man_t * p, Vec_Int_t * vProbeIds, char * pCommLime );
 /*=== giaSwitch.c ============================================================*/
 extern float               Gia_ManEvaluateSwitching( Gia_Man_t * p );
diff --git a/src/aig/gia/giaSweeper.c b/src/aig/gia/giaSweeper.c
index 64fd990f..844c3e45 100644
--- a/src/aig/gia/giaSweeper.c
+++ b/src/aig/gia/giaSweeper.c
@@ -19,6 +19,7 @@
 ***********************************************************************/
 
 #include "gia.h"
+#include "base/main/main.h"
 #include "sat/bsat/satSolver.h"
 
 ABC_NAMESPACE_IMPL_START
@@ -407,6 +408,92 @@ Gia_Man_t * Gia_SweeperExtractUserLogic( Gia_Man_t * p, Vec_Int_t * vProbeIds, V
     return pNew;
 }
 
+/**Function*************************************************************
+
+  Synopsis    [Sweeper cleanup.]
+
+  Description [Returns new GIA with sweeper defined, which is the same
+  as the original sweeper, with all the dangling logic removed and SAT 
+  solver restarted. The probe IDs are guaranteed to have the same logic
+  functions as in the original manager.]
+               
+  SideEffects [The input manager is deleted inside this procedure.]
+
+  SeeAlso     []
+
+***********************************************************************/
+Gia_Man_t * Gia_SweeperCleanup( Gia_Man_t * p, char * pCommLime )
+{
+    Swp_Man_t * pSwp = (Swp_Man_t *)p->pData;
+    Vec_Int_t * vObjIds;
+    Gia_Man_t * pNew, * pTemp;
+    Gia_Obj_t * pObj;
+    int i, iLit, ProbeId;
+
+    // collect all internal nodes pointed to by currently-used probes
+    Gia_ManIncrementTravId( p );
+    vObjIds = Vec_IntAlloc( 1000 );
+    Vec_IntForEachEntry( pSwp->vProbes, iLit, ProbeId )
+    {
+        if ( iLit < 0 ) continue;
+        pObj = Gia_Lit2Obj( p, iLit );
+        Gia_ManExtract_rec( p, Gia_Regular(pObj), vObjIds );
+    }
+    // create new manager
+    pNew = Gia_ManStart( 1 + Gia_ManPiNum(p) + Vec_IntSize(vObjIds) + 100 );
+    pNew->pName = Abc_UtilStrsav( p->pName );
+    pNew->pSpec = Abc_UtilStrsav( p->pSpec );
+    Gia_ManConst0(p)->Value = 0;
+    Gia_ManForEachPi( p, pObj, i )
+        pObj->Value = Gia_ManAppendCi(pNew);
+    // create internal nodes
+    Gia_ManHashStart( pNew );
+    Gia_ManForEachObjVec( vObjIds, p, pObj, i )
+        pObj->Value = Gia_ManHashAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) );
+    Gia_ManHashStop( pNew );
+    // create outputs
+    Vec_IntFill( pSwp->vLit2Prob, 2*Gia_ManObjNum(pNew), -1 );
+    Vec_IntForEachEntry( pSwp->vProbes, iLit, ProbeId )
+    {
+        if ( iLit < 0 ) continue;
+        pObj = Gia_Lit2Obj( p, iLit );
+        iLit = Gia_Regular(pObj)->Value ^ Gia_IsComplement(pObj);
+        Vec_IntWriteEntry( pSwp->vProbes, ProbeId, iLit );
+        Vec_IntSetEntryFull( pSwp->vLit2Prob, iLit, ProbeId ); // consider hash table in the future
+    }
+    Vec_IntFree( vObjIds );
+    // duplicated if needed
+    if ( Gia_ManHasDangling(pNew) )
+    {
+        pNew = Gia_ManCleanup( pTemp = pNew );
+        Gia_ManStop( pTemp );
+    }
+    // execute command line
+    if ( pCommLime )
+    {
+        // set pNew to be current GIA in ABC
+        Abc_FrameUpdateGia( Abc_FrameGetGlobalFrame(), pNew );
+        // execute command line pCommLine using Abc_CmdCommandExecute()
+        Cmd_CommandExecute( Abc_FrameGetGlobalFrame(), pCommLime );
+        // get pNew to be current GIA in ABC     
+        pNew = Abc_FrameGetGia( Abc_FrameGetGlobalFrame() );
+    }
+    // restart the SAT solver
+    Vec_IntClear( pSwp->vId2Lit );
+    sat_solver_delete( pSwp->pSat );
+    pSwp->pSat         = sat_solver_new();
+    pSwp->nSatVars     = 1;
+    sat_solver_setnvars( pSwp->pSat, 1000 );
+    Swp_ManSetObj2Lit( pSwp, 0, (iLit = Abc_Var2Lit(pSwp->nSatVars++, 0)) );
+    iLit = Abc_LitNot(iLit);
+    sat_solver_addclause( pSwp->pSat, &iLit, &iLit + 1 );
+    pSwp->timeStart    = clock();
+    // return the result
+    pNew = p->pData; p->pData = NULL;
+    Gia_ManStop( p );
+    return pNew;
+}
+
 
 /**Function*************************************************************
 
@@ -1009,9 +1096,12 @@ Vec_Int_t * Gia_SweeperFraig( Gia_Man_t * p, Vec_Int_t * vProbeIds, char * pComm
     // execute command line
     if ( pCommLime )
     {
-    // set pNew to be current GIA in ABC
-    // execute command line pCommLine using Abc_CmdCommandExecute()
-    // get pNew to be current GIA in ABC     
+        // set pNew to be current GIA in ABC
+        Abc_FrameUpdateGia( Abc_FrameGetGlobalFrame(), pNew );
+        // execute command line pCommLine using Abc_CmdCommandExecute()
+        Cmd_CommandExecute( Abc_FrameGetGlobalFrame(), pCommLime );
+        // get pNew to be current GIA in ABC     
+        pNew = Abc_FrameGetGia( Abc_FrameGetGlobalFrame() );
     }
     vLits = Gia_SweeperGraft( p, NULL, pNew );
     Gia_ManStop( pNew );
@@ -1100,81 +1190,6 @@ Gia_Man_t * Gia_SweeperFraigTest( Gia_Man_t * p, int nWords, int nConfs, int fVe
     return pGia;
 }
 
-/**Function*************************************************************
-
-  Synopsis    [Sweeper cleanup.]
-
-  Description [Returns new GIA with sweeper defined, which is the same
-  as the original sweeper, with all the dangling logic removed and SAT 
-  solver restarted. The probe IDs are guaranteed to have the same logic
-  functions as in the original manager.]
-               
-  SideEffects [The input manager is deleted inside this procedure.]
-
-  SeeAlso     []
-
-***********************************************************************/
-#if 0
-Gia_Man_t * Gia_SweeperCleanup( Gia_Man_t * p, char * pCommLime )
-{
-    Vec_Int_t * vObjIds;
-    Gia_Man_t * pNew, * pTemp;
-    Gia_Obj_t * pObj;
-    int i, ProbeId;
-
-    // collect all internal nodes pointed to by used probes
-    Gia_ManIncrementTravId( p );
-    vObjIds = Vec_IntAlloc( 1000 );
-    Vec_IntForEachEntry( p->vProbes, ProbeId, i )
-    {
-        if ( ProbeId < 0 ) continue;
-        pObj = Gia_Lit2Obj( p, Gia_SweeperProbeLit(p, ProbeId) );
-        Gia_ManExtract_rec( p, Gia_Regular(pObj), vObjIds );
-    }
-    // create new manager
-    pNew = Gia_ManStart( 1 + Gia_ManPiNum(p) + Vec_IntSize(vObjIds) + 100 );
-    pNew->pName = Abc_UtilStrsav( p->pName );
-    pNew->pSpec = Abc_UtilStrsav( p->pSpec );
-    Gia_ManConst0(p)->Value = 0;
-    Gia_ManForEachPi( p, pObj, i )
-        pObj->Value = Gia_ManAppendCi(pNew);
-    // create internal nodes
-    Gia_ManHashStart( pNew );
-    Gia_ManForEachObjVec( vObjIds, p, pObj, i )
-        pObj->Value = Gia_ManHashAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) );
-    Gia_ManHashStop( pNew );
-    // create outputs
-    Vec_IntForEachEntry( p->vProbes, ProbeId, i )
-    {
-
-    Vec_IntPush( pSwp->vProbes, iLit );
-    Vec_IntPush( pSwp->vProbRefs, 1 );
-    Vec_IntSetEntryFull( pSwp->vLit2Prob, iLit, ProbeId ); // consider hash table in the future
-
-
-
-        pObj = Gia_Lit2Obj( p, Gia_SweeperProbeLit(p, ProbeId) );
-        Gia_ManAppendCo( pNew, Gia_Regular(pObj)->Value ^ Gia_IsComplement(pObj) );
-    }
-    // return the values back
-    Gia_ManForEachPi( p, pObj, i )
-        pObj->Value = 0;
-    Gia_ManForEachObjVec( vObjIds, p, pObj, i )
-        pObj->Value = Vec_IntEntry( vValues, i );
-    Vec_IntFree( vObjIds );
-    Vec_IntFree( vValues );
-    // duplicated if needed
-    if ( Gia_ManHasDangling(pNew) )
-    {
-        pNew = Gia_ManCleanup( pTemp = pNew );
-        Gia_ManStop( pTemp );
-    }
-
-    return pNew;
-}
-
-#endif
-
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////
diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c
index 673ed6c0..c7ffe95a 100644
--- a/src/base/abci/abc.c
+++ b/src/base/abci/abc.c
@@ -493,11 +493,11 @@ void Abc_FrameClearDesign()
   SeeAlso     []
 
 ***********************************************************************/
-void Abc_CommandUpdate9( Abc_Frame_t * pAbc, Gia_Man_t * pNew )
+void Abc_FrameUpdateGia( Abc_Frame_t * pAbc, Gia_Man_t * pNew )
 {
     if ( pNew == NULL )
     {
-        Abc_Print( -1, "Abc_CommandUpdate9(): Tranformation has failed.\n" );
+        Abc_Print( -1, "Abc_FrameUpdateGia(): Tranformation has failed.\n" );
         return;
     }
     // transfer names
@@ -518,6 +518,28 @@ void Abc_CommandUpdate9( Abc_Frame_t * pAbc, Gia_Man_t * pNew )
     pAbc->pGia  = pNew;
 }
 
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Gia_Man_t * Abc_FrameGetGia( Abc_Frame_t * pAbc )
+{
+    Gia_Man_t * pGia;
+    if ( pAbc->pGia2 )
+        Gia_ManStop( pAbc->pGia2 );
+    pAbc->pGia2 = NULL;
+    pGia = pAbc->pGia;
+    pAbc->pGia = NULL;
+    return pGia;
+}
+
 
 /**Function*************************************************************
 
@@ -22879,7 +22901,7 @@ int Abc_CommandCexCut( Abc_Frame_t * pAbc, int argc, char ** argv )
         Abc_Print( 1, "Command has failed.\n");
         return 0;
     }
-    Abc_CommandUpdate9( pAbc, pGiaNew );
+    Abc_FrameUpdateGia( pAbc, pGiaNew );
 */
     return 0;
 
@@ -23553,7 +23575,7 @@ int Abc_CommandAbc9Read( Abc_Frame_t * pAbc, int argc, char ** argv )
     fclose( pFile );
 
     pAig = Gia_AigerRead( FileName, fSkipStrash, 0 );
-    Abc_CommandUpdate9( pAbc, pAig );
+    Abc_FrameUpdateGia( pAbc, pAig );
     return 0;
 
 usage:
@@ -23623,7 +23645,7 @@ int Abc_CommandAbc9ReadBlif( Abc_Frame_t * pAbc, int argc, char ** argv )
     fclose( pFile );
 
     pAig = Abc_NtkHieCecTest( FileName, fVerbose );
-    Abc_CommandUpdate9( pAbc, pAig );
+    Abc_FrameUpdateGia( pAbc, pAig );
     return 0;
 
 usage:
@@ -23702,7 +23724,7 @@ int Abc_CommandAbc9ReadCBlif( Abc_Frame_t * pAbc, int argc, char ** argv )
     fclose( pFile );
 
     pAig = Abc_NtkHieCecTest2( FileName, pModelName, fVerbose );
-    Abc_CommandUpdate9( pAbc, pAig );
+    Abc_FrameUpdateGia( pAbc, pAig );
     return 0;
 
 usage:
@@ -23775,7 +23797,7 @@ int Abc_CommandAbc9ReadStg( Abc_Frame_t * pAbc, int argc, char ** argv )
     fclose( pFile );
 
     pAig = Gia_ManStgRead( FileName, kHot, fVerbose );
-    Abc_CommandUpdate9( pAbc, pAig );
+    Abc_FrameUpdateGia( pAbc, pAig );
     return 0;
 
 usage:
@@ -23845,7 +23867,7 @@ int Abc_CommandAbc9Get( Abc_Frame_t * pAbc, int argc, char ** argv )
         pMan = Abc_NtkToDar( pAbc->pNtkCur, 0, 1 );
     pAig = Gia_ManFromAig( pMan );
     Aig_ManStop( pMan );
-    Abc_CommandUpdate9( pAbc, pAig );
+    Abc_FrameUpdateGia( pAbc, pAig );
     if ( fNames )
     {
         pAig->vNamesIn  = Abc_NtkCollectCiNames( pAbc->pNtkCur );
@@ -24305,7 +24327,7 @@ int Abc_CommandAbc9Hash( Abc_Frame_t * pAbc, int argc, char ** argv )
         return 1;
     }
     pTemp = Gia_ManRehash( pAbc->pGia, fAddStrash );
-    Abc_CommandUpdate9( pAbc, pTemp );
+    Abc_FrameUpdateGia( pAbc, pTemp );
     return 0;
 
 usage:
@@ -24356,7 +24378,7 @@ int Abc_CommandAbc9Topand( Abc_Frame_t * pAbc, int argc, char ** argv )
         return 1;
     }
     pTemp = Gia_ManDupTopAnd( pAbc->pGia, fVerbose );
-    Abc_CommandUpdate9( pAbc, pTemp );
+    Abc_FrameUpdateGia( pAbc, pTemp );
     return 0;
 
 usage:
@@ -24428,13 +24450,13 @@ int Abc_CommandAbc9Cof( Abc_Frame_t * pAbc, int argc, char ** argv )
     {
         Abc_Print( -1, "Cofactoring all variables whose fanout count is higher than %d.\n", nLimFan );
         pTemp = Gia_ManDupCofAll( pAbc->pGia, nLimFan, fVerbose );
-        Abc_CommandUpdate9( pAbc, pTemp );
+        Abc_FrameUpdateGia( pAbc, pTemp );
     }
     else if ( iVar )
     {
         Abc_Print( -1, "Cofactoring one variable with object ID %d.\n", iVar );
         pTemp = Gia_ManDupCof( pAbc->pGia, iVar );
-        Abc_CommandUpdate9( pAbc, pTemp );
+        Abc_FrameUpdateGia( pAbc, pTemp );
     }
     else
     {
@@ -24519,7 +24541,7 @@ int Abc_CommandAbc9Trim( Abc_Frame_t * pAbc, int argc, char ** argv )
         pTemp = Gia_ManDupTrimmed2( pTemp2 = pTemp );
         Gia_ManStop( pTemp2 );
     }
-    Abc_CommandUpdate9( pAbc, pTemp );
+    Abc_FrameUpdateGia( pAbc, pTemp );
     return 0;
 
 usage:
@@ -24595,7 +24617,7 @@ int Abc_CommandAbc9Dfs( Abc_Frame_t * pAbc, int argc, char ** argv )
         if ( fVerbose )
             Abc_Print( -1, "AIG objects are reordered in the DFS order.\n" );
     }
-    Abc_CommandUpdate9( pAbc, pTemp );
+    Abc_FrameUpdateGia( pAbc, pTemp );
     return 0;
 
 usage:
@@ -25666,7 +25688,7 @@ int Abc_CommandAbc9Times( Abc_Frame_t * pAbc, int argc, char ** argv )
         return 1;
     }
     pTemp = Gia_ManDupTimes( pAbc->pGia, nTimes );
-    Abc_CommandUpdate9( pAbc, pTemp );
+    Abc_FrameUpdateGia( pAbc, pTemp );
     return 0;
 
 usage:
@@ -25763,7 +25785,7 @@ int Abc_CommandAbc9Frames( Abc_Frame_t * pAbc, int argc, char ** argv )
         pTemp = Gia_ManFrames2( pAbc->pGia, pPars );
     else
         pTemp = Gia_ManFrames( pAbc->pGia, pPars );
-    Abc_CommandUpdate9( pAbc, pTemp );
+    Abc_FrameUpdateGia( pAbc, pTemp );
     return 0;
 
 usage:
@@ -25832,7 +25854,7 @@ int Abc_CommandAbc9Retime( Abc_Frame_t * pAbc, int argc, char ** argv )
         return 0;
     }
     pTemp = Gia_ManRetimeForward( pAbc->pGia, nMaxIters, fVerbose );
-    Abc_CommandUpdate9( pAbc, pTemp );
+    Abc_FrameUpdateGia( pAbc, pTemp );
     return 0;
 
 usage:
@@ -25887,7 +25909,7 @@ int Abc_CommandAbc9Enable( Abc_Frame_t * pAbc, int argc, char ** argv )
         pTemp = Gia_ManRemoveEnables( pAbc->pGia );
     else
         pTemp = Gia_ManDupSelf( pAbc->pGia );
-    Abc_CommandUpdate9( pAbc, pTemp );
+    Abc_FrameUpdateGia( pAbc, pTemp );
     return 0;
 
 usage:
@@ -25938,7 +25960,7 @@ int Abc_CommandAbc9Dc2( Abc_Frame_t * pAbc, int argc, char ** argv )
         return 1;
     }
     pTemp = Gia_ManCompress2( pAbc->pGia, fUpdateLevel, fVerbose );
-    Abc_CommandUpdate9( pAbc, pTemp );
+    Abc_FrameUpdateGia( pAbc, pTemp );
     return 0;
 
 usage:
@@ -25994,7 +26016,7 @@ int Abc_CommandAbc9Bidec( Abc_Frame_t * pAbc, int argc, char ** argv )
         return 1;
     }
     pTemp = Gia_ManPerformBidec( pAbc->pGia, fVerbose );
-    Abc_CommandUpdate9( pAbc, pTemp );
+    Abc_FrameUpdateGia( pAbc, pTemp );
     return 0;
 
 usage:
@@ -26050,7 +26072,7 @@ int Abc_CommandAbc9Shrink( Abc_Frame_t * pAbc, int argc, char ** argv )
         return 1;
     }
     pTemp = Gia_ManPerformMapShrink( pAbc->pGia, fKeepLevel, fVerbose );
-    Abc_CommandUpdate9( pAbc, pTemp );
+    Abc_FrameUpdateGia( pAbc, pTemp );
     return 0;
 
 usage:
@@ -26122,7 +26144,7 @@ int Abc_CommandAbc9Miter( Abc_Frame_t * pAbc, int argc, char ** argv )
             return 1;
         }
         pAux = Gia_ManTransformMiter( pAbc->pGia );
-        Abc_CommandUpdate9( pAbc, pAux );
+        Abc_FrameUpdateGia( pAbc, pAux );
         Abc_Print( 1, "The miter (current AIG) is transformed by XORing POs pair-wise.\n" );
         return 0;
     }
@@ -26159,7 +26181,7 @@ int Abc_CommandAbc9Miter( Abc_Frame_t * pAbc, int argc, char ** argv )
     // compute the miter
     pAux = Gia_ManMiter( pAbc->pGia, pSecond, fDualOut, fSeq, fVerbose );
     Gia_ManStop( pSecond );
-    Abc_CommandUpdate9( pAbc, pAux );
+    Abc_FrameUpdateGia( pAbc, pAux );
     return 0;
 
 usage:
@@ -26294,7 +26316,7 @@ int Abc_CommandAbc9Scl( Abc_Frame_t * pAbc, int argc, char ** argv )
         return 1;
     }
     pTemp = Gia_ManSeqStructSweep( pAbc->pGia, fConst, fEquiv, fVerbose );
-    Abc_CommandUpdate9( pAbc, pTemp );
+    Abc_FrameUpdateGia( pAbc, pTemp );
     return 0;
 
 usage:
@@ -26387,7 +26409,7 @@ int Abc_CommandAbc9Lcorr( Abc_Frame_t * pAbc, int argc, char ** argv )
         return 0;
     }
     pTemp = Cec_ManLSCorrespondence( pAbc->pGia, pPars );
-    Abc_CommandUpdate9( pAbc, pTemp );
+    Abc_FrameUpdateGia( pAbc, pTemp );
     return 0;
 
 usage:
@@ -26494,7 +26516,7 @@ int Abc_CommandAbc9Scorr( Abc_Frame_t * pAbc, int argc, char ** argv )
         return 0;
     }
     pTemp = Cec_ManLSCorrespondence( pAbc->pGia, pPars );
-    Abc_CommandUpdate9( pAbc, pTemp );
+    Abc_FrameUpdateGia( pAbc, pTemp );
     return 0;
 
 usage:
@@ -26563,7 +26585,7 @@ int Abc_CommandAbc9Choice( Abc_Frame_t * pAbc, int argc, char ** argv )
         return 1;
     }
     pTemp = Cec_ManChoiceComputation( pAbc->pGia, pPars );
-    Abc_CommandUpdate9( pAbc, pTemp );
+    Abc_FrameUpdateGia( pAbc, pTemp );
     return 0;
 
 usage:
@@ -26672,7 +26694,7 @@ int Abc_CommandAbc9Sat( Abc_Frame_t * pAbc, int argc, char ** argv )
     else
     {
         pTemp = Cec_ManSatSolving( pAbc->pGia, pPars );
-        Abc_CommandUpdate9( pAbc, pTemp );
+        Abc_FrameUpdateGia( pAbc, pTemp );
     }
     return 0;
 
@@ -26805,7 +26827,7 @@ int Abc_CommandAbc9Fraig( Abc_Frame_t * pAbc, int argc, char ** argv )
         return 1;
     }
     pTemp = Cec_ManSatSweeping( pAbc->pGia, pPars );
-    Abc_CommandUpdate9( pAbc, pTemp );
+    Abc_FrameUpdateGia( pAbc, pTemp );
     return 0;
 
 usage:
@@ -26885,7 +26907,7 @@ int Abc_CommandAbc9CFraig( Abc_Frame_t * pAbc, int argc, char ** argv )
         return 1;
     }
     pTemp = Gia_SweeperFraigTest( pAbc->pGia, nWords, nConfs, fVerbose );
-    Abc_CommandUpdate9( pAbc, pTemp );
+    Abc_FrameUpdateGia( pAbc, pTemp );
     return 0;
 
 usage:
@@ -27229,7 +27251,7 @@ int Abc_CommandAbc9Reduce( Abc_Frame_t * pAbc, int argc, char ** argv )
     }
     else
         pTemp = Gia_ManEquivReduceAndRemap( pAbc->pGia, 1, fDualOut );
-    Abc_CommandUpdate9( pAbc, pTemp );
+    Abc_FrameUpdateGia( pAbc, pTemp );
     return 0;
 
 usage:
@@ -27578,7 +27600,7 @@ int Abc_CommandAbc9Sweep( Abc_Frame_t * pAbc, int argc, char ** argv )
         return 1;
     }
     pTemp = Gia_ManFraigSweep( pAbc->pGia, pPars );
-    Abc_CommandUpdate9( pAbc, pTemp );
+    Abc_FrameUpdateGia( pAbc, pTemp );
     return 0;
 
 usage:
@@ -28117,7 +28139,7 @@ int Abc_CommandAbc9If( Abc_Frame_t * pAbc, int argc, char ** argv )
         Abc_Print( -1, "Abc_CommandAbc9If(): Mapping of the AIG has failed.\n" );
         return 1;
     }
-    Abc_CommandUpdate9( pAbc, pNew );
+    Abc_FrameUpdateGia( pAbc, pNew );
     return 0;
 
 usage:
@@ -28304,7 +28326,7 @@ int Abc_CommandAbc9Speedup( Abc_Frame_t * pAbc, int argc, char ** argv )
     }
     pAbc->pGia->pLutLib = fUseLutLib ? pAbc->pLibLut : NULL;
     pTemp = Gia_ManSpeedup( pAbc->pGia, Percentage, Degree, fVerbose, fVeryVerbose );
-    Abc_CommandUpdate9( pAbc, pTemp );
+    Abc_FrameUpdateGia( pAbc, pTemp );
     return 0;
 
 usage:
@@ -28493,7 +28515,7 @@ int Abc_CommandAbc9Dch( Abc_Frame_t * pAbc, int argc, char ** argv )
         return 1;
     }
     pTemp = Gia_ManPerformDch( pAbc->pGia, pPars );
-    Abc_CommandUpdate9( pAbc, pTemp );
+    Abc_FrameUpdateGia( pAbc, pTemp );
     return 0;
 
 usage:
@@ -28570,7 +28592,7 @@ int Abc_CommandAbc9Rpm( Abc_Frame_t * pAbc, int argc, char ** argv )
         pTemp = Abs_RpmPerformOld( pAbc->pGia, fVerbose );
     else
         pTemp = Abs_RpmPerform( pAbc->pGia, nCutMax, fVerbose, fVeryVerbose );
-    Abc_CommandUpdate9( pAbc, pTemp );
+    Abc_FrameUpdateGia( pAbc, pTemp );
     return 0;
 
 usage:
@@ -28662,7 +28684,7 @@ int Abc_CommandAbc9BackReach( Abc_Frame_t * pAbc, int argc, char ** argv )
         return 1;
     }
     pTemp = Gia_ManCofTest( pAbc->pGia, nFrameMax, nConfMax, nTimeMax, fVerbose );
-    Abc_CommandUpdate9( pAbc, pTemp );
+    Abc_FrameUpdateGia( pAbc, pTemp );
     return 0;
 
 usage:
@@ -28730,7 +28752,7 @@ int Abc_CommandAbc9Posplit( Abc_Frame_t * pAbc, int argc, char ** argv )
     {
         pTemp = Gia_ManFromAigSimple( pMan );
         Aig_ManStop( pMan );
-        Abc_CommandUpdate9( pAbc, pTemp );
+        Abc_FrameUpdateGia( pAbc, pTemp );
     }
     return 0;
 
@@ -29459,7 +29481,7 @@ int Abc_CommandAbc9Iso( Abc_Frame_t * pAbc, int argc, char ** argv )
     // update the internal storage of PO equivalences
     Abc_FrameReplacePoEquivs( pAbc, &vPosEquivs );
     // update the AIG
-    Abc_CommandUpdate9( pAbc, pAig );
+    Abc_FrameUpdateGia( pAbc, pAig );
     return 0;
 
 usage:
@@ -29570,7 +29592,7 @@ int Abc_CommandAbc9Cycle( Abc_Frame_t * pAbc, int argc, char ** argv )
         return 1;
     }
     pTemp = Gia_ManDupCycled( pAbc->pGia, nFrames );
-    Abc_CommandUpdate9( pAbc, pTemp );
+    Abc_FrameUpdateGia( pAbc, pTemp );
     return 0;
 
 usage:
@@ -29665,7 +29687,7 @@ int Abc_CommandAbc9Cone( Abc_Frame_t * pAbc, int argc, char ** argv )
     }
     pTemp = Gia_ManConeExtract( pAbc->pGia, iOutNum, nDelta, nOutsMin, nOutsMax );
     if ( pTemp )
-        Abc_CommandUpdate9( pAbc, pTemp );
+        Abc_FrameUpdateGia( pAbc, pTemp );
     return 0;
 
 usage:
@@ -29930,7 +29952,7 @@ int Abc_CommandAbc9AbsDerive( Abc_Frame_t * pAbc, int argc, char ** argv )
         return 0;
     }
     pTemp = Gia_ManDupAbsFlops( pAbc->pGia, pAbc->pGia->vFlopClasses );
-    Abc_CommandUpdate9( pAbc, pTemp );
+    Abc_FrameUpdateGia( pAbc, pTemp );
     return 0;
 
 usage:
@@ -30072,7 +30094,7 @@ int Abc_CommandAbc9GlaDerive( Abc_Frame_t * pAbc, int argc, char ** argv )
     pTemp = Gia_ManDupAbsGates( pAbc->pGia, pAbc->pGia->vGateClasses );
     Gia_ManStop( pTemp );
     pTemp = Gia_ManDupAbsGates( pAbc->pGia, pAbc->pGia->vGateClasses );
-    Abc_CommandUpdate9( pAbc, pTemp );
+    Abc_FrameUpdateGia( pAbc, pTemp );
 //    Abc_Print( 1,"This command is currently not enabled.\n" );
     return 0;
 
diff --git a/src/base/main/main.h b/src/base/main/main.h
index 7f2d11bf..4257d623 100644
--- a/src/base/main/main.h
+++ b/src/base/main/main.h
@@ -82,6 +82,8 @@ extern ABC_DLL int             Abc_FrameSetMode( Abc_Frame_t * p, int fNameMode
 extern ABC_DLL void            Abc_FrameRestart( Abc_Frame_t * p );
 extern ABC_DLL int             Abc_FrameShowProgress( Abc_Frame_t * p );
 extern ABC_DLL void            Abc_FrameClearVerifStatus( Abc_Frame_t * p );
+extern ABC_DLL void            Abc_FrameUpdateGia( Abc_Frame_t * p, Gia_Man_t * pNew );
+extern ABC_DLL Gia_Man_t *     Abc_FrameGetGia( Abc_Frame_t * p );
 
 extern ABC_DLL void            Abc_FrameSetCurrentNetwork( Abc_Frame_t * p, Abc_Ntk_t * pNet );
 extern ABC_DLL void            Abc_FrameSwapCurrentAndBackup( Abc_Frame_t * p );