From ecae67e3bf4580591d1bbadd02696b2490fd469d Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Mon, 4 Sep 2017 15:57:00 -0700 Subject: Several changes to various packages. --- src/aig/gia/giaDup.c | 21 +++++++++++++++++++++ src/base/abc/abc.h | 2 ++ src/base/abc/abcNtk.c | 49 ++++++++++++++++++++++++++++++++++++++++++++++++ src/base/abc/abcUtil.c | 49 ++++++++++++++++++++++++++++++++++++++++++++---- src/base/abci/abc.c | 1 - src/base/abci/abcDar.c | 29 ++++++++++++++++++++++++++++ src/sat/bsat/satInterA.c | 3 ++- 7 files changed, 148 insertions(+), 6 deletions(-) (limited to 'src') diff --git a/src/aig/gia/giaDup.c b/src/aig/gia/giaDup.c index b05c8636..477c44dc 100644 --- a/src/aig/gia/giaDup.c +++ b/src/aig/gia/giaDup.c @@ -764,6 +764,27 @@ Gia_Man_t * Gia_ManDupWithAttributes( Gia_Man_t * p ) pNew->pCellStr = Abc_UtilStrsav( p->pCellStr ); return pNew; } +Gia_Man_t * Gia_ManDupRemovePis( Gia_Man_t * p, int nRemPis ) +{ + Gia_Man_t * pNew; + Gia_Obj_t * pObj; + int i; + pNew = Gia_ManStart( Gia_ManObjNum(p) ); + pNew->pName = Abc_UtilStrsav( p->pName ); + pNew->pSpec = Abc_UtilStrsav( p->pSpec ); + Gia_ManConst0(p)->Value = 0; + Gia_ManForEachObj1( p, pObj, i ) + { + if ( Gia_ObjIsAnd(pObj) ) + pObj->Value = Gia_ManAppendAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) ); + else if ( Gia_ObjIsCi(pObj) && Gia_ObjCioId(pObj) < Gia_ManCiNum(p)-nRemPis ) + pObj->Value = Gia_ManAppendCi( pNew ); + else if ( Gia_ObjIsCo(pObj) ) + pObj->Value = Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) ); + } + Gia_ManSetRegNum( pNew, Gia_ManRegNum(p) ); + return pNew; +} /**Function************************************************************* diff --git a/src/base/abc/abc.h b/src/base/abc/abc.h index 8defc9d4..51ed350e 100644 --- a/src/base/abc/abc.h +++ b/src/base/abc/abc.h @@ -602,6 +602,7 @@ extern ABC_DLL int Abc_NtkCheckUniqueCioNames( Abc_Ntk_t * pNtk ) /*=== abcCollapse.c ==========================================================*/ extern ABC_DLL Abc_Ntk_t * Abc_NtkCollapse( Abc_Ntk_t * pNtk, int fBddSizeMax, int fDualRail, int fReorder, int fVerbose ); extern ABC_DLL Abc_Ntk_t * Abc_NtkCollapseSat( Abc_Ntk_t * pNtk, int nCubeLim, int nBTLimit, int nCostMax, int fCanon, int fReverse, int fCnfShared, int fVerbose ); +extern ABC_DLL Gia_Man_t * Abc_NtkClpGia( Abc_Ntk_t * pNtk ); /*=== abcCut.c ==========================================================*/ extern ABC_DLL void * Abc_NodeGetCutsRecursive( void * p, Abc_Obj_t * pObj, int fDag, int fTree ); extern ABC_DLL void * Abc_NodeGetCuts( void * p, Abc_Obj_t * pObj, int fDag, int fTree ); @@ -787,6 +788,7 @@ extern ABC_DLL void Abc_NtkMakeComb( Abc_Ntk_t * pNtk, int fRemove extern ABC_DLL void Abc_NtkPermute( Abc_Ntk_t * pNtk, int fInputs, int fOutputs, int fFlops, char * pFlopPermFile ); extern ABC_DLL void Abc_NtkUnpermute( Abc_Ntk_t * pNtk ); extern ABC_DLL Abc_Ntk_t * Abc_NtkCreateFromSops( char * pName, Vec_Ptr_t * vSops ); +extern ABC_DLL Abc_Ntk_t * Abc_NtkCreateFromGias( char * pName, Vec_Ptr_t * vGias ); /*=== abcObj.c ==========================================================*/ extern ABC_DLL Abc_Obj_t * Abc_ObjAlloc( Abc_Ntk_t * pNtk, Abc_ObjType_t Type ); extern ABC_DLL void Abc_ObjRecycle( Abc_Obj_t * pObj ); diff --git a/src/base/abc/abcNtk.c b/src/base/abc/abcNtk.c index ff1a2822..a62542b9 100644 --- a/src/base/abc/abcNtk.c +++ b/src/base/abc/abcNtk.c @@ -2239,6 +2239,55 @@ Abc_Ntk_t * Abc_NtkCreateFromSops( char * pName, Vec_Ptr_t * vSops ) return pNtk; } +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Abc_Ntk_t * Abc_NtkCreateFromGias( char * pName, Vec_Ptr_t * vGias ) +{ + Gia_Man_t * pGia = (Gia_Man_t *)Vec_PtrEntry(vGias, 0); + Abc_Ntk_t * pNtk = Abc_NtkAlloc( ABC_NTK_STRASH, ABC_FUNC_AIG, 1 ); + Abc_Obj_t * pAbcObj, * pAbcObjPo; + Gia_Obj_t * pObj; int i, k; + pNtk->pName = Extra_UtilStrsav( pName ); + for ( k = 0; k < Gia_ManCiNum(pGia); k++ ) + Abc_NtkCreatePi( pNtk ); + Vec_PtrForEachEntry( Gia_Man_t *, vGias, pGia, i ) + { + assert( Gia_ManCoNum(pGia) == 1 ); + Gia_ManCleanValue(pGia); + Gia_ManForEachCi( pGia, pObj, k ) + pObj->Value = Abc_ObjId( Abc_NtkCi(pNtk, k) ); + Gia_ManForEachAnd( pGia, pObj, k ) + { + Abc_Obj_t * pAbcObj0 = Abc_NtkObj( pNtk, Gia_ObjFanin0(pObj)->Value ); + Abc_Obj_t * pAbcObj1 = Abc_NtkObj( pNtk, Gia_ObjFanin1(pObj)->Value ); + pAbcObj0 = Abc_ObjNotCond( pAbcObj0, Gia_ObjFaninC0(pObj) ); + pAbcObj1 = Abc_ObjNotCond( pAbcObj1, Gia_ObjFaninC1(pObj) ); + pAbcObj = Abc_AigAnd( (Abc_Aig_t *)pNtk->pManFunc, pAbcObj0, pAbcObj1 ); + pObj->Value = Abc_ObjId( pAbcObj ); + } + pObj = Gia_ManCo(pGia, 0); + if ( Gia_ObjFaninId0p(pGia, pObj) == 0 ) + pAbcObj = Abc_ObjNot( Abc_AigConst1(pNtk) ); + else + pAbcObj = Abc_NtkObj( pNtk, Gia_ObjFanin0(pObj)->Value ); + pAbcObj = Abc_ObjNotCond( pAbcObj, Gia_ObjFaninC0(pObj) ); + pAbcObjPo = Abc_NtkCreatePo( pNtk ); + Abc_ObjAddFanin( pAbcObjPo, pAbcObj ); + } + Abc_NtkAddDummyPiNames( pNtk ); + Abc_NtkAddDummyPoNames( pNtk ); + return pNtk; +} + //////////////////////////////////////////////////////////////////////// /// END OF FILE /// diff --git a/src/base/abc/abcUtil.c b/src/base/abc/abcUtil.c index 6b67d82a..8cac0a42 100644 --- a/src/base/abc/abcUtil.c +++ b/src/base/abc/abcUtil.c @@ -3142,6 +3142,45 @@ Vec_Wec_t * Abc_SopSynthesize( Vec_Ptr_t * vSops ) assert( Vec_WecSize(vRes) == iNode ); return vRes; } +Vec_Wec_t * Abc_GiaSynthesize( Vec_Ptr_t * vGias ) +{ + Vec_Wec_t * vRes = NULL; + Abc_Ntk_t * pNtk = Abc_NtkCreateFromGias( "top", vGias ); + Abc_Ntk_t * pNtkNew; + Abc_Obj_t * pObj, * pFanin; + int i, k, iNode = 0; + Abc_FrameReplaceCurrentNetwork( Abc_FrameReadGlobalFrame(), pNtk ); + Cmd_CommandExecute( Abc_FrameGetGlobalFrame(), "dc2; map -a" ); + pNtkNew = Abc_FrameReadNtk( Abc_FrameReadGlobalFrame() ); + vRes = Vec_WecStart( Abc_NtkPiNum(pNtkNew) + Abc_NtkNodeNum(pNtkNew) + Abc_NtkPoNum(pNtkNew) ); + Abc_NtkForEachPi( pNtkNew, pObj, i ) + pObj->iTemp = iNode++; + Abc_NtkForEachNode( pNtkNew, pObj, i ) + { + Vec_Int_t * vNode = Vec_WecEntry(vRes, iNode); + Vec_IntPush( vNode, Abc_GateToType(pObj) ); + Vec_IntPush( vNode, iNode ); + Abc_ObjForEachFanin( pObj, pFanin, k ) + Vec_IntPush( vNode, pFanin->iTemp ); + pObj->iTemp = iNode++; + } + Abc_NtkForEachPo( pNtkNew, pObj, i ) + Vec_IntPushTwo( Vec_WecEntry(vRes, iNode++), ABC_OPER_BIT_BUF, Abc_ObjFanin0(pObj)->iTemp ); + assert( Vec_WecSize(vRes) == iNode ); + return vRes; +} +Gia_Man_t * Abc_GiaSynthesizeInter( Gia_Man_t * p ) +{ + Abc_Ntk_t * pNtkNew, * pNtk; + Vec_Ptr_t * vGias = Vec_PtrAlloc( 1 ); + Vec_PtrPush( vGias, p ); + pNtk = Abc_NtkCreateFromGias( "top", vGias ); + Vec_PtrFree( vGias ); + Abc_FrameReplaceCurrentNetwork( Abc_FrameReadGlobalFrame(), pNtk ); + Cmd_CommandExecute( Abc_FrameGetGlobalFrame(), "ps; balance; collapse; ps; muxes; strash; ps; dc2; ps" ); + pNtkNew = Abc_FrameReadNtk( Abc_FrameReadGlobalFrame() ); + return Abc_NtkClpGia( pNtkNew ); +} /**Function************************************************************* @@ -3197,11 +3236,10 @@ Gia_Man_t * Abc_NtkStrashToGia( Abc_Ntk_t * pNtk ) Gia_ManStop( pTemp ); return pNew; } -Gia_Man_t * Abc_SopSynthesizeOne( Vec_Ptr_t * vSops ) +Gia_Man_t * Abc_SopSynthesizeOne( char * pSop ) { Abc_Ntk_t * pNtkNew, * pNtk; - char * pSop = (char *)Vec_PtrEntry(vSops, 0); - assert( Vec_PtrSize(vSops) == 1 ); + Vec_Ptr_t * vSops; if ( strlen(pSop) == 3 ) { Gia_Man_t * pNew = Gia_ManStart( 1 ); @@ -3211,9 +3249,12 @@ Gia_Man_t * Abc_SopSynthesizeOne( Vec_Ptr_t * vSops ) Gia_ManAppendCo( pNew, pSop[1] == '1' ); return pNew; } + vSops = Vec_PtrAlloc( 1 ); + Vec_PtrPush( vSops, pSop ); pNtk = Abc_NtkCreateFromSops( "top", vSops ); + Vec_PtrFree( vSops ); Abc_FrameReplaceCurrentNetwork( Abc_FrameReadGlobalFrame(), pNtk ); - Cmd_CommandExecute( Abc_FrameGetGlobalFrame(), "fx; strash; dc2" ); + Cmd_CommandExecute( Abc_FrameGetGlobalFrame(), "fx; strash; balance; dc2" ); pNtkNew = Abc_FrameReadNtk( Abc_FrameReadGlobalFrame() ); return Abc_NtkStrashToGia( pNtkNew ); } diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c index a6a77571..45198165 100644 --- a/src/base/abci/abc.c +++ b/src/base/abci/abc.c @@ -9883,7 +9883,6 @@ usage: ***********************************************************************/ int Abc_CommandExpand( Abc_Frame_t * pAbc, int argc, char ** argv ) { - extern Gia_Man_t * Abc_NtkClpGia( Abc_Ntk_t * pNtk ); extern void Abc_NtkExpandCubes( Abc_Ntk_t * pNtk, Gia_Man_t * pGia, int fVerbose ); Abc_Ntk_t * pStrash, * pNtk2, * pNtk = Abc_FrameReadNtk(pAbc); Gia_Man_t * pGia; int c, fVerbose = 0; diff --git a/src/base/abci/abcDar.c b/src/base/abci/abcDar.c index 996ae6a2..8ec810f5 100644 --- a/src/base/abci/abcDar.c +++ b/src/base/abci/abcDar.c @@ -3773,6 +3773,35 @@ Abc_Ntk_t * Abc_NtkInterOne( Abc_Ntk_t * pNtkOn, Abc_Ntk_t * pNtkOff, int fRelat Aig_ManStop( pManAig ); return pNtkAig; } +Gia_Man_t * Gia_ManInterOne( Gia_Man_t * pNtkOn, Gia_Man_t * pNtkOff, int fVerbose ) +{ + extern Aig_Man_t * Aig_ManInter( Aig_Man_t * pManOn, Aig_Man_t * pManOff, int fRelation, int fVerbose ); + Gia_Man_t * pNtkAig; + Aig_Man_t * pManOn, * pManOff, * pManAig; + assert( Gia_ManCiNum(pNtkOn) == Gia_ManCiNum(pNtkOff) ); + assert( Gia_ManCoNum(pNtkOn) == 1 ); + assert( Gia_ManCoNum(pNtkOff) == 1 ); + // create internal AIGs + pManOn = Gia_ManToAigSimple( pNtkOn ); + if ( pManOn == NULL ) + return NULL; + pManOff = Gia_ManToAigSimple( pNtkOff ); + if ( pManOff == NULL ) + return NULL; + // derive the interpolant + pManAig = Aig_ManInter( pManOn, pManOff, 0, fVerbose ); + if ( pManAig == NULL ) + { + Abc_Print( 1, "Interpolant computation failed.\n" ); + return NULL; + } + Aig_ManStop( pManOn ); + Aig_ManStop( pManOff ); + // create logic network + pNtkAig = Gia_ManFromAigSimple( pManAig ); + Aig_ManStop( pManAig ); + return pNtkAig; +} /**Function************************************************************* diff --git a/src/sat/bsat/satInterA.c b/src/sat/bsat/satInterA.c index c769352f..df127d1d 100644 --- a/src/sat/bsat/satInterA.c +++ b/src/sat/bsat/satInterA.c @@ -1019,10 +1019,11 @@ void * Inta_ManInterpolate( Inta_Man_t * p, Sto_Man_t * pCnf, abctime TimeToStop if ( fVerbose ) { // ABC_PRT( "Interpo", Abc_Clock() - clkTotal ); - printf( "Vars = %d. Roots = %d. Learned = %d. Resol steps = %d. Ave = %.2f. Mem = %.2f MB\n", + printf( "Vars = %d. Roots = %d. Learned = %d. Resol steps = %d. Ave = %.2f. Mem = %.2f MB ", p->pCnf->nVars, p->pCnf->nRoots, p->pCnf->nClauses-p->pCnf->nRoots, p->Counter, 1.0*(p->Counter-p->pCnf->nRoots)/(p->pCnf->nClauses-p->pCnf->nRoots), 1.0*Sto_ManMemoryReport(p->pCnf)/(1<<20) ); + Abc_PrintTime( 1, "Time", Abc_Clock() - clkTotal ); p->timeTotal += Abc_Clock() - clkTotal; } -- cgit v1.2.3