Prepared &gla to try abstracting and proving concurrently.

2 files changed, 86 insertions, 70 deletions

diff --git a/src/aig/gia/giaAbsGla2.c b/src/aig/gia/giaAbsGla2.c
index 24ea351a..432b4f70 100644
--- a/src/aig/gia/giaAbsGla2.c
+++ b/src/aig/gia/giaAbsGla2.c
@@ -129,7 +129,6 @@ static inline int Ga2_ObjFindOrAddLit( Ga2_Man_t * p, Gia_Obj_t * pObj, int f )
 // calling pthreads
 extern void Gia_Ga2ProveAbsracted( char * pFileName, int fVerbose );
 extern void Gia_Ga2ProveCancel( int fVerbose );
-extern void Gia_Ga2ProveFinish( int fVerbose );
 extern int  Gia_Ga2ProveCheck( int fVerbose );
 
 ////////////////////////////////////////////////////////////////////////
@@ -1513,7 +1512,7 @@ int Ga2_ManPerform( Gia_Man_t * pAig, Gia_ParVta_t * pPars )
     Ga2_Man_t * p;
     Vec_Int_t * vCore, * vPPis;
     clock_t clk2, clk = clock();
-    int Status = l_Undef, RetValue = -1, iFrameTryProve = -1, fOneIsSent = 0;
+    int Status = l_Undef, RetValue = -1, iFrameTryToProve = -1, fOneIsSent = 0;
     int i, c, f, Lit;
     // check trivial case 
     assert( Gia_ManPoNum(pAig) == 1 ); 
@@ -1616,26 +1615,27 @@ int Ga2_ManPerform( Gia_Man_t * pAig, Gia_ParVta_t * pPars )
                     p->nCexes++;
                     p->timeSat += clock() - clk2;
 
-                    clk2 = clock();
-                    vPPis = Ga2_ManRefine( p );
-                    p->timeCex += clock() - clk2;
-                    if ( vPPis == NULL )
-                    {
-                        if ( pPars->fVerbose )
-                            Ga2_ManAbsPrintFrame( p, f, sat_solver2_nconflicts(p->pSat)-nConflsBeg, c, clock() - clk, 1 );
-                        goto finish;
-                    }
-
                     // cancel old one if it was sent
                     if ( Abc_FrameIsBridgeMode() && fOneIsSent )
                     {
                         Gia_Ga2SendCancel( p, pPars->fVerbose );
                         fOneIsSent = 0;
                     }
-                    if ( iFrameTryProve >= 0 )
+                    if ( iFrameTryToProve >= 0 )
                     {
                         Gia_Ga2ProveCancel( pPars->fVerbose );
-                        iFrameTryProve = -1;
+                        iFrameTryToProve = -1;
+                    }
+
+                    // perform refinement
+                    clk2 = clock();
+                    vPPis = Ga2_ManRefine( p );
+                    p->timeCex += clock() - clk2;
+                    if ( vPPis == NULL )
+                    {
+                        if ( pPars->fVerbose )
+                            Ga2_ManAbsPrintFrame( p, f, sat_solver2_nconflicts(p->pSat)-nConflsBeg, c, clock() - clk, 1 );
+                        goto finish;
                     }
 
                     if ( c == 0 )
@@ -1780,11 +1780,11 @@ int Ga2_ManPerform( Gia_Man_t * pAig, Gia_ParVta_t * pPars )
                 if ( p->pPars->fCallProver )
                 {
                     // cancel old one if it is proving
-                    if ( iFrameTryProve >= 0 )
+                    if ( iFrameTryToProve >= 0 )
                         Gia_Ga2ProveCancel( pPars->fVerbose );
                     // prove new one
                     Gia_Ga2ProveAbsracted( Ga2_GlaGetFileName(p, 1), pPars->fVerbose );
-                    iFrameTryProve = f;
+                    iFrameTryToProve = f;
                 }
                 // speak to the bridge
                 if ( Abc_FrameIsBridgeMode() )
@@ -1812,12 +1812,11 @@ int Ga2_ManPerform( Gia_Man_t * pAig, Gia_ParVta_t * pPars )
 finish:
     Prf_ManStopP( &p->pSat->pPrf2 );
     // cancel old one if it is proving
-    if ( iFrameTryProve >= 0 )
+    if ( iFrameTryToProve >= 0 )
         Gia_Ga2ProveCancel( pPars->fVerbose );
-    Gia_Ga2ProveFinish( pPars->fVerbose );
     // analize the results
     if ( RetValue == 1 )
-        Abc_Print( 1, "GLA completed %d frames and proved abstraction derived in frame %d.  ", p->pPars->iFrameProved+1, iFrameTryProve );
+        Abc_Print( 1, "GLA completed %d frames and proved abstraction derived in frame %d.  ", p->pPars->iFrameProved+1, iFrameTryToProve );
     else if ( pAig->pCexSeq == NULL )
     {
 //        if ( pAig->vGateClasses != NULL )
diff --git a/src/aig/gia/giaAbsPth.c b/src/aig/gia/giaAbsPth.c
index 12abf1d4..e0069132 100644
--- a/src/aig/gia/giaAbsPth.c
+++ b/src/aig/gia/giaAbsPth.c
@@ -22,7 +22,7 @@
 #include "proof/pdr/pdr.h"
 
 // comment this out to disable pthreads
-//#define ABC_USE_PTHREADS
+#define ABC_USE_PTHREADS
 
 #ifdef ABC_USE_PTHREADS
 
@@ -41,43 +41,31 @@ ABC_NAMESPACE_IMPL_START
 ///                        DECLARATIONS                              ///
 ////////////////////////////////////////////////////////////////////////
 
-////////////////////////////////////////////////////////////////////////
-///                     FUNCTION DEFINITIONS                         ///
-////////////////////////////////////////////////////////////////////////
-
-/**Function*************************************************************
-
-  Synopsis    [Start and stop proving abstracted model.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
 #ifndef ABC_USE_PTHREADS
 
 void Gia_Ga2ProveAbsracted( char * pFileName, int fVerbose ) {}
 void Gia_Ga2ProveCancel( int fVerbose )                      {}
-void Gia_Ga2ProveFinish( int fVerbose )                      {}
 int  Gia_Ga2ProveCheck( int fVerbose )                       { return 0; }
 
 #else // pthreads are used
 
 // information given to the thread
-typedef struct Abs_Pair_t_
+typedef struct Abs_ThData_t_
 {
     char * pFileName;
     int    fVerbose;
     int    RunId;
-} Abs_Pair_t;
+} Abs_ThData_t;
 
-// the last valid thread
-static int g_nRunIds = 0;
-int Abs_CallBackToStop( int RunId ) { assert( RunId <= g_nRunIds ); return RunId < g_nRunIds; }
+// mutext to control access to shared variables
+pthread_mutex_t g_mutex = PTHREAD_MUTEX_INITIALIZER;
+static volatile int g_nRunIds = 0;             // the number of the last prover instance
+static volatile int g_fAbstractionProved = 0;  // set to 1 when prover successed to prove
 
+// call back procedure for PDR
+int Abs_CallBackToStop( int RunId ) { assert( RunId <= g_nRunIds ); return RunId < g_nRunIds; }
 
+// test procedure to replace PDR
 int Pdr_ManSolve_test( Aig_Man_t * pAig, Pdr_Par_t * pPars, Abc_Cex_t ** ppCex )
 {
     char * p = ABC_ALLOC( char, 111 );
@@ -90,16 +78,30 @@ int Pdr_ManSolve_test( Aig_Man_t * pAig, Pdr_Par_t * pPars, Abc_Cex_t ** ppCex )
     return -1;
 }
 
-static int g_fAbstractionProved = 0;
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    [Create one thread]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
 void * Abs_ProverThread( void * pArg )
 {
-    Abs_Pair_t * pPair = (Abs_Pair_t *)pArg;
+    Abs_ThData_t * pThData = (Abs_ThData_t *)pArg;
     Pdr_Par_t Pars, * pPars = &Pars;
     Aig_Man_t * pAig, * pTemp;
-    int RetValue;
-    pAig = Ioa_ReadAiger( pPair->pFileName, 0 );
+    int RetValue, status;
+    pAig = Ioa_ReadAiger( pThData->pFileName, 0 );
     if ( pAig == NULL )
-        Abc_Print( 1, "\nCannot open file \"%s\".\n", pPair->pFileName );
+        Abc_Print( 1, "\nCannot open file \"%s\".\n", pThData->pFileName );
     else
     {
         // synthesize abstraction
@@ -108,28 +110,33 @@ void * Abs_ProverThread( void * pArg )
         // call PDR
         Pdr_ManSetDefaultParams( pPars );
         pPars->fSilent = 1;
-        pPars->RunId = pPair->RunId;
+        pPars->RunId = pThData->RunId;
         pPars->pFuncStop = Abs_CallBackToStop;
         RetValue = Pdr_ManSolve( pAig, pPars, NULL );
 //        RetValue = Pdr_ManSolve_test( pAig, pPars, NULL );
         // update the result
-        g_fAbstractionProved = (RetValue == 1);
+        if ( RetValue == 1 )
+        {
+            status = pthread_mutex_lock(&g_mutex);  assert( status == 0 );
+            g_fAbstractionProved = 1;
+            status = pthread_mutex_unlock(&g_mutex);  assert( status == 0 );
+        }
         // free memory
         Aig_ManStop( pAig );
         // quit this thread
-        if ( pPair->fVerbose )
+        if ( pThData->fVerbose )
         {
             if ( RetValue == 1 )
-                Abc_Print( 1, "\nProved abstraction %d.\n", pPair->RunId );
+                Abc_Print( 1, "\nProved abstraction %d.\n", pThData->RunId );
             else if ( RetValue == 0 )
-                Abc_Print( 1, "\nDisproved abstraction %d.\n", pPair->RunId );
+                Abc_Print( 1, "\nDisproved abstraction %d.\n", pThData->RunId );
             else if ( RetValue == -1 )
-                Abc_Print( 1, "\nCancelled abstraction %d.\n", pPair->RunId );
+                Abc_Print( 1, "\nCancelled abstraction %d.\n", pThData->RunId );
             else assert( 0 );
         }
     }
-    ABC_FREE( pPair->pFileName );
-    ABC_FREE( pPair );
+    ABC_FREE( pThData->pFileName );
+    ABC_FREE( pThData );
     // quit this thread
     pthread_exit( NULL );
     assert(0);
@@ -137,38 +144,48 @@ void * Abs_ProverThread( void * pArg )
 }
 void Gia_Ga2ProveAbsracted( char * pFileName, int fVerbose )
 {
-    Abs_Pair_t * pPair;
+    Abs_ThData_t * pThData;
     pthread_t ProverThread;
-    int RetValue;
+    int status;
     assert( pFileName != NULL );
-    g_fAbstractionProved = 0;
     // disable verbosity
     fVerbose = 0;
+    // reset the proof 
+    status = pthread_mutex_lock(&g_mutex);  assert( status == 0 );
+    g_fAbstractionProved = 0;
+    status = pthread_mutex_unlock(&g_mutex);  assert( status == 0 );
+    // collect thread data
+    pThData = ABC_CALLOC( Abs_ThData_t, 1 );
+    pThData->pFileName = Abc_UtilStrsav( (void *)pFileName );
+    pThData->fVerbose = fVerbose;
+    status = pthread_mutex_lock(&g_mutex);  assert( status == 0 );
+    pThData->RunId = ++g_nRunIds;
+    status = pthread_mutex_unlock(&g_mutex);  assert( status == 0 );
     // create thread
-    pPair = ABC_CALLOC( Abs_Pair_t, 1 );
-    pPair->pFileName = Abc_UtilStrsav( (void *)pFileName );
-    pPair->fVerbose = fVerbose;
-    pPair->RunId = ++g_nRunIds;
-    if ( fVerbose )  Abc_Print( 1, "\nTrying to prove abstraction %d.\n", pPair->RunId );
-    RetValue = pthread_create( &ProverThread, NULL, Abs_ProverThread, pPair );
-    assert( RetValue == 0 );
+    if ( fVerbose )  Abc_Print( 1, "\nTrying to prove abstraction %d.\n", pThData->RunId );
+    status = pthread_create( &ProverThread, NULL, Abs_ProverThread, pThData );
+    assert( status == 0 );
 }
 void Gia_Ga2ProveCancel( int fVerbose )
 {
+    int status;
+    status = pthread_mutex_lock(&g_mutex);  assert( status == 0 );
     g_nRunIds++;
-}
-void Gia_Ga2ProveFinish( int fVerbose )
-{
-    g_fAbstractionProved = 0;
+    status = pthread_mutex_unlock(&g_mutex);  assert( status == 0 );
 }
 int Gia_Ga2ProveCheck( int fVerbose )
 {
-    return g_fAbstractionProved;
+    int status;
+    if ( g_fAbstractionProved == 0 )
+        return 0;
+    status = pthread_mutex_lock(&g_mutex);  assert( status == 0 );
+    g_fAbstractionProved = 0;
+    status = pthread_mutex_unlock(&g_mutex);  assert( status == 0 );
+    return 1;
 }
 
 #endif
 
-
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////