Added simplification before the concurrent call to PDR.

src/base/abci/abc.c

@@ -28164,7 +28164,7 @@ int Abc_CommandAbc9Gla( Abc_Frame_t * pAbc, int argc, char ** argv )
     int c, fNewAlgo = 1;
     Abs_ParSetDefaults( pPars );
     Extra_UtilGetoptReset();
-    while ( ( c = Extra_UtilGetopt( argc, argv, "FSCLDETRPBAtfardmnscbpqwvh" ) ) != EOF )
+    while ( ( c = Extra_UtilGetopt( argc, argv, "FSCLDETRPBAtfardmnscbpquwvh" ) ) != EOF )
     {
         switch ( c )
         {
@@ -28323,6 +28323,9 @@ int Abc_CommandAbc9Gla( Abc_Frame_t * pAbc, int argc, char ** argv )
         case 'q':
             pPars->fCallProver ^= 1;
             break;
+        case 'u':
+            pPars->fSimpProver ^= 1;
+            break;
         case 'v':
             pPars->fVerbose ^= 1;
             break;
@@ -28371,7 +28374,7 @@ int Abc_CommandAbc9Gla( Abc_Frame_t * pAbc, int argc, char ** argv )
     return 0;
 
 usage:
-    Abc_Print( -2, "usage: &gla [-FSCLDETRPB num] [-A file] [-fardmnscbpqwvh]\n" );
+    Abc_Print( -2, "usage: &gla [-FSCLDETRPB num] [-A file] [-fardmnscbpquwvh]\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 );
@@ -28395,6 +28398,7 @@ usage:
     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-q      : toggle calling the prover [default = %s]\n", pPars->fCallProver? "yes": "no" );
+    Abc_Print( -2, "\t-u      : toggle enabling simplifation before calling the prover [default = %s]\n", pPars->fSimpProver? "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");

src/proof/abs/abs.h

@@ -69,6 +69,7 @@ struct Abs_Par_t_
     int                  fDumpVabs;          // dumps the abstracted model
     int                  fDumpMabs;          // dumps the original AIG with abstraction map
     int                  fCallProver;        // calls the prover
+    int                  fSimpProver;        // calls simplification before prover
     char *               pFileVabs;          // dumps the abstracted model into this file
     int                  fVerbose;           // verbose flag
     int                  fVeryVerbose;       // print additional information
@@ -108,7 +109,7 @@ extern int               Gia_ManPerformGlaOld( Gia_Man_t * p, Abs_Par_t * pPars,
 /*=== absIter.c =========================================================*/
 extern Gia_Man_t *       Gia_ManShrinkGla( Gia_Man_t * p, int nFrameMax, int nTimeOut, int fUsePdr, int fUseSat, int fUseBdd, int fVerbose );
 /*=== absPth.c =========================================================*/
-extern void              Gia_GlaProveAbsracted( Gia_Man_t * p, int fVerbose );
+extern void              Gia_GlaProveAbsracted( Gia_Man_t * p, int fSimpProver, int fVerbose );
 extern void              Gia_GlaProveCancel( int fVerbose );
 extern int               Gia_GlaProveCheck( int fVerbose );
 /*=== absVta.c =========================================================*/

src/proof/abs/absGla.c

@@ -1797,7 +1797,7 @@ int Gia_ManPerformGla( Gia_Man_t * pAig, Abs_Par_t * pPars )
                     if ( iFrameTryToProve >= 0 )
                         Gia_GlaProveCancel( pPars->fVerbose );
                     // prove new one
-                    Gia_GlaProveAbsracted( pAig, pPars->fVeryVerbose );
+                    Gia_GlaProveAbsracted( pAig, pPars->fSimpProver, pPars->fVeryVerbose );
                     iFrameTryToProve = f;
                     p->nPdrCalls++;
                 }

src/proof/abs/absPth.c

@@ -46,9 +46,9 @@ ABC_NAMESPACE_IMPL_START
 
 #ifndef ABC_USE_PTHREADS
 
-void Gia_GlaProveAbsracted( Gia_Man_t * p, int fVerbose ) {}
-void Gia_GlaProveCancel( int fVerbose )                   {}
-int  Gia_GlaProveCheck( int fVerbose )                    { return 0; }
+void Gia_GlaProveAbsracted( Gia_Man_t * p, int fSimpProver, int fVerbose ) {}
+void Gia_GlaProveCancel( int fVerbose )                                    {}
+int  Gia_GlaProveCheck( int fVerbose )                                     { return 0; }
 
 #else // pthreads are used
 
@@ -134,7 +134,7 @@ void * Abs_ProverThread( void * pArg )
     assert(0);
     return NULL;
 }
-void Gia_GlaProveAbsracted( Gia_Man_t * pGia, int fVerbose )
+void Gia_GlaProveAbsracted( Gia_Man_t * pGia, int fSimpProver, int fVerbose )
 {
     extern Aig_Man_t * Dar_ManRwsat( Aig_Man_t * pAig, int fBalance, int fVerbose );
     Abs_ThData_t * pThData;
@@ -152,16 +152,19 @@ void Gia_GlaProveAbsracted( Gia_Man_t * pGia, int fVerbose )
     pAig = Gia_ManToAigSimple( pAbs );
     Gia_ManStop( pAbs );
     // simplify abstraction
-    Ssw_ManSetDefaultParams( pPars );
-    pPars->nFramesK = 4;
-    pAig = Ssw_SignalCorrespondence( pTemp = pAig, pPars );
+    if ( fSimpProver )
+    {
+        Ssw_ManSetDefaultParams( pPars );
+        pPars->nFramesK = 4;
+        pAig = Ssw_SignalCorrespondence( pTemp = pAig, pPars );
 //printf( "\n" );
 //Aig_ManPrintStats( pTemp );
 //Aig_ManPrintStats( pAig );
-    Aig_ManStop( pTemp );
+        Aig_ManStop( pTemp );
+    }
     // synthesize abstraction
-    pAig = Dar_ManRwsat( pTemp = pAig, 0, 0 ); 
-    Aig_ManStop( pTemp );
+//    pAig = Dar_ManRwsat( pTemp = pAig, 0, 0 ); 
+//    Aig_ManStop( pTemp );
     // reset the proof 
     status = pthread_mutex_lock(&g_mutex);  assert( status == 0 );
     g_fAbstractionProved = 0;