1 files changed, 45 insertions, 51 deletions

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 )