diff options
| author | Alan Mishchenko <alanmi@berkeley.edu> | 2012-08-10 09:31:03 -0700 |
|---|---|---|
| committer | Alan Mishchenko <alanmi@berkeley.edu> | 2012-08-10 09:31:03 -0700 |
| commit | 65b652fadbd31e254eade41c32ed48b45d7aed7f (patch) | |
| tree | c7aa7c445ee2bd22ce7941138ac5c3d518dd3459 | |
| parent | 409ce39b61d774fc10c61f77c721814e597ae1f7 (diff) | |
| download | abc-65b652fadbd31e254eade41c32ed48b45d7aed7f.tar.gz abc-65b652fadbd31e254eade41c32ed48b45d7aed7f.tar.bz2 abc-65b652fadbd31e254eade41c32ed48b45d7aed7f.zip | |
Added purification of UNSAT core in &gla.
| -rw-r--r-- | src/aig/gia/giaAbsGla2.c | 44 | ||||
| -rw-r--r-- | src/misc/util/abc_global.h | 12 |
2 files changed, 49 insertions, 7 deletions
diff --git a/src/aig/gia/giaAbsGla2.c b/src/aig/gia/giaAbsGla2.c index 79bb616f..8e932cf3 100644 --- a/src/aig/gia/giaAbsGla2.c +++ b/src/aig/gia/giaAbsGla2.c @@ -1383,6 +1383,7 @@ void Gia_Ga2SendCancel( Ga2_Man_t * p, int fVerbose ) ***********************************************************************/ int Ga2_ManPerform( Gia_Man_t * pAig, Gia_ParVta_t * pPars ) { + int fUseSecondCore = 1; Ga2_Man_t * p; Vec_Int_t * vCore, * vPPis; clock_t clk2, clk = clock(); @@ -1526,7 +1527,7 @@ int Ga2_ManPerform( Gia_Man_t * pAig, Gia_ParVta_t * pPars ) goto finish; if ( p->pSat->nRuntimeLimit && clock() > p->pSat->nRuntimeLimit ) // timeout goto finish; - assert( RetValue == l_False ); +// assert( RetValue == l_False ); if ( c == 0 ) { if ( p->pPars->nFramesNoChange >= 0 ) @@ -1543,6 +1544,47 @@ int Ga2_ManPerform( Gia_Man_t * pAig, Gia_ParVta_t * pPars ) sat_solver2_rollback( p->pSat ); // reduce abstraction Ga2_ManShrinkAbs( p, nAbs, nValues, nVarsOld ); + + // purify UNSAT core + if ( fUseSecondCore ) + { + int nOldCore = Vec_IntSize(vCore); + Vec_IntSort( vCore, 0 ); +// Vec_IntPrint( vCore ); + // create bookmark to be used for rollback + assert( nVarsOld == p->pSat->size ); + sat_solver2_bookmark( p->pSat ); + // start incremental proof manager + assert( p->pSat->pPrf2 == NULL ); + p->pSat->pPrf2 = Prf_ManAlloc(); + if ( p->pSat->pPrf2 ) + { + p->nProofIds = 0; + Vec_IntFill( p->vProofIds, Gia_ManObjNum(p->pGia), -1 ); + Prf_ManRestart( p->pSat->pPrf2, p->vProofIds, sat_solver2_nlearnts(p->pSat), Vec_IntSize(vCore) ); + + Ga2_ManAddToAbs( p, vCore ); + Vec_IntFree( vCore ); +// if ( pPars->fVerbose ) +// Ga2_ManAbsPrintFrame( p, f, sat_solver2_nconflicts(p->pSat)-nConflsBeg, c+1, clock() - clk, 0 ); + } + // run SAT solver + clk2 = clock(); + Status = sat_solver2_solve( p->pSat, &Lit, &Lit+1, (ABC_INT64_T)pPars->nConfLimit, (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0 ); + assert( Status == l_False ); + p->timeUnsat += clock() - clk2; + + // derive the core + assert( p->pSat->pPrf2 != NULL ); + vCore = (Vec_Int_t *)Sat_ProofCore( p->pSat ); + Prf_ManStopP( &p->pSat->pPrf2 ); + // update the SAT solver + sat_solver2_rollback( p->pSat ); + // reduce abstraction + Ga2_ManShrinkAbs( p, nAbs, nValues, nVarsOld ); +// printf( "\n%4d -> %4d\n", nOldCore, Vec_IntSize(vCore) ); + } + Ga2_ManAddToAbs( p, vCore ); Vec_IntFree( vCore ); // verify diff --git a/src/misc/util/abc_global.h b/src/misc/util/abc_global.h index f81687a5..e4505ad5 100644 --- a/src/misc/util/abc_global.h +++ b/src/misc/util/abc_global.h @@ -296,18 +296,18 @@ static inline void Abc_PrintInt( int i ) Abc_Print( 1, " %4d", i ); else if ( v3 > -9.995 && v3 < 9.995 ) - Abc_Print( 1, "%4.2fk", v3, v3 ); + Abc_Print( 1, "%4.2fk", v3 ); else if ( v3 > -99.95 && v3 < 99.95 ) - Abc_Print( 1, "%4.1fk", v3, v3 ); + Abc_Print( 1, "%4.1fk", v3 ); else if ( v3 > -999.5 && v3 < 999.5 ) - Abc_Print( 1, "%4.0fk", v3, v3 ); + Abc_Print( 1, "%4.0fk", v3 ); else if ( v6 > -9.995 && v6 < 9.995 ) - Abc_Print( 1, "%4.2fm", v6, v6 ); + Abc_Print( 1, "%4.2fm", v6 ); else if ( v6 > -99.95 && v6 < 99.95 ) - Abc_Print( 1, "%4.1fm", v6, v6 ); + Abc_Print( 1, "%4.1fm", v6 ); else if ( v6 > -999.5 && v6 < 999.5 ) - Abc_Print( 1, "%4.0fm", v6, v6 ); + Abc_Print( 1, "%4.0fm", v6 ); } static inline void Abc_PrintTime( int level, const char * pStr, clock_t time ) |