Added switch '-p' to '&gla -n' to use full proof for UNSAT core computation (for experiments).

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

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;

src/base/abci/abc.c

@@ -28342,7 +28342,7 @@ int Abc_CommandAbc9Gla( Abc_Frame_t * pAbc, int argc, char ** argv )
     int c, fStartVta = 0, fNewAlgo = 1;
     Gia_VtaSetDefaultParams( pPars );
     Extra_UtilGetoptReset();
-    while ( ( c = Extra_UtilGetopt( argc, argv, "FSCLDETRPAtrfkadmnscbwvh" ) ) != EOF )
+    while ( ( c = Extra_UtilGetopt( argc, argv, "FSCLDETRPAtrfkadmnscbpwvh" ) ) != EOF )
     {
         switch ( c )
         {
@@ -28487,6 +28487,9 @@ int Abc_CommandAbc9Gla( Abc_Frame_t * pAbc, int argc, char ** argv )
         case 'b':
             pPars->fSkipHash ^= 1;
             break;
+        case 'p':
+            pPars->fUseFullProof ^= 1;
+            break;
         case 'v':
             pPars->fVerbose ^= 1;
             break;
@@ -28535,7 +28538,7 @@ int Abc_CommandAbc9Gla( Abc_Frame_t * pAbc, int argc, char ** argv )
     return 0;
 
 usage:
-    Abc_Print( -2, "usage: &gla [-FSCLDETRP num] [-A file] [-fkadmnscbwvh]\n" );
+    Abc_Print( -2, "usage: &gla [-FSCLDETRP num] [-A file] [-fkadmnscbpwvh]\n" );
     Abc_Print( -2, "\t          fixed-time-frame gate-level proof- and cex-based abstraction\n" );
     Abc_Print( -2, "\t-F num  : the max number of timeframes to unroll [default = %d]\n", pPars->nFramesMax );
     Abc_Print( -2, "\t-S num  : the starting time frame (0=unused) [default = %d]\n", pPars->nFramesStart );
@@ -28556,6 +28559,7 @@ usage:
     Abc_Print( -2, "\t-s      : toggle skipping previously proved timeframes [default = %s]\n", pPars->fUseSkip? "yes": "no" );
     Abc_Print( -2, "\t-c      : toggle using naive (2-input AND node) CNF encoding [default = %s]\n", pPars->fUseSimple? "yes": "no" );
     Abc_Print( -2, "\t-b      : toggle CNF construction without hashing [default = %s]\n", pPars->fSkipHash? "yes": "no" );
+    Abc_Print( -2, "\t-p      : toggle using full-proof for UNSAT cores [default = %s]\n", pPars->fUseFullProof? "yes": "no" );
     Abc_Print( -2, "\t-v      : toggle printing verbose information [default = %s]\n", pPars->fVerbose? "yes": "no" );
     Abc_Print( -2, "\t-w      : toggle printing more verbose information [default = %s]\n", pPars->fVeryVerbose? "yes": "no" );
     Abc_Print( -2, "\t-h      : print the command usage\n");