diff options
| author | Alan Mishchenko <alanmi@berkeley.edu> | 2013-02-26 15:38:37 -0500 |
|---|---|---|
| committer | Alan Mishchenko <alanmi@berkeley.edu> | 2013-02-26 15:38:37 -0500 |
| commit | 458c0538d6f52636dfceca4020adc07df0f04fab (patch) | |
| tree | 2e413809736fe654dcd755e4f61dd4307febae9e | |
| parent | a1c543c6c9162b30440a50d7cb00e35facd69e87 (diff) | |
| download | abc-458c0538d6f52636dfceca4020adc07df0f04fab.tar.gz abc-458c0538d6f52636dfceca4020adc07df0f04fab.tar.bz2 abc-458c0538d6f52636dfceca4020adc07df0f04fab.zip | |
User-controlable SAT sweeper.
| -rw-r--r-- | src/aig/gia/giaSweeper.c | 10 |
1 files changed, 8 insertions, 2 deletions
diff --git a/src/aig/gia/giaSweeper.c b/src/aig/gia/giaSweeper.c index 0b1c647a..fae5b795 100644 --- a/src/aig/gia/giaSweeper.c +++ b/src/aig/gia/giaSweeper.c @@ -623,7 +623,7 @@ static Vec_Int_t * Gia_ManGetCex( Gia_Man_t * pGia, Vec_Int_t * vId2Lit, sat_sol int Gia_SweeperCheckEquiv( Gia_Man_t * pGia, int Probe1, int Probe2 ) { Swp_Man_t * p = (Swp_Man_t *)pGia->pData; - int iLitOld, iLitNew, pLitsSat[2], RetValue, RetValue1; + int iLitOld, iLitNew, pLitsSat[2], RetValue, RetValue1, LitSat, i; clock_t clk; p->nSatCalls++; assert( p->pSat != NULL ); @@ -648,6 +648,8 @@ int Gia_SweeperCheckEquiv( Gia_Man_t * pGia, int Probe1, int Probe2 ) assert( iLitOld > iLitNew ); // if the nodes do not have SAT variables, allocate them + Vec_IntForEachEntry( p->vCondLits, LitSat, i ) + Gia_ManCnfNodeAddToSolver( p, Abc_Lit2Var(LitSat) ); Gia_ManCnfNodeAddToSolver( p, Abc_Lit2Var(iLitOld) ); Gia_ManCnfNodeAddToSolver( p, Abc_Lit2Var(iLitNew) ); sat_solver_compress( p->pSat ); @@ -751,12 +753,16 @@ p->timeSatUndec += clock() - clk; int Gia_SweeperCondCheckUnsat( Gia_Man_t * pGia ) { Swp_Man_t * p = (Swp_Man_t *)pGia->pData; - int RetValue; + int RetValue, LitSat, i; clock_t clk; p->nSatCalls++; assert( p->pSat != NULL ); p->vCexUser = NULL; + Vec_IntForEachEntry( p->vCondLits, LitSat, i ) + Gia_ManCnfNodeAddToSolver( p, Abc_Lit2Var(LitSat) ); + sat_solver_compress( p->pSat ); + clk = clock(); RetValue = sat_solver_solve( p->pSat, Vec_IntArray(p->vCondLits), Vec_IntArray(p->vCondLits) + Vec_IntSize(p->vCondLits), (ABC_INT64_T)p->nConfMax, (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0 ); |