diff options
Diffstat (limited to 'src/opt')
| -rw-r--r-- | src/opt/lpk/lpkCore.c | 2 | ||||
| -rw-r--r-- | src/opt/mfs/mfsInter.c | 11 | ||||
| -rw-r--r-- | src/opt/mfs/mfsResub.c | 19 |
3 files changed, 16 insertions, 16 deletions
diff --git a/src/opt/lpk/lpkCore.c b/src/opt/lpk/lpkCore.c index e819a7fb..34911c20 100644 --- a/src/opt/lpk/lpkCore.c +++ b/src/opt/lpk/lpkCore.c @@ -340,7 +340,7 @@ void Lpk_ComputeSupports( Lpk_Man_t * p, Lpk_Cut_t * pCut, unsigned * pTruth ) pTruthInv = Lpk_CutTruth( p, pCut, 1 ); RetValue1 = Kit_CreateCloudFromTruth( p->pDsdMan->dd, pTruth, pCut->nLeaves, p->vBddDir ); RetValue2 = Kit_CreateCloudFromTruth( p->pDsdMan->dd, pTruthInv, pCut->nLeaves, p->vBddInv ); - if ( RetValue1 && RetValue2 ) + if ( RetValue1 && RetValue2 && Vec_IntSize(p->vBddDir) > 1 && Vec_IntSize(p->vBddInv) > 1 ) Kit_TruthCofSupports( p->vBddDir, p->vBddInv, pCut->nLeaves, p->vMemory, p->puSupps ); else p->puSupps[0] = p->puSupps[1] = 0; diff --git a/src/opt/mfs/mfsInter.c b/src/opt/mfs/mfsInter.c index 16db5061..65acd4eb 100644 --- a/src/opt/mfs/mfsInter.c +++ b/src/opt/mfs/mfsInter.c @@ -220,6 +220,7 @@ Hop_Obj_t * Abc_NtkMfsInterplate( Mfs_Man_t * p, int * pCands, int nCands ) Kit_Graph_t * pGraph; Hop_Obj_t * pFunc; int nFanins, status; + int c, i, * pGloVars; // derive the SAT solver for interpolation pSat = Abc_MfsCreateSolverResub( p, pCands, nCands ); @@ -235,6 +236,16 @@ Hop_Obj_t * Abc_NtkMfsInterplate( Mfs_Man_t * p, int * pCands, int nCands ) pCnf = sat_solver_store_release( pSat ); sat_solver_delete( pSat ); + // set the global variables + pGloVars = Int_ManSetGlobalVars( p->pMan, nCands ); + for ( c = 0; c < nCands; c++ ) + { + // 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 ); + } + // derive the interpolant nFanins = Int_ManInterpolate( p->pMan, pCnf, 0, &puTruth ); Sto_ManFree( pCnf ); diff --git a/src/opt/mfs/mfsResub.c b/src/opt/mfs/mfsResub.c index 1e9da4d2..4171c111 100644 --- a/src/opt/mfs/mfsResub.c +++ b/src/opt/mfs/mfsResub.c @@ -235,12 +235,8 @@ p->timeInt += clock() - clk; clk = clock(); // derive the function pFunc = Abc_NtkMfsInterplate( p, pCands, nCands+1 ); - // shift fanins by 1 - for ( i = Vec_PtrSize(p->vFanins); i > 0; i-- ) - p->vFanins->pArray[i] = p->vFanins->pArray[i-1]; - p->vFanins->nSize++; - Vec_PtrWriteEntry( p->vFanins, 0, Vec_PtrEntry(p->vDivs, iVar) ); // update the network + Vec_PtrPush( p->vFanins, Vec_PtrEntry(p->vDivs, iVar) ); Abc_NtkMfsUpdateNetwork( p, pNode, p->vFanins, pFunc ); p->timeInt += clock() - clk; return 1; @@ -372,17 +368,10 @@ p->timeInt += clock() - clk; clk = clock(); // derive the function pFunc = Abc_NtkMfsInterplate( p, pCands, nCands+2 ); - // shift fanins by 1 - for ( i = Vec_PtrSize(p->vFanins); i > 0; i-- ) - p->vFanins->pArray[i] = p->vFanins->pArray[i-1]; - p->vFanins->nSize++; - // shift fanins by 1 - for ( i = Vec_PtrSize(p->vFanins); i > 0; i-- ) - p->vFanins->pArray[i] = p->vFanins->pArray[i-1]; - p->vFanins->nSize++; - Vec_PtrWriteEntry( p->vFanins, 0, Vec_PtrEntry(p->vDivs, iVar2) ); - Vec_PtrWriteEntry( p->vFanins, 1, Vec_PtrEntry(p->vDivs, iVar) ); // 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 ); p->timeInt += clock() - clk; return 1; |