From 56117d56e82f816eea5e261e47b0859372219972 Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Sun, 9 Sep 2012 15:28:31 -0700 Subject: Added switch '-p' to '&gla -n' to use full proof for UNSAT core computation (for experiments). --- src/aig/gia/gia.h | 1 + src/aig/gia/giaAbsGla.c | 6 ++++-- 2 files changed, 5 insertions(+), 2 deletions(-) (limited to 'src/aig') 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; -- cgit v1.2.3