Made abstraction and PDR communicate in-memory rather than through a file.

3 files changed, 59 insertions, 65 deletions

diff --git a/src/proof/abs/abs.h b/src/proof/abs/abs.h
index eeeda583..e7ab9e7d 100644
--- a/src/proof/abs/abs.h
+++ b/src/proof/abs/abs.h
@@ -99,6 +99,10 @@ extern int               Gia_ManPerformGla( Gia_Man_t * p, Abs_Par_t * pPars );
 extern int               Gia_ManPerformGlaOld( Gia_Man_t * p, Abs_Par_t * pPars, int fStartVta );
 /*=== 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_GlaProveCancel( int fVerbose );
+extern int               Gia_GlaProveCheck( int fVerbose );
 /*=== absVta.c =========================================================*/
 extern int               Gia_VtaPerform( Gia_Man_t * pAig, Abs_Par_t * pPars );
 /*=== absUtil.c =========================================================*/
diff --git a/src/proof/abs/absGla.c b/src/proof/abs/absGla.c
index b026c6e3..76b6c231 100644
--- a/src/proof/abs/absGla.c
+++ b/src/proof/abs/absGla.c
@@ -126,11 +126,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 int  Gia_Ga2ProveCheck( int fVerbose );
-
 ////////////////////////////////////////////////////////////////////////
 ///                     FUNCTION DEFINITIONS                         ///
 ////////////////////////////////////////////////////////////////////////
@@ -1449,7 +1444,7 @@ char * Ga2_GlaGetFileName( Ga2_Man_t * p, int fAbs )
 void Ga2_GlaDumpAbsracted( Ga2_Man_t * p, int fVerbose )
 {
     char * pFileName;
-    assert( p->pPars->fDumpMabs || p->pPars->fDumpVabs || p->pPars->fCallProver );
+    assert( p->pPars->fDumpMabs || p->pPars->fDumpVabs );
     if ( p->pPars->fDumpMabs )
     {
         pFileName = Ga2_GlaGetFileName(p, 0);
@@ -1460,7 +1455,7 @@ void Ga2_GlaDumpAbsracted( Ga2_Man_t * p, int fVerbose )
         p->pGia->vGateClasses = Ga2_ManAbsTranslate( p );
         Gia_WriteAiger( p->pGia, pFileName, 0, 0 );
     }
-    if ( p->pPars->fDumpVabs || p->pPars->fCallProver )
+    else if ( p->pPars->fDumpVabs )
     {
         Vec_Int_t * vGateClasses;
         Gia_Man_t * pAbs;
@@ -1475,6 +1470,7 @@ void Ga2_GlaDumpAbsracted( Ga2_Man_t * p, int fVerbose )
         Gia_ManStop( pAbs );
         Vec_IntFreeP( &vGateClasses );
     }
+    else assert( 0 );
 }
 
 /**Function*************************************************************
@@ -1564,7 +1560,7 @@ int Gia_ManPerformGla( Gia_Man_t * pAig, Abs_Par_t * pPars )
         Abc_Print( 1, "FrameMax = %d  ConfMax = %d  Timeout = %d  RatioMin = %d %%  RatioMax = %d %%\n", 
             pPars->nFramesMax, pPars->nConfLimit, pPars->nTimeOut, pPars->nRatioMin, pPars->nRatioMax );
         Abc_Print( 1, "LrnStart = %d  LrnDelta = %d  LrnRatio = %d %%  Skip = %d  SimpleCNF = %d  Dump = %d\n", 
-            pPars->nLearnedStart, pPars->nLearnedDelta, pPars->nLearnedPerce, pPars->fUseSkip, pPars->fUseSimple, pPars->fDumpVabs|pPars->fDumpMabs|pPars->fCallProver );
+            pPars->nLearnedStart, pPars->nLearnedDelta, pPars->nLearnedPerce, pPars->fUseSkip, pPars->fUseSimple, pPars->fDumpVabs|pPars->fDumpMabs );
         if ( pPars->fDumpVabs || pPars->fDumpMabs )
             Abc_Print( 1, "%s will be dumped into file \"%s\".\n", 
                 pPars->fDumpVabs ? "Abstracted model" : "Miter with abstraction map",
@@ -1642,7 +1638,7 @@ int Gia_ManPerformGla( Gia_Man_t * pAig, Abs_Par_t * pPars )
                     }
                     if ( iFrameTryToProve >= 0 )
                     {
-                        Gia_Ga2ProveCancel( pPars->fVerbose );
+                        Gia_GlaProveCancel( pPars->fVerbose );
                         iFrameTryToProve = -1;
                     }
 
@@ -1762,7 +1758,7 @@ int Gia_ManPerformGla( Gia_Man_t * pAig, Abs_Par_t * pPars )
             if ( pPars->fVerbose )
                 Ga2_ManAbsPrintFrame( p, f, sat_solver2_nconflicts(p->pSat)-nConflsBeg, c, clock() - clk, 1 );
             // check if abstraction was proved
-            if ( Gia_Ga2ProveCheck( pPars->fVerbose ) )
+            if ( Gia_GlaProveCheck( pPars->fVerbose ) )
             {
                 RetValue = 1;
                 goto finish;
@@ -1785,7 +1781,7 @@ int Gia_ManPerformGla( Gia_Man_t * pAig, Abs_Par_t * pPars )
             if ( p->pPars->nFramesNoChange == p->pPars->nFramesNoChangeLim )
             {
                 // dump the model into file
-                if ( p->pPars->fDumpVabs || p->pPars->fDumpMabs || p->pPars->fCallProver )
+                if ( p->pPars->fDumpVabs || p->pPars->fDumpMabs )
                 {
                     char Command[1000];
                     Abc_FrameSetStatus( -1 );
@@ -1800,9 +1796,9 @@ int Gia_ManPerformGla( Gia_Man_t * pAig, Abs_Par_t * pPars )
                 {
                     // cancel old one if it is proving
                     if ( iFrameTryToProve >= 0 )
-                        Gia_Ga2ProveCancel( pPars->fVerbose );
+                        Gia_GlaProveCancel( pPars->fVerbose );
                     // prove new one
-                    Gia_Ga2ProveAbsracted( Ga2_GlaGetFileName(p, 1), pPars->fVerbose );
+                    Gia_GlaProveAbsracted( pAig, pPars->fVerbose );
                     iFrameTryToProve = f;
                 }
                 // speak to the bridge
@@ -1832,7 +1828,7 @@ finish:
     Prf_ManStopP( &p->pSat->pPrf2 );
     // cancel old one if it is proving
     if ( iFrameTryToProve >= 0 )
-        Gia_Ga2ProveCancel( pPars->fVerbose );
+        Gia_GlaProveCancel( 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, iFrameTryToProve );
diff --git a/src/proof/abs/absPth.c b/src/proof/abs/absPth.c
index 73f76822..fb10eb81 100644
--- a/src/proof/abs/absPth.c
+++ b/src/proof/abs/absPth.c
@@ -18,16 +18,14 @@
 
 ***********************************************************************/
  
-#include "aig/ioa/ioa.h"
+#include "abs.h"
 #include "proof/pdr/pdr.h"
 
+// to compile on Linux, add -lpthread to LIBS in Makefile
+
 // uncomment this line to enable pthreads
 //#define ABC_USE_PTHREADS
 
-// to compile on Linux, modify Makefile as follows:
-// add -pthread to OPTFLAGS
-// add -lpthread to LIBS
-
 #ifdef ABC_USE_PTHREADS
 
 #ifdef WIN32
@@ -47,18 +45,18 @@ ABC_NAMESPACE_IMPL_START
 
 #ifndef ABC_USE_PTHREADS
 
-void Gia_Ga2ProveAbsracted( char * pFileName, int fVerbose ) {}
-void Gia_Ga2ProveCancel( int fVerbose )                      {}
-int  Gia_Ga2ProveCheck( int fVerbose )                       { return 0; }
+void Gia_GlaProveAbsracted( Gia_Man_t * p, int fVerbose ) {}
+void Gia_GlaProveCancel( int fVerbose )                   {}
+int  Gia_GlaProveCheck( int fVerbose )                    { return 0; }
 
 #else // pthreads are used
 
 // information given to the thread
 typedef struct Abs_ThData_t_
 {
-    char * pFileName;
-    int    fVerbose;
-    int    RunId;
+    Aig_Man_t * pAig;
+    int         fVerbose;
+    int         RunId;
 } Abs_ThData_t;
 
 // mutext to control access to shared variables
@@ -101,66 +99,62 @@ void * Abs_ProverThread( void * pArg )
 {
     Abs_ThData_t * pThData = (Abs_ThData_t *)pArg;
     Pdr_Par_t Pars, * pPars = &Pars;
-    Aig_Man_t * pAig, * pTemp;
     int RetValue, status;
-    pAig = Ioa_ReadAiger( pThData->pFileName, 0 );
-    if ( pAig == NULL )
-        Abc_Print( 1, "\nCannot open file \"%s\".\n", pThData->pFileName );
-    else
+    // call PDR
+    Pdr_ManSetDefaultParams( pPars );
+    pPars->fSilent   = 1;
+    pPars->RunId     = pThData->RunId;
+    pPars->pFuncStop = Abs_CallBackToStop;
+    RetValue = Pdr_ManSolve( pThData->pAig, pPars, NULL );
+//    RetValue = Pdr_ManSolve_test( pAig, pPars, NULL );
+    // update the result
+    if ( RetValue == 1 )
+    {
+        status = pthread_mutex_lock(&g_mutex);  assert( status == 0 );
+        g_fAbstractionProved = 1;
+        status = pthread_mutex_unlock(&g_mutex);  assert( status == 0 );
+    }
+    // quit this thread
+    if ( pThData->fVerbose )
     {
-        // synthesize abstraction
-        pAig = Aig_ManScl( pTemp = pAig, 1, 1, 0, -1, -1, 0, 0 );
-        Aig_ManStop( pTemp );
-        // call PDR
-        Pdr_ManSetDefaultParams( pPars );
-        pPars->fSilent = 1;
-        pPars->RunId = pThData->RunId;
-        pPars->pFuncStop = Abs_CallBackToStop;
-        RetValue = Pdr_ManSolve( pAig, pPars, NULL );
-//        RetValue = Pdr_ManSolve_test( pAig, pPars, NULL );
-        // update the result
         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 ( pThData->fVerbose )
-        {
-            if ( RetValue == 1 )
-                Abc_Print( 1, "\nProved abstraction %d.\n", pThData->RunId );
-            else if ( RetValue == 0 )
-                Abc_Print( 1, "\nDisproved abstraction %d.\n", pThData->RunId );
-            else if ( RetValue == -1 )
-                Abc_Print( 1, "\nCancelled abstraction %d.\n", pThData->RunId );
-            else assert( 0 );
-        }
+            Abc_Print( 1, "\nProved abstraction %d.\n", pThData->RunId );
+        else if ( RetValue == 0 )
+            Abc_Print( 1, "\nDisproved abstraction %d.\n", pThData->RunId );
+        else if ( RetValue == -1 )
+            Abc_Print( 1, "\nCancelled abstraction %d.\n", pThData->RunId );
+        else assert( 0 );
     }
-    ABC_FREE( pThData->pFileName );
+    // free memory
+    Aig_ManStop( pThData->pAig );
     ABC_FREE( pThData );
     // quit this thread
     pthread_exit( NULL );
     assert(0);
     return NULL;
 }
-void Gia_Ga2ProveAbsracted( char * pFileName, int fVerbose )
+void Gia_GlaProveAbsracted( Gia_Man_t * pGia, int fVerbose )
 {
     Abs_ThData_t * pThData;
+    Gia_Man_t * pAbs;
+    Aig_Man_t * pAig;
     pthread_t ProverThread;
     int status;
-    assert( pFileName != NULL );
     // disable verbosity
     fVerbose = 0;
+    // create abstraction 
+    assert( pGia->vGateClasses != NULL );
+    pAbs = Gia_ManDupAbsGates( pGia, pGia->vGateClasses );
+    Gia_ManCleanValue( pGia );
+    pAig = Gia_ManToAigSimple( pAbs );
+    Gia_ManStop( pAbs );
     // 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->pAig = pAig;
     pThData->fVerbose = fVerbose;
     status = pthread_mutex_lock(&g_mutex);  assert( status == 0 );
     pThData->RunId = ++g_nRunIds;
@@ -170,14 +164,14 @@ void Gia_Ga2ProveAbsracted( char * pFileName, int fVerbose )
     status = pthread_create( &ProverThread, NULL, Abs_ProverThread, pThData );
     assert( status == 0 );
 }
-void Gia_Ga2ProveCancel( int fVerbose )
+void Gia_GlaProveCancel( int fVerbose )
 {
     int status;
     status = pthread_mutex_lock(&g_mutex);  assert( status == 0 );
     g_nRunIds++;
     status = pthread_mutex_unlock(&g_mutex);  assert( status == 0 );
 }
-int Gia_Ga2ProveCheck( int fVerbose )
+int Gia_GlaProveCheck( int fVerbose )
 {
     int status;
     if ( g_fAbstractionProved == 0 )