diff options
| -rw-r--r-- | src/aig/gia/giaDup.c | 81 | ||||
| -rw-r--r-- | src/base/abci/abc.c | 26 | ||||
| -rw-r--r-- | src/proof/cec/cecSplit.c | 32 |
3 files changed, 137 insertions, 2 deletions
diff --git a/src/aig/gia/giaDup.c b/src/aig/gia/giaDup.c index c7a0f3dc..747e68b1 100644 --- a/src/aig/gia/giaDup.c +++ b/src/aig/gia/giaDup.c @@ -2749,6 +2749,87 @@ Gia_Man_t * Gia_ManDupSliced( Gia_Man_t * p, int nSuppMax ) } +/**Function************************************************************* + + Synopsis [Extract constraints.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Gia_ManDupWithConstrCollectAnd_rec( Gia_Man_t * p, Gia_Obj_t * pObj, Vec_Int_t * vSuper ) +{ + if ( Gia_IsComplement(pObj) || !Gia_ObjIsAnd(pObj) ) + { + Vec_IntPushUnique( vSuper, Gia_ObjToLit(p, pObj) ); + return; + } + Gia_ManDupWithConstrCollectAnd_rec( p, Gia_ObjChild0(pObj), vSuper ); + Gia_ManDupWithConstrCollectAnd_rec( p, Gia_ObjChild1(pObj), vSuper ); +} +Gia_Man_t * Gia_ManDupWithConstr( Gia_Man_t * p ) +{ + Vec_Int_t * vSuper; + Gia_Man_t * pNew, * pTemp; + Gia_Obj_t * pObj; + int i, iDriver, iLit, iLitBest = -1, LevelBest = -1; + assert( Gia_ManPoNum(p) == 1 ); + assert( Gia_ManRegNum(p) == 0 ); + pObj = Gia_ManPo( p, 0 ); + if ( Gia_ObjFaninC0(pObj) ) + { + printf( "The miter's output is not AND-decomposable.\n" ); + return NULL; + } + vSuper = Vec_IntAlloc( 100 ); + Gia_ManDupWithConstrCollectAnd_rec( p, Gia_ObjChild0(pObj), vSuper ); + assert( Vec_IntSize(vSuper) > 1 ); + // find the highest level + Gia_ManLevelNum( p ); + Vec_IntForEachEntry( vSuper, iLit, i ) + if ( LevelBest < Gia_ObjLevelId(p, Abc_Lit2Var(iLit)) ) + LevelBest = Gia_ObjLevelId(p, Abc_Lit2Var(iLit)), iLitBest = iLit; + assert( iLitBest != -1 ); + // create new manager + pNew = Gia_ManStart( Gia_ManObjNum(p) ); + pNew->pName = Abc_UtilStrsav( p->pName ); + pNew->pSpec = Abc_UtilStrsav( p->pSpec ); + Gia_ManConst0(p)->Value = 0; + Gia_ManHashAlloc( pNew ); + Gia_ManForEachObj1( p, pObj, i ) + { + if ( Gia_ObjIsAnd(pObj) ) + pObj->Value = Gia_ManHashAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) ); + else if ( Gia_ObjIsCi(pObj) ) + pObj->Value = Gia_ManAppendCi( pNew ); + } + // create AND of nodes + iDriver = -1; + Vec_IntForEachEntry( vSuper, iLit, i ) + { + if ( iLit == iLitBest ) + continue; + if ( iDriver == -1 ) + iDriver = Gia_ObjLitCopy(p, iLit); + else + iDriver = Gia_ManHashAnd( pNew, iDriver, Gia_ObjLitCopy(p, iLit) ); + } + // create the main PO + Gia_ManAppendCo( pNew, Gia_ObjLitCopy(p, iLitBest) ); + // create the constraint PO + Gia_ManAppendCo( pNew, Abc_LitNot(iDriver) ); + pNew->nConstrs = 1; + // rehash + pNew = Gia_ManCleanup( pTemp = pNew ); + Gia_ManStop( pTemp ); + Vec_IntFree( vSuper ); + return pNew; + +} + //////////////////////////////////////////////////////////////////////// /// END OF FILE /// //////////////////////////////////////////////////////////////////////// diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c index 5bb79eef..9bd645e6 100644 --- a/src/base/abci/abc.c +++ b/src/base/abci/abc.c @@ -23072,9 +23072,33 @@ int Abc_CommandUnfold( Abc_Frame_t * pAbc, int argc, char ** argv ) Abc_Print( -1, "Empty network.\n" ); return 1; } + if ( Abc_NtkIsComb(pNtk) && Abc_NtkPoNum(pNtk) > 1 ) + { + Abc_Print( -1, "Combinational miter has more than one PO.\n" ); + return 0; + } if ( Abc_NtkIsComb(pNtk) ) { - Abc_Print( -1, "The network is combinational.\n" ); + extern Gia_Man_t * Gia_ManDupWithConstr( Gia_Man_t * p ); + Gia_Man_t * pNew; + Aig_Man_t * pAig = Abc_NtkToDar( pNtk, 0, 0 ); + Gia_Man_t * pGia = Gia_ManFromAigSimple( pAig ); + Aig_ManStop( pAig ); + pNew = Gia_ManDupWithConstr( pGia ); + if ( pNew == NULL ) + { + Abc_Print( -1, "Cannot extract constrains from the miter.\n" ); + return 0; + } + Gia_ManStop( pGia ); + pAig = Gia_ManToAigSimple( pNew ); + Gia_ManStop( pNew ); + pNtkRes = Abc_NtkFromAigPhase( pAig ); + Aig_ManStop( pAig ); + ABC_FREE( pNtkRes->pName ); + pNtkRes->pName = Extra_UtilStrsav( pNtk->pName ); + // replace the current network + Abc_FrameReplaceCurrentNetwork( pAbc, pNtkRes ); return 0; } if ( !Abc_NtkIsStrash(pNtk) ) diff --git a/src/proof/cec/cecSplit.c b/src/proof/cec/cecSplit.c index 5279570e..ece365bc 100644 --- a/src/proof/cec/cecSplit.c +++ b/src/proof/cec/cecSplit.c @@ -558,7 +558,7 @@ void * Cec_GiaSplitWorkerThread( void * pArg ) assert( 0 ); return NULL; } -int Cec_GiaSplitTest( Gia_Man_t * p, int nProcs, int nTimeOut, int nIterMax, int LookAhead, int fVerbose, int fVeryVerbose ) +int Cec_GiaSplitTestInt( Gia_Man_t * p, int nProcs, int nTimeOut, int nIterMax, int LookAhead, int fVerbose, int fVeryVerbose ) { abctime clkTotal = Abc_Clock(); Par_ThData_t ThData[PAR_THR_MAX]; @@ -721,6 +721,36 @@ finish: fflush( stdout ); return RetValue; } +int Cec_GiaSplitTest( Gia_Man_t * p, int nProcs, int nTimeOut, int nIterMax, int LookAhead, int fVerbose, int fVeryVerbose ) +{ + Abc_Cex_t * pCex = NULL; + Gia_Man_t * pOne; + Gia_Obj_t * pObj; + int i, RetValue1, fOneUndef = 0, RetValue = -1; + Abc_CexFreeP( &p->pCexComb ); + Gia_ManForEachPo( p, pObj, i ) + { + pOne = Gia_ManDupOutputGroup( p, i, i+1 ); + if ( fVerbose ) + printf( "\nSolving output %d:\n", i ); + RetValue1 = Cec_GiaSplitTestInt( pOne, nProcs, nTimeOut, nIterMax, LookAhead, fVerbose, fVeryVerbose ); + Gia_ManStop( pOne ); + // collect the result + if ( RetValue1 == 0 && RetValue == -1 ) + { + pCex = pOne->pCexComb; pOne->pCexComb = NULL; + pCex->iPo = i; + RetValue = 0; + } + if ( RetValue1 == -1 ) + fOneUndef = 1; + } + if ( RetValue == -1 ) + RetValue = fOneUndef ? -1 : 1; + else + p->pCexComb = pCex; + return RetValue; +} //////////////////////////////////////////////////////////////////////// /// END OF FILE /// |