From ae4b51351c93983a1285ce1028e3bbd90a6d5721 Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Thu, 13 Jan 2011 12:38:59 -0800 Subject: Cumulative changes in the last few weeks. --- src/opt/mfs/mfsCore.c | 12 ++++++------ src/opt/mfs/mfsGia.c | 2 +- src/opt/mfs/mfsInt.h | 7 +++++-- src/opt/mfs/mfsInter.c | 18 ++++++++++-------- src/opt/mfs/mfsMan.c | 10 ++++++---- src/opt/mfs/mfsResub.c | 44 ++++++++++++++++++++++---------------------- src/opt/mfs/mfsSat.c | 10 +++++----- src/opt/mfs/module.make | 1 - 8 files changed, 55 insertions(+), 49 deletions(-) (limited to 'src/opt/mfs') diff --git a/src/opt/mfs/mfsCore.c b/src/opt/mfs/mfsCore.c index bda95d55..72774730 100644 --- a/src/opt/mfs/mfsCore.c +++ b/src/opt/mfs/mfsCore.c @@ -268,10 +268,10 @@ clk = clock(); p->nNodesBad++; return 1; } -clk = clock(); - if ( p->pPars->fGiaSat ) - Abc_NtkMfsConstructGia( p ); -p->timeGia += clock() - clk; +//clk = clock(); +// if ( p->pPars->fGiaSat ) +// Abc_NtkMfsConstructGia( p ); +//p->timeGia += clock() - clk; // solve the SAT problem if ( p->pPars->fPower ) Abc_NtkMfsEdgePower( p, pNode ); @@ -284,8 +284,8 @@ p->timeGia += clock() - clk; Abc_NtkMfsResubNode2( p, pNode ); } p->timeSat += clock() - clk; - if ( p->pPars->fGiaSat ) - Abc_NtkMfsDeconstructGia( p ); +// if ( p->pPars->fGiaSat ) +// Abc_NtkMfsDeconstructGia( p ); return 1; } diff --git a/src/opt/mfs/mfsGia.c b/src/opt/mfs/mfsGia.c index 016b4ae2..af6cc159 100644 --- a/src/opt/mfs/mfsGia.c +++ b/src/opt/mfs/mfsGia.c @@ -271,7 +271,7 @@ int Abc_NtkMfsTryResubOnceGia( Mfs_Man_t * p, int * pCands, int nCands ) assert( Val3 == 1 ); */ // store the counter-example - Vec_IntForEachEntry( p->vProjVars, iVar, i ) + Vec_IntForEachEntry( p->vProjVarsSat, iVar, i ) { pData = (unsigned *)Vec_PtrEntry( p->vDivCexes, i ); iOut = iVar - 2 * p->pCnf->nVars; diff --git a/src/opt/mfs/mfsInt.h b/src/opt/mfs/mfsInt.h index 5611afa0..28a68bd8 100644 --- a/src/opt/mfs/mfsInt.h +++ b/src/opt/mfs/mfsInt.h @@ -61,19 +61,22 @@ struct Mfs_Man_t_ Vec_Ptr_t * vNodes; // the internal nodes of the window Vec_Ptr_t * vDivs; // the divisors of the node Vec_Int_t * vDivLits; // the SAT literals of divisor nodes - Vec_Int_t * vProjVars; // the projection variables + Vec_Int_t * vProjVarsCnf; // the projection variables + Vec_Int_t * vProjVarsSat; // the projection variables // intermediate simulation data Vec_Ptr_t * vDivCexes; // the counter-example for dividors int nDivWords; // the number of words int nCexes; // the numbe rof current counter-examples int nSatCalls; int nSatCexes; +/* // intermediate AIG data Gia_Man_t * pGia; // replica of the AIG in the new package // Gia_Obj_t ** pSat2Gia; // mapping of PO SAT var into internal GIA nodes Tas_Man_t * pTas; // the SAT solver Vec_Int_t * vCex; // the counter-example Vec_Ptr_t * vGiaLits; // literals given as assumptions +*/ // used for bidecomposition Vec_Int_t * vTruth; Bdc_Man_t * pManDec; @@ -87,7 +90,7 @@ struct Mfs_Man_t_ Int_Man_t * pMan; // interpolation manager; Vec_Int_t * vMem; // memory for intermediate SOPs Vec_Vec_t * vLevels; // levelized structure for updating - Vec_Ptr_t * vFanins; // the new set of fanins + Vec_Ptr_t * vMfsFanins; // the new set of fanins int nTotConfLim; // total conflict limit int nTotConfLevel; // total conflicts on this level // switching activity diff --git a/src/opt/mfs/mfsInter.c b/src/opt/mfs/mfsInter.c index 1b3f2415..0934513b 100644 --- a/src/opt/mfs/mfsInter.c +++ b/src/opt/mfs/mfsInter.c @@ -96,13 +96,13 @@ sat_solver * Abc_MfsCreateSolverResub( Mfs_Man_t * p, int * pCands, int nCands, Lits[0] = toLitCond( p->pCnf->pVarNums[pObjPo->Id], fInvert ); // collect the outputs of the divisors - Vec_IntClear( p->vProjVars ); + Vec_IntClear( p->vProjVarsCnf ); Vec_PtrForEachEntryStart( Aig_Obj_t *, p->pAigWin->vPos, pObjPo, i, Aig_ManPoNum(p->pAigWin) - Vec_PtrSize(p->vDivs) ) { assert( p->pCnf->pVarNums[pObjPo->Id] >= 0 ); - Vec_IntPush( p->vProjVars, p->pCnf->pVarNums[pObjPo->Id] ); + Vec_IntPush( p->vProjVarsCnf, p->pCnf->pVarNums[pObjPo->Id] ); } - assert( Vec_IntSize(p->vProjVars) == Vec_PtrSize(p->vDivs) ); + assert( Vec_IntSize(p->vProjVarsCnf) == Vec_PtrSize(p->vDivs) ); // start the solver pSat = sat_solver_new(); @@ -178,7 +178,7 @@ sat_solver * Abc_MfsCreateSolverResub( Mfs_Man_t * p, int * pCands, int nCands, // get the variable number of this divisor i = lit_var( pCands[c] ) - 2 * p->pCnf->nVars; // get the corresponding SAT variable - iVar = Vec_IntEntry( p->vProjVars, i ); + iVar = Vec_IntEntry( p->vProjVarsCnf, i ); // add the corresponding EXOR gate if ( !Abc_MfsSatAddXor( pSat, iVar, iVar + p->pCnf->nVars, 2 * p->pCnf->nVars + i ) ) { @@ -198,15 +198,17 @@ sat_solver * Abc_MfsCreateSolverResub( Mfs_Man_t * p, int * pCands, int nCands, else { // add the clauses for the EXOR gates - and remember their outputs - Vec_IntForEachEntry( p->vProjVars, iVar, i ) + Vec_IntClear( p->vProjVarsSat ); + Vec_IntForEachEntry( p->vProjVarsCnf, iVar, i ) { if ( !Abc_MfsSatAddXor( pSat, iVar, iVar + p->pCnf->nVars, 2 * p->pCnf->nVars + i ) ) { sat_solver_delete( pSat ); return NULL; } - Vec_IntWriteEntry( p->vProjVars, i, 2 * p->pCnf->nVars + i ); + Vec_IntPush( p->vProjVarsSat, 2 * p->pCnf->nVars + i ); } + assert( Vec_IntSize(p->vProjVarsCnf) == Vec_IntSize(p->vProjVarsSat) ); // simplify the solver status = sat_solver_simplify(pSat); if ( status == 0 ) @@ -259,7 +261,7 @@ unsigned * Abc_NtkMfsInterplateTruth( Mfs_Man_t * p, int * pCands, int nCands, i // get the variable number of this divisor i = lit_var( pCands[c] ) - 2 * p->pCnf->nVars; // get the corresponding SAT variable - pGloVars[c] = Vec_IntEntry( p->vProjVars, i ); + pGloVars[c] = Vec_IntEntry( p->vProjVarsCnf, i ); } // derive the interpolant @@ -362,7 +364,7 @@ Hop_Obj_t * Abc_NtkMfsInterplate( Mfs_Man_t * p, int * pCands, int nCands ) // get the variable number of this divisor i = lit_var( pCands[c] ) - 2 * p->pCnf->nVars; // get the corresponding SAT variable - pGloVars[c] = Vec_IntEntry( p->vProjVars, i ); + pGloVars[c] = Vec_IntEntry( p->vProjVarsCnf, i ); } // derive the interpolant diff --git a/src/opt/mfs/mfsMan.c b/src/opt/mfs/mfsMan.c index 74889c45..df331b43 100644 --- a/src/opt/mfs/mfsMan.c +++ b/src/opt/mfs/mfsMan.c @@ -49,14 +49,15 @@ Mfs_Man_t * Mfs_ManAlloc( Mfs_Par_t * pPars ) p = ABC_ALLOC( Mfs_Man_t, 1 ); memset( p, 0, sizeof(Mfs_Man_t) ); p->pPars = pPars; - p->vProjVars = Vec_IntAlloc( 100 ); + p->vProjVarsCnf = Vec_IntAlloc( 100 ); + p->vProjVarsSat = Vec_IntAlloc( 100 ); p->vDivLits = Vec_IntAlloc( 100 ); p->nDivWords = Aig_BitWordNum(p->pPars->nDivMax + MFS_FANIN_MAX); p->vDivCexes = Vec_PtrAllocSimInfo( p->pPars->nDivMax+MFS_FANIN_MAX+1, p->nDivWords ); p->pMan = Int_ManAlloc(); p->vMem = Vec_IntAlloc( 0 ); p->vLevels = Vec_VecStart( 32 ); - p->vFanins = Vec_PtrAlloc( 32 ); + p->vMfsFanins= Vec_PtrAlloc( 32 ); return p; } @@ -201,8 +202,9 @@ void Mfs_ManStop( Mfs_Man_t * p ) Int_ManFree( p->pMan ); Vec_IntFree( p->vMem ); Vec_VecFree( p->vLevels ); - Vec_PtrFree( p->vFanins ); - Vec_IntFree( p->vProjVars ); + Vec_PtrFree( p->vMfsFanins ); + Vec_IntFree( p->vProjVarsCnf ); + Vec_IntFree( p->vProjVarsSat ); Vec_IntFree( p->vDivLits ); Vec_PtrFree( p->vDivCexes ); ABC_FREE( p ); diff --git a/src/opt/mfs/mfsResub.c b/src/opt/mfs/mfsResub.c index 38004089..40cb6198 100644 --- a/src/opt/mfs/mfsResub.c +++ b/src/opt/mfs/mfsResub.c @@ -42,14 +42,14 @@ ABC_NAMESPACE_IMPL_START SeeAlso [] ***********************************************************************/ -void Abc_NtkMfsUpdateNetwork( Mfs_Man_t * p, Abc_Obj_t * pObj, Vec_Ptr_t * vFanins, Hop_Obj_t * pFunc ) +void Abc_NtkMfsUpdateNetwork( Mfs_Man_t * p, Abc_Obj_t * pObj, Vec_Ptr_t * vMfsFanins, Hop_Obj_t * pFunc ) { Abc_Obj_t * pObjNew, * pFanin; int k; // create the new node pObjNew = Abc_NtkCreateNode( pObj->pNtk ); pObjNew->pData = pFunc; - Vec_PtrForEachEntry( Abc_Obj_t *, vFanins, pFanin, k ) + Vec_PtrForEachEntry( Abc_Obj_t *, vMfsFanins, pFanin, k ) Abc_ObjAddFanin( pObjNew, pFanin ); // replace the old node by the new node //printf( "Replacing node " ); Abc_ObjPrint( stdout, pObj ); @@ -103,14 +103,14 @@ int Abc_NtkMfsTryResubOnce( Mfs_Man_t * p, int * pCands, int nCands ) int fVeryVerbose = 0; unsigned * pData; int RetValue, RetValue2 = -1, iVar, i, clk = clock(); - +/* if ( p->pPars->fGiaSat ) { RetValue2 = Abc_NtkMfsTryResubOnceGia( p, pCands, nCands ); p->timeGia += clock() - clk; return RetValue2; } - +*/ p->nSatCalls++; RetValue = sat_solver_solve( p->pSat, pCands, pCands + nCands, (ABC_INT64_T)p->pPars->nBTLimit, (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0 ); // assert( RetValue == l_False || RetValue == l_True ); @@ -137,7 +137,7 @@ p->timeGia += clock() - clk; printf( "S " ); p->nSatCexes++; // store the counter-example - Vec_IntForEachEntry( p->vProjVars, iVar, i ) + Vec_IntForEachEntry( p->vProjVarsSat, iVar, i ) { pData = (unsigned *)Vec_PtrEntry( p->vDivCexes, i ); if ( !sat_solver_var_value( p->pSat, iVar ) ) // remove 0s!!! @@ -186,14 +186,14 @@ int Abc_NtkMfsSolveSatResub( Mfs_Man_t * p, Abc_Obj_t * pNode, int iFanin, int f // try fanins without the critical fanin nCands = 0; - Vec_PtrClear( p->vFanins ); + Vec_PtrClear( p->vMfsFanins ); Abc_ObjForEachFanin( pNode, pFanin, i ) { if ( i == iFanin ) continue; - Vec_PtrPush( p->vFanins, pFanin ); + Vec_PtrPush( p->vMfsFanins, pFanin ); iVar = Vec_PtrSize(p->vDivs) - Abc_ObjFaninNum(pNode) + i; - pCands[nCands++] = toLitCond( Vec_IntEntry( p->vProjVars, iVar ), 1 ); + pCands[nCands++] = toLitCond( Vec_IntEntry( p->vProjVarsSat, iVar ), 1 ); } RetValue = Abc_NtkMfsTryResubOnce( p, pCands, nCands ); if ( RetValue == -1 ) @@ -212,7 +212,7 @@ clk = clock(); if ( pFunc == NULL ) return 0; // update the network - Abc_NtkMfsUpdateNetwork( p, pNode, p->vFanins, pFunc ); + Abc_NtkMfsUpdateNetwork( p, pNode, p->vMfsFanins, pFunc ); p->timeInt += clock() - clk; return 1; } @@ -269,7 +269,7 @@ p->timeInt += clock() - clk; if ( iVar == Vec_PtrSize(p->vDivs)-Abc_ObjFaninNum(pNode) ) return 0; - pCands[nCands] = toLitCond( Vec_IntEntry(p->vProjVars, iVar), 1 ); + pCands[nCands] = toLitCond( Vec_IntEntry(p->vProjVarsSat, iVar), 1 ); RetValue = Abc_NtkMfsTryResubOnce( p, pCands, nCands+1 ); if ( RetValue == -1 ) return 0; @@ -287,8 +287,8 @@ clk = clock(); if ( pFunc == NULL ) return 0; // update the network - Vec_PtrPush( p->vFanins, Vec_PtrEntry(p->vDivs, iVar) ); - Abc_NtkMfsUpdateNetwork( p, pNode, p->vFanins, pFunc ); + Vec_PtrPush( p->vMfsFanins, Vec_PtrEntry(p->vDivs, iVar) ); + Abc_NtkMfsUpdateNetwork( p, pNode, p->vMfsFanins, pFunc ); p->timeInt += clock() - clk; return 1; } @@ -334,14 +334,14 @@ int Abc_NtkMfsSolveSatResub2( Mfs_Man_t * p, Abc_Obj_t * pNode, int iFanin, int // try fanins without the critical fanin nCands = 0; - Vec_PtrClear( p->vFanins ); + Vec_PtrClear( p->vMfsFanins ); Abc_ObjForEachFanin( pNode, pFanin, i ) { if ( i == iFanin || i == iFanin2 ) continue; - Vec_PtrPush( p->vFanins, pFanin ); + Vec_PtrPush( p->vMfsFanins, pFanin ); iVar = Vec_PtrSize(p->vDivs) - Abc_ObjFaninNum(pNode) + i; - pCands[nCands++] = toLitCond( Vec_IntEntry( p->vProjVars, iVar ), 1 ); + pCands[nCands++] = toLitCond( Vec_IntEntry( p->vProjVarsSat, iVar ), 1 ); } RetValue = Abc_NtkMfsTryResubOnce( p, pCands, nCands ); if ( RetValue == -1 ) @@ -358,7 +358,7 @@ clk = clock(); if ( pFunc == NULL ) return 0; // update the network - Abc_NtkMfsUpdateNetwork( p, pNode, p->vFanins, pFunc ); + Abc_NtkMfsUpdateNetwork( p, pNode, p->vMfsFanins, pFunc ); p->timeInt += clock() - clk; return 1; } @@ -435,8 +435,8 @@ p->timeInt += clock() - clk; if ( iVar == Vec_PtrSize(p->vDivs)-Abc_ObjFaninNum(pNode) ) return 0; - pCands[nCands] = toLitCond( Vec_IntEntry(p->vProjVars, iVar2), 1 ); - pCands[nCands+1] = toLitCond( Vec_IntEntry(p->vProjVars, iVar), 1 ); + pCands[nCands] = toLitCond( Vec_IntEntry(p->vProjVarsSat, iVar2), 1 ); + pCands[nCands+1] = toLitCond( Vec_IntEntry(p->vProjVarsSat, iVar), 1 ); RetValue = Abc_NtkMfsTryResubOnce( p, pCands, nCands+2 ); if ( RetValue == -1 ) return 0; @@ -452,10 +452,10 @@ clk = clock(); if ( pFunc == NULL ) return 0; // update the network - Vec_PtrPush( p->vFanins, Vec_PtrEntry(p->vDivs, iVar2) ); - Vec_PtrPush( p->vFanins, Vec_PtrEntry(p->vDivs, iVar) ); - assert( Vec_PtrSize(p->vFanins) == nCands + 2 ); - Abc_NtkMfsUpdateNetwork( p, pNode, p->vFanins, pFunc ); + Vec_PtrPush( p->vMfsFanins, Vec_PtrEntry(p->vDivs, iVar2) ); + Vec_PtrPush( p->vMfsFanins, Vec_PtrEntry(p->vDivs, iVar) ); + assert( Vec_PtrSize(p->vMfsFanins) == nCands + 2 ); + Abc_NtkMfsUpdateNetwork( p, pNode, p->vMfsFanins, pFunc ); p->timeInt += clock() - clk; return 1; } diff --git a/src/opt/mfs/mfsSat.c b/src/opt/mfs/mfsSat.c index c5806f2a..37ee2b39 100644 --- a/src/opt/mfs/mfsSat.c +++ b/src/opt/mfs/mfsSat.c @@ -63,7 +63,7 @@ int Abc_NtkMfsSolveSat_iter( Mfs_Man_t * p ) p->nCares++; // add SAT assignment to the solver Mint = 0; - Vec_IntForEachEntry( p->vProjVars, iVar, b ) + Vec_IntForEachEntry( p->vProjVarsSat, iVar, b ) { Lits[b] = toLit( iVar ); if ( sat_solver_var_value( p->pSat, iVar ) ) @@ -75,7 +75,7 @@ int Abc_NtkMfsSolveSat_iter( Mfs_Man_t * p ) assert( !Aig_InfoHasBit(p->uCare, Mint) ); Aig_InfoSetBit( p->uCare, Mint ); // add the blocking clause - RetValue = sat_solver_addclause( p->pSat, Lits, Lits + Vec_IntSize(p->vProjVars) ); + RetValue = sat_solver_addclause( p->pSat, Lits, Lits + Vec_IntSize(p->vProjVarsSat) ); if ( RetValue == 0 ) return 0; return 1; @@ -97,15 +97,15 @@ int Abc_NtkMfsSolveSat( Mfs_Man_t * p, Abc_Obj_t * pNode ) Aig_Obj_t * pObjPo; int RetValue, i; // collect projection variables - Vec_IntClear( p->vProjVars ); + Vec_IntClear( p->vProjVarsSat ); Vec_PtrForEachEntryStart( Aig_Obj_t *, p->pAigWin->vPos, pObjPo, i, Aig_ManPoNum(p->pAigWin) - Abc_ObjFaninNum(pNode) ) { assert( p->pCnf->pVarNums[pObjPo->Id] >= 0 ); - Vec_IntPush( p->vProjVars, p->pCnf->pVarNums[pObjPo->Id] ); + Vec_IntPush( p->vProjVarsSat, p->pCnf->pVarNums[pObjPo->Id] ); } // prepare the truth table of care set - p->nFanins = Vec_IntSize( p->vProjVars ); + p->nFanins = Vec_IntSize( p->vProjVarsSat ); p->nWords = Aig_TruthWordNum( p->nFanins ); memset( p->uCare, 0, sizeof(unsigned) * p->nWords ); diff --git a/src/opt/mfs/module.make b/src/opt/mfs/module.make index bafc1ce5..544accec 100644 --- a/src/opt/mfs/module.make +++ b/src/opt/mfs/module.make @@ -1,6 +1,5 @@ SRC += src/opt/mfs/mfsCore.c \ src/opt/mfs/mfsDiv.c \ - src/opt/mfs/mfsGia.c \ src/opt/mfs/mfsInter.c \ src/opt/mfs/mfsMan.c \ src/opt/mfs/mfsResub.c \ -- cgit v1.2.3