diff options
| author | Alan Mishchenko <alanmi@berkeley.edu> | 2012-09-09 15:28:31 -0700 |
|---|---|---|
| committer | Alan Mishchenko <alanmi@berkeley.edu> | 2012-09-09 15:28:31 -0700 |
| commit | 56117d56e82f816eea5e261e47b0859372219972 (patch) | |
| tree | 2196cb6c58b0e25ebe93576a4e42900992b80b69 /src/aig | |
| parent | 4333fd24d2a45a7ea6d5825306284beb8086e839 (diff) | |
| download | abc-56117d56e82f816eea5e261e47b0859372219972.tar.gz abc-56117d56e82f816eea5e261e47b0859372219972.tar.bz2 abc-56117d56e82f816eea5e261e47b0859372219972.zip | |
Added switch '-p' to '&gla -n' to use full proof for UNSAT core computation (for experiments).
Diffstat (limited to 'src/aig')
| -rw-r--r-- | src/aig/gia/gia.h | 1 | ||||
| -rw-r--r-- | src/aig/gia/giaAbsGla.c | 6 |
2 files changed, 5 insertions, 2 deletions
diff --git a/src/aig/gia/gia.h b/src/aig/gia/gia.h index eb726dc9..8a468feb 100644 --- a/src/aig/gia/gia.h +++ b/src/aig/gia/gia.h @@ -230,6 +230,7 @@ struct Gia_ParVta_t_ int fUseSkip; // skip proving intermediate timeframes int fUseSimple; // use simple CNF construction int fSkipHash; // skip hashing CNF while unrolling + int fUseFullProof; // use full proof for UNSAT cores int fDumpVabs; // dumps the abstracted model int fDumpMabs; // dumps the original AIG with abstraction map char * pFileVabs; // dumps the abstracted model into this file diff --git a/src/aig/gia/giaAbsGla.c b/src/aig/gia/giaAbsGla.c index 822a55dd..150d61e2 100644 --- a/src/aig/gia/giaAbsGla.c +++ b/src/aig/gia/giaAbsGla.c @@ -974,7 +974,8 @@ Gla_Man_t * Gla_ManStart( Gia_Man_t * pGia0, Gia_ParVta_t * pPars ) } // other p->pSat = sat_solver2_new(); -// p->pSat->pPrf1 = Vec_SetAlloc( 20 ); + if ( pPars->fUseFullProof ) + p->pSat->pPrf1 = Vec_SetAlloc( 20 ); // p->pSat->fVerbose = p->pPars->fVerbose; // sat_solver2_set_learntmax( p->pSat, pPars->nLearnedMax ); p->pSat->nLearntStart = p->pPars->nLearnedStart; @@ -1785,7 +1786,8 @@ int Gia_GlaPerform( Gia_Man_t * pAig, Gia_ParVta_t * pPars, int fStartVta ) // start incremental proof manager assert( p->pSat->pPrf2 == NULL ); - p->pSat->pPrf2 = Prf_ManAlloc(); + if ( p->pSat->pPrf1 == NULL ) + p->pSat->pPrf2 = Prf_ManAlloc(); if ( p->pSat->pPrf2 ) { p->nProofIds = 0; |