luke
/
abc
mirror of https://github.com/YosysHQ/abc.git
1
0
Fork 0
Code Issues Packages Projects Releases Wiki Activity

User-controlable SAT sweeper.

This commit is contained in:
Alan Mishchenko 2013-03-04 00:33:36 -08:00
parent c959cf1ba1
commit 0c9337f627
4 changed files with 161 additions and 122 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

2
src/aig/gia/gia.h
View File

@ -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 );

171
src/aig/gia/giaSweeper.c
View File

@ -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 ///
////////////////////////////////////////////////////////////////////////

108
src/base/abci/abc.c
View File

@ -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;

2
src/base/main/main.h
View File

@ -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 );