diff options
Diffstat (limited to 'src/proof/pdr')
| -rw-r--r-- | src/proof/pdr/pdrCore.c | 195 | ||||
| -rw-r--r-- | src/proof/pdr/pdrIncr.c | 41 |
2 files changed, 226 insertions, 10 deletions
diff --git a/src/proof/pdr/pdrCore.c b/src/proof/pdr/pdrCore.c index 501f9be6..60454752 100644 --- a/src/proof/pdr/pdrCore.c +++ b/src/proof/pdr/pdrCore.c @@ -288,7 +288,7 @@ int * Pdr_ManSortByPriority( Pdr_Man_t * p, Pdr_Set_t * pCube ) best_i = i; for ( j = i+1; j < nSize; j++ ) // if ( pArray[j] < pArray[best_i] ) - if ( pPrios[pCube->Lits[pArray[j]]>>1] < pPrios[pCube->Lits[pArray[best_i]]>>1] ) + if ( pPrios[pCube->Lits[pArray[j]]>>1] < pPrios[pCube->Lits[pArray[best_i]]>>1] ) // list lower priority first (these will be removed first) best_i = j; temp = pArray[i]; pArray[i] = pArray[best_i]; @@ -488,7 +488,7 @@ int ZPdr_ManDown( Pdr_Man_t * p, int k, Pdr_Set_t ** ppCube, Pdr_Set_t * pPred, /**Function************************************************************* - Synopsis [Specialized sorting of flops based on cost.] + Synopsis [Specialized sorting of flops based on priority.] Description [] @@ -497,17 +497,171 @@ int ZPdr_ManDown( Pdr_Man_t * p, int k, Pdr_Set_t ** ppCube, Pdr_Set_t * pPred, SeeAlso [] ***********************************************************************/ -static inline void Vec_IntSelectSortCostReverseLit( int * pArray, int nSize, Vec_Int_t * vCosts ) +static inline int Vec_IntSelectSortPrioReverseLit( int * pArray, int nSize, Vec_Int_t * vPrios ) { int i, j, best_i; for ( i = 0; i < nSize-1; i++ ) { best_i = i; for ( j = i+1; j < nSize; j++ ) - if ( Vec_IntEntry(vCosts, Abc_Lit2Var(pArray[j])) > Vec_IntEntry(vCosts, Abc_Lit2Var(pArray[best_i])) ) + if ( Vec_IntEntry(vPrios, Abc_Lit2Var(pArray[j])) > Vec_IntEntry(vPrios, Abc_Lit2Var(pArray[best_i])) ) // prefer higher priority best_i = j; ABC_SWAP( int, pArray[i], pArray[best_i] ); } + return 1; +} + +/**Function************************************************************* + + Synopsis [Performs generalization using a different idea.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Pdr_ManGeneralize2( Pdr_Man_t * p, int k, Pdr_Set_t * pCube, Pdr_Set_t ** ppCubeMin ) +{ + int fUseMinAss = 0; + sat_solver * pSat = Pdr_ManFetchSolver( p, k ); + int Order = Vec_IntSelectSortPrioReverseLit( pCube->Lits, pCube->nLits, p->vPrio ); + Vec_Int_t * vLits1 = Pdr_ManCubeToLits( p, k, pCube, 1, 0 ); + int RetValue, Count = 0, iLit, Lits[2], nLits = Vec_IntSize( vLits1 ); + // create free variables + int i, iUseVar, iAndVar; + iAndVar = Pdr_ManFreeVar(p, k); + for ( i = 1; i < nLits; i++ ) + Pdr_ManFreeVar(p, k); + iUseVar = Pdr_ManFreeVar(p, k); + for ( i = 1; i < nLits; i++ ) + Pdr_ManFreeVar(p, k); + assert( iUseVar == iAndVar + nLits ); + // if there is only one positive literal, put it in front and always assume + if ( fUseMinAss ) + { + for ( i = 0; i < pCube->nLits && Count < 2; i++ ) + Count += !Abc_LitIsCompl(pCube->Lits[i]); + if ( Count == 1 ) + { + for ( i = 0; i < pCube->nLits; i++ ) + if ( !Abc_LitIsCompl(pCube->Lits[i]) ) + break; + assert( i < pCube->nLits ); + iLit = pCube->Lits[i]; + for ( ; i > 0; i-- ) + pCube->Lits[i] = pCube->Lits[i-1]; + pCube->Lits[0] = iLit; + } + } + // add clauses for the additional AND-gates + Vec_IntForEachEntry( vLits1, iLit, i ) + { + sat_solver_add_buffer_enable( pSat, iAndVar + i, Abc_Lit2Var(iLit), iUseVar + i, Abc_LitIsCompl(iLit) ); + Vec_IntWriteEntry( vLits1, i, Abc_Var2Lit(iAndVar + i, 0) ); + } + // add clauses for the additional OR-gate + RetValue = sat_solver_addclause( pSat, Vec_IntArray(vLits1), Vec_IntLimit(vLits1) ); + assert( RetValue == 1 ); + // add implications + vLits1 = Pdr_ManCubeToLits( p, k, pCube, 0, 1 ); + assert( Vec_IntSize(vLits1) == nLits ); + Vec_IntForEachEntry( vLits1, iLit, i ) + { + Lits[0] = Abc_Var2Lit(iUseVar + i, 1); + Lits[1] = iLit; + RetValue = sat_solver_addclause( pSat, Lits, Lits+2 ); + assert( RetValue == 1 ); + Vec_IntWriteEntry( vLits1, i, Abc_Var2Lit(iUseVar + i, 0) ); + } + sat_solver_compress( pSat ); + // perform minimization + if ( fUseMinAss ) + { + if ( Count == 1 ) // always assume the only positive literal + { + if ( !sat_solver_push(pSat, Vec_IntEntry(vLits1, 0)) ) // UNSAT with the first (mandatory) literal + nLits = 1; + else + nLits = 1 + sat_solver_minimize_assumptions2( pSat, Vec_IntArray(vLits1)+1, nLits-1, p->pPars->nConfLimit ); + sat_solver_pop(pSat); // unassume the first literal + } + else + nLits = sat_solver_minimize_assumptions2( pSat, Vec_IntArray(vLits1), nLits, p->pPars->nConfLimit ); + Vec_IntShrink( vLits1, nLits ); + } + else + { + // try removing one literal at a time in the old-fashioned way + int k, Entry; + Vec_Int_t * vTemp = Vec_IntAlloc( nLits ); + for ( i = nLits - 1; i >= 0; i-- ) + { + // if we are about to remove a positive lit, make sure at least one positive lit remains + if ( !Abc_LitIsCompl(Vec_IntEntry(vLits1, i)) ) + { + Vec_IntForEachEntry( vLits1, iLit, k ) + if ( iLit != -1 && k != i && !Abc_LitIsCompl(iLit) ) + break; + if ( k == Vec_IntSize(vLits1) ) // no other positive literals, except the i-th one + continue; + } + // load remaining literals + Vec_IntClear( vTemp ); + Vec_IntForEachEntry( vLits1, Entry, k ) + if ( Entry != -1 && k != i ) + Vec_IntPush( vTemp, Entry ); + else if ( Entry != -1 ) // assume opposite literal + Vec_IntPush( vTemp, Abc_LitNot(Entry) ); + // solve with assumptions + RetValue = sat_solver_solve( pSat, Vec_IntArray(vTemp), Vec_IntLimit(vTemp), p->pPars->nConfLimit, 0, 0, 0 ); + // commit the literal + if ( RetValue == l_False ) + { + int LitNot = Abc_LitNot(Vec_IntEntry(vLits1, i)); + int RetValue = sat_solver_addclause( pSat, &LitNot, &LitNot+1 ); + assert( RetValue ); + } + // update the clause + if ( RetValue == l_False ) + Vec_IntWriteEntry( vLits1, i, -1 ); + } + Vec_IntFree( vTemp ); + // compact + k = 0; + Vec_IntForEachEntry( vLits1, Entry, i ) + if ( Entry != -1 ) + Vec_IntWriteEntry( vLits1, k++, Entry ); + Vec_IntShrink( vLits1, k ); + } + // remap auxiliary literals into original literals + Vec_IntForEachEntry( vLits1, iLit, i ) + Vec_IntWriteEntry( vLits1, i, pCube->Lits[Abc_Lit2Var(iLit)-iUseVar] ); + // make sure the cube has at least one positive literal + if ( fUseMinAss ) + { + Vec_IntForEachEntry( vLits1, iLit, i ) + if ( !Abc_LitIsCompl(iLit) ) + break; + if ( i == Vec_IntSize(vLits1) ) // has no positive literals + { + // find positive lit in the cube + for ( i = 0; i < pCube->nLits; i++ ) + if ( !Abc_LitIsCompl(pCube->Lits[i]) ) + break; + assert( i < pCube->nLits ); + Vec_IntPush( vLits1, pCube->Lits[i] ); +// printf( "-" ); + } +// else +// printf( "+" ); + } + // create a subset cube + *ppCubeMin = Pdr_SetCreateSubset( pCube, Vec_IntArray(vLits1), Vec_IntSize(vLits1) ); + assert( !Pdr_SetIsInit(*ppCubeMin, -1) ); + Order = 0; + return 0; } /**Function************************************************************* @@ -532,7 +686,7 @@ int Pdr_ManGeneralize( Pdr_Man_t * p, int k, Pdr_Set_t * pCube, Pdr_Set_t ** ppP // if there is no induction, return *ppCubeMin = NULL; if ( p->pPars->fFlopOrder ) - Vec_IntSelectSortCostReverseLit( pCube->Lits, pCube->nLits, p->vPrio ); + Vec_IntSelectSortPrioReverseLit( pCube->Lits, pCube->nLits, p->vPrio ); RetValue = Pdr_ManCheckCube( p, k, pCube, ppPred, p->pPars->nConfLimit, 0, 1 ); if ( p->pPars->fFlopOrder ) Vec_IntSelectSort( pCube->Lits, pCube->nLits ); @@ -543,8 +697,6 @@ int Pdr_ManGeneralize( Pdr_Man_t * p, int k, Pdr_Set_t * pCube, Pdr_Set_t ** ppP p->tGeneral += clock() - clk; return 0; } - - keep = p->pPars->fSkipDown ? NULL : Hash_IntAlloc( 1 ); // reduce clause using assumptions // pCubeMin = Pdr_SetDup( pCube ); @@ -552,6 +704,31 @@ int Pdr_ManGeneralize( Pdr_Man_t * p, int k, Pdr_Set_t * pCube, Pdr_Set_t ** ppP if ( pCubeMin == NULL ) pCubeMin = Pdr_SetDup( pCube ); + // perform simplified generalization + if ( p->pPars->fSimpleGeneral ) + { + assert( pCubeMin->nLits > 0 ); + if ( pCubeMin->nLits > 1 ) + { + RetValue = Pdr_ManGeneralize2( p, k, pCubeMin, ppCubeMin ); + Pdr_SetDeref( pCubeMin ); + assert( ppCubeMin != NULL ); + pCubeMin = *ppCubeMin; + } + *ppCubeMin = pCubeMin; + if ( p->pPars->fVeryVerbose ) + { + printf("Cube:\n"); + for ( i = 0; i < pCubeMin->nLits; i++) + printf ("%d ", pCubeMin->Lits[i]); + printf("\n"); + } + p->tGeneral += Abc_Clock() - clk; + return 1; + } + + keep = p->pPars->fSkipDown ? NULL : Hash_IntAlloc( 1 ); + // perform generalization if ( !p->pPars->fSkipGeneral ) { @@ -691,9 +868,7 @@ int Pdr_ManGeneralize( Pdr_Man_t * p, int k, Pdr_Set_t * pCube, Pdr_Set_t ** ppP { printf("Cube:\n"); for ( i = 0; i < pCubeMin->nLits; i++) - { - printf ("%d ", pCubeMin->Lits[i]); - } + printf ("%d ", pCubeMin->Lits[i]); printf("\n"); } *ppCubeMin = pCubeMin; diff --git a/src/proof/pdr/pdrIncr.c b/src/proof/pdr/pdrIncr.c index 3fcd3d31..8ca8e29e 100644 --- a/src/proof/pdr/pdrIncr.c +++ b/src/proof/pdr/pdrIncr.c @@ -190,6 +190,21 @@ sat_solver * IPdr_ManSetSolver( Pdr_Man_t * p, int k, int nTotal ) SeeAlso [] ***********************************************************************/ + +int IPdr_ManRestoreAbsFlops( Pdr_Man_t * p ) +{ + Pdr_Set_t * pSet; int i, j, k; + + Vec_VecForEachEntry( Pdr_Set_t *, p->vClauses, pSet, i, j ) + { + for ( k = 0; k < pSet->nLits; k++ ) + { + Vec_IntWriteEntry( p->vAbsFlops, Abc_Lit2Var(pSet->Lits[k]), 1 ); + } + } + return 0; +} + int IPdr_ManRestore( Pdr_Man_t * p, Vec_Vec_t * vClauses, Vec_Int_t * vMap ) { int i; @@ -288,6 +303,17 @@ int IPdr_ManSolveInt( Pdr_Man_t * p, int fCheckClauses, int fPushClauses ) return 1; } } + + if ( p->pPars->fUseAbs && p->vAbsFlops == NULL && iFrame >= 1 ) + { + assert( p->vAbsFlops == NULL ); + p->vAbsFlops = Vec_IntStart( Saig_ManRegNum(p->pAig) ); + p->vMapFf2Ppi = Vec_IntStartFull( Saig_ManRegNum(p->pAig) ); + p->vMapPpi2Ff = Vec_IntAlloc( 100 ); + + IPdr_ManRestoreAbsFlops( p ); + } + } while ( 1 ) { @@ -442,6 +468,9 @@ int IPdr_ManSolveInt( Pdr_Man_t * p, int fCheckClauses, int fPushClauses ) break; // keep solving } p->pAig->pSeqModel = pCex; + + if ( p->pPars->fVerbose && p->pPars->fUseAbs ) + Pdr_ManPrintProgress( p, !p->pPars->fSolveAll, Abc_Clock() - clkStart ); return 0; // SAT } p->pPars->nFailOuts++; @@ -491,6 +520,7 @@ int IPdr_ManSolveInt( Pdr_Man_t * p, int fCheckClauses, int fPushClauses ) p->timeToStopOne = 0; } } + /* if ( p->pPars->fUseAbs && p->vAbsFlops && !fRefined ) { int i, Used; @@ -498,6 +528,17 @@ int IPdr_ManSolveInt( Pdr_Man_t * p, int fCheckClauses, int fPushClauses ) if ( Used && (Vec_IntEntry(p->vPrio, i) >> p->nPrioShift) == 0 ) Vec_IntWriteEntry( p->vAbsFlops, i, 0 ); } + */ + if ( p->pPars->fUseAbs && p->vAbsFlops && !fRefined ) + { + Pdr_Set_t * pSet; + int i, j, k; + Vec_IntFill( p->vAbsFlops, Vec_IntSize( p->vAbsFlops ), 0 ); + Vec_VecForEachEntry( Pdr_Set_t *, p->vClauses, pSet, i, j ) + for ( k = 0; k < pSet->nLits; k++ ) + Vec_IntWriteEntry( p->vAbsFlops, Abc_Lit2Var(pSet->Lits[k]), 1 ); + } + if ( p->pPars->fVerbose ) Pdr_ManPrintProgress( p, !fRefined, Abc_Clock() - clkStart ); if ( fRefined ) |