Prepared &gla to try abstracting and proving concurrently.

5 files changed, 166 insertions, 46 deletions

diff --git a/src/aig/gia/giaAbsGla2.c b/src/aig/gia/giaAbsGla2.c
index 55f79ac7..24ea351a 100644
--- a/src/aig/gia/giaAbsGla2.c
+++ b/src/aig/gia/giaAbsGla2.c
@@ -129,6 +129,7 @@ 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 );
 
 ////////////////////////////////////////////////////////////////////////
@@ -1434,8 +1435,8 @@ void Ga2_GlaDumpAbsracted( Ga2_Man_t * p, int fVerbose )
     if ( p->pPars->fDumpMabs )
     {
         pFileName = Ga2_GlaGetFileName(p, 0);
-        if ( fVerbose )
-            Abc_Print( 1, "Dumping miter with abstraction map into file \"%s\"...\n", pFileName );
+//        if ( fVerbose )
+//            Abc_Print( 1, "Dumping miter with abstraction map into file \"%s\"...\n", pFileName );
         // dump abstraction map
         Vec_IntFreeP( &p->pGia->vGateClasses );
         p->pGia->vGateClasses = Ga2_ManAbsTranslate( p );
@@ -1446,8 +1447,8 @@ void Ga2_GlaDumpAbsracted( Ga2_Man_t * p, int fVerbose )
         Vec_Int_t * vGateClasses;
         Gia_Man_t * pAbs;
         pFileName = Ga2_GlaGetFileName(p, 1);
-        if ( fVerbose )
-            Abc_Print( 1, "Dumping abstracted model into file \"%s\"...\n", pFileName );
+//        if ( fVerbose )
+//            Abc_Print( 1, "Dumping abstracted model into file \"%s\"...\n", pFileName );
         // dump absracted model
         vGateClasses = Ga2_ManAbsTranslate( p );
         pAbs = Gia_ManDupAbsGates( p->pGia, vGateClasses );
@@ -1545,7 +1546,7 @@ int Ga2_ManPerform( Gia_Man_t * pAig, Gia_ParVta_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->nLearnedStart, pPars->nLearnedDelta, pPars->nLearnedPerce, pPars->fUseSkip, pPars->fUseSimple, pPars->fDumpVabs|pPars->fDumpMabs|pPars->fCallProver );
         if ( pPars->fDumpVabs || pPars->fDumpMabs )
             Abc_Print( 1, "%s will be dumped into file \"%s\".\n", 
                 pPars->fDumpVabs ? "Abstracted model" : "Miter with abstraction map",
@@ -1810,6 +1811,10 @@ 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 )
+        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 );
diff --git a/src/aig/gia/giaAbsPth.c b/src/aig/gia/giaAbsPth.c
index 31f63674..c69f3891 100644
--- a/src/aig/gia/giaAbsPth.c
+++ b/src/aig/gia/giaAbsPth.c
@@ -18,10 +18,11 @@
 
 ***********************************************************************/
  
-#include "gia.h"
+#include "aig/ioa/ioa.h"
+#include "proof/pdr/pdr.h"
 
 // comment this out to disable pthreads
-//#define ABC_USE_PTHREADS
+#define ABC_USE_PTHREADS
 
 #ifdef ABC_USE_PTHREADS
 
@@ -34,7 +35,7 @@
 
 #endif
 
-ABC_NAMESPACE_IMPL_START
+ABC_NAMESPACE_IMPL_START 
 
 ////////////////////////////////////////////////////////////////////////
 ///                        DECLARATIONS                              ///
@@ -59,21 +60,110 @@ ABC_NAMESPACE_IMPL_START
 
 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_
+{
+    char * pFileName;
+    int    fVerbose;
+    int    RunId;
+} Abs_Pair_t;
+
+// the last valid thread
+static int g_nRunIds = 0;
+int Abs_CallBackToStop( int RunId ) { assert( RunId <= g_nRunIds ); return RunId < g_nRunIds; }
+
+
+int Pdr_ManSolve_test( Aig_Man_t * pAig, Pdr_Par_t * pPars, Abc_Cex_t ** ppCex )
+{
+    char * p = ABC_ALLOC( char, 111 );
+    while ( 1 )
+    {
+        if ( pPars->pFuncStop && pPars->pFuncStop(pPars->RunId) )
+            break;
+    }
+    ABC_FREE( p );
+    return -1;
+}
+
+static int g_fAbstractionProved = 0;
+void * Abs_ProverThread( void * pArg )
+{
+    Abs_Pair_t * pPair = (Abs_Pair_t *)pArg;
+    Pdr_Par_t Pars, * pPars = &Pars;
+    Aig_Man_t * pAig, * pTemp;
+    int RetValue;
+    pAig = Ioa_ReadAiger( pPair->pFileName, 0 );
+    if ( pAig == NULL )
+        Abc_Print( 1, "\nCannot open file \"%s\".\n", pPair->pFileName );
+    else
+    {
+        // 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 = pPair->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);
+        // free memory
+        Aig_ManStop( pAig );
+        // quit this thread
+        if ( pPair->fVerbose )
+        {
+            if ( RetValue == 1 )
+                Abc_Print( 1, "\nProved abstraction %d.\n", pPair->RunId );
+            else if ( RetValue == 0 )
+                Abc_Print( 1, "\nDisproved abstraction %d.\n", pPair->RunId );
+            else if ( RetValue == -1 )
+                Abc_Print( 1, "\nCancelled abstraction %d.\n", pPair->RunId );
+            else assert( 0 );
+        }
+    }
+    ABC_FREE( pPair->pFileName );
+    ABC_FREE( pPair );
+    // quit this thread
+    pthread_exit( NULL );
+    assert(0);
+    return NULL;
+}
 void Gia_Ga2ProveAbsracted( char * pFileName, int fVerbose )
 {
-    Abc_Print( 1, "Trying to prove abstraction.\n" );
+    Abs_Pair_t * pPair;
+    pthread_t ProverThread;
+    int RetValue;
+    assert( pFileName != NULL );
+    g_fAbstractionProved = 0;
+    // disable verbosity
+    fVerbose = 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 );
 }
 void Gia_Ga2ProveCancel( int fVerbose )
 {
-    Abc_Print( 1, "Canceling attempt to prove abstraction.\n" );
+    g_nRunIds++;
+}
+void Gia_Ga2ProveFinish( int fVerbose )
+{
+    g_fAbstractionProved = 0;
 }
 int Gia_Ga2ProveCheck( int fVerbose )
 {
-    return 0;
+    return g_fAbstractionProved;
 }
 
 #endif
diff --git a/src/base/abci/abcDar.c b/src/base/abci/abcDar.c
index 85377956..8278fa16 100644
--- a/src/base/abci/abcDar.c
+++ b/src/base/abci/abcDar.c
@@ -2577,15 +2577,18 @@ int Abc_NtkDarPdr( Abc_Ntk_t * pNtk, Pdr_Par_t * pPars, Abc_Cex_t ** ppCex )
     else
         RetValue = Pdr_ManSolve( pMan, pPars, ppCex );
     // output the result
-    if ( RetValue == 1 )
-        Abc_Print( 1, "Property proved.  " );
-    else if ( RetValue == 0 )
-        Abc_Print( 1, "Output %d of miter \"%s\" was asserted in frame %d.  ", (*ppCex)->iPo, pNtk->pName, ppCex? (*ppCex)->iFrame : -1 );
-    else if ( RetValue == -1 )
-        Abc_Print( 1, "Property UNDECIDED.  " );
-    else
-        assert( 0 );
-ABC_PRT( "Time", clock() - clk );
+    if ( !pPars->fSilent )
+    {
+        if ( RetValue == 1 )
+            Abc_Print( 1, "Property proved.  " );
+        else if ( RetValue == 0 )
+            Abc_Print( 1, "Output %d of miter \"%s\" was asserted in frame %d.  ", (*ppCex)->iPo, pNtk->pName, ppCex? (*ppCex)->iFrame : -1 );
+        else if ( RetValue == -1 )
+            Abc_Print( 1, "Property UNDECIDED.  " );
+        else
+            assert( 0 );
+    ABC_PRT( "Time", clock() - clk );
+    }
 
     if ( *ppCex && !Saig_ManVerifyCex( pMan, *ppCex ) )
         Abc_Print( 1, "Abc_NtkDarPdr(): Counter-example verification has FAILED.\n" );
diff --git a/src/proof/pdr/pdr.h b/src/proof/pdr/pdr.h
index d245b467..491477dd 100644
--- a/src/proof/pdr/pdr.h
+++ b/src/proof/pdr/pdr.h
@@ -40,20 +40,23 @@ ABC_NAMESPACE_HEADER_START
 typedef struct Pdr_Par_t_ Pdr_Par_t;
 struct Pdr_Par_t_
 {
-    int iOutput;      // zero-based number of primary output to solve
-    int nRecycle;     // limit on vars for recycling
-    int nFrameMax;    // limit on frame count
-    int nConfLimit;   // limit on SAT solver conflicts
-    int nRestLimit;   // limit on the number of proof-obligations
-    int nTimeOut;     // timeout in seconds
-    int fTwoRounds;   // use two rounds for generalization
-    int fMonoCnf;     // monolythic CNF
-    int fDumpInv;     // dump inductive invariant
-    int fShortest;    // forces bug traces to be shortest
-    int fSkipGeneral; // skips expensive generalization step
-    int fVerbose;     // verbose output
-    int fVeryVerbose; // very verbose output
-    int iFrame;       // explored up to this frame
+    int iOutput;          // zero-based number of primary output to solve
+    int nRecycle;         // limit on vars for recycling
+    int nFrameMax;        // limit on frame count
+    int nConfLimit;       // limit on SAT solver conflicts
+    int nRestLimit;       // limit on the number of proof-obligations
+    int nTimeOut;         // timeout in seconds
+    int fTwoRounds;       // use two rounds for generalization
+    int fMonoCnf;         // monolythic CNF
+    int fDumpInv;         // dump inductive invariant
+    int fShortest;        // forces bug traces to be shortest
+    int fSkipGeneral;     // skips expensive generalization step
+    int fVerbose;         // verbose output`
+    int fVeryVerbose;     // very verbose output
+    int fSilent;          // totally silent execution
+    int iFrame;           // explored up to this frame
+    int RunId;            // PDR id in this run 
+    int(*pFuncStop)(int); // callback to terminate
 };
 
 ////////////////////////////////////////////////////////////////////////
@@ -65,8 +68,8 @@ struct Pdr_Par_t_
 ////////////////////////////////////////////////////////////////////////
 
 /*=== pdrCore.c ==========================================================*/
-extern void            Pdr_ManSetDefaultParams( Pdr_Par_t * pPars );
-extern int             Pdr_ManSolve( Aig_Man_t * p, Pdr_Par_t * pPars, Abc_Cex_t ** ppCex );
+extern void               Pdr_ManSetDefaultParams( Pdr_Par_t * pPars );
+extern int                Pdr_ManSolve( Aig_Man_t * p, Pdr_Par_t * pPars, Abc_Cex_t ** ppCex );
 
 
 ABC_NAMESPACE_HEADER_END
diff --git a/src/proof/pdr/pdrCore.c b/src/proof/pdr/pdrCore.c
index 765894e3..5cb05143 100644
--- a/src/proof/pdr/pdrCore.c
+++ b/src/proof/pdr/pdrCore.c
@@ -528,7 +528,9 @@ int Pdr_ManBlockCube( Pdr_Man_t * p, Pdr_Set_t * pCube )
             Pdr_QueuePush( p, pThis );
         }
 
-        // check the timeout
+        // check termination
+        if ( p->pPars->pFuncStop && p->pPars->pFuncStop(p->pPars->RunId) )
+            return -1;
         if ( p->timeToStop && clock() > p->timeToStop )
             return -1;
     }
@@ -565,7 +567,10 @@ int Pdr_ManSolveInt( Pdr_Man_t * p )
         {
             if ( p->pPars->fVerbose ) 
                 Pdr_ManPrintProgress( p, 1, clock() - clkStart );
-            Abc_Print( 1, "Reached conflict limit (%d).\n",  p->pPars->nConfLimit );
+                if ( p->pPars->nConfLimit )
+                    Abc_Print( 1, "Reached conflict limit (%d).\n",  p->pPars->nConfLimit );
+                else if ( p->pPars->fVerbose ) 
+                    Abc_Print( 1, "Computation cancelled by the callback.\n" );
             p->pPars->iFrame = k;
             return -1;
         }
@@ -576,7 +581,10 @@ int Pdr_ManSolveInt( Pdr_Man_t * p )
             {
                 if ( p->pPars->fVerbose ) 
                     Pdr_ManPrintProgress( p, 1, clock() - clkStart );
-                Abc_Print( 1, "Reached conflict limit (%d).\n",  p->pPars->nConfLimit );
+                if ( p->pPars->nConfLimit )
+                    Abc_Print( 1, "Reached conflict limit (%d).\n",  p->pPars->nConfLimit );
+                else if ( p->pPars->fVerbose ) 
+                    Abc_Print( 1, "Computation cancelled by the callback.\n" );
                 p->pPars->iFrame = k;
                 return -1;
             }
@@ -615,7 +623,8 @@ int Pdr_ManSolveInt( Pdr_Man_t * p )
             {
                 if ( p->pPars->fVerbose ) 
                     Pdr_ManPrintProgress( p, 1, clock() - clkStart );
-                Abc_Print( 1, "Reached conflict limit (%d).\n",  p->pPars->nConfLimit );
+                if ( !p->pPars->fSilent )
+                    Abc_Print( 1, "Reached conflict limit (%d).\n",  p->pPars->nConfLimit );
                 p->pPars->iFrame = k;
                 return -1;
             }
@@ -623,8 +632,10 @@ int Pdr_ManSolveInt( Pdr_Man_t * p )
             {
                 if ( p->pPars->fVerbose ) 
                     Pdr_ManPrintProgress( p, 1, clock() - clkStart );
-                Pdr_ManReportInvariant( p );
-                Pdr_ManVerifyInvariant( p );
+                if ( !p->pPars->fSilent )
+                    Pdr_ManReportInvariant( p );
+                if ( !p->pPars->fSilent )
+                    Pdr_ManVerifyInvariant( p );
                 p->pPars->iFrame = k;
                 return 1; // UNSAT
             }
@@ -633,7 +644,12 @@ int Pdr_ManSolveInt( Pdr_Man_t * p )
 //            clkStart = clock();
         }
 
-        // check the timeout
+        // check termination
+        if ( p->pPars->pFuncStop && p->pPars->pFuncStop(p->pPars->RunId) )
+        {
+            p->pPars->iFrame = k;
+            return -1;
+        }
         if ( p->timeToStop && clock() > p->timeToStop )
         {
             if ( fPrintClauses )
@@ -643,7 +659,8 @@ int Pdr_ManSolveInt( Pdr_Man_t * p )
             }
             if ( p->pPars->fVerbose ) 
                 Pdr_ManPrintProgress( p, 1, clock() - clkStart );
-            Abc_Print( 1, "Reached timeout (%d seconds).\n",  p->pPars->nTimeOut );
+            if ( !p->pPars->fSilent )
+                Abc_Print( 1, "Reached timeout (%d seconds).\n",  p->pPars->nTimeOut );
             p->pPars->iFrame = k;
             return -1;
         }
@@ -651,7 +668,8 @@ int Pdr_ManSolveInt( Pdr_Man_t * p )
         {
             if ( p->pPars->fVerbose ) 
                 Pdr_ManPrintProgress( p, 1, clock() - clkStart );
-            Abc_Print( 1, "Reached limit on the number of timeframes (%d).\n", p->pPars->nFrameMax );
+            if ( !p->pPars->fSilent )
+                Abc_Print( 1, "Reached limit on the number of timeframes (%d).\n", p->pPars->nFrameMax );
             p->pPars->iFrame = k;
             return -1;
         } 
@@ -677,7 +695,8 @@ int Pdr_ManSolve_( Aig_Man_t * pAig, Pdr_Par_t * pPars, Vec_Int_t ** pvPrioInit,
     clock_t clk = clock();
     p = Pdr_ManStart( pAig, pPars, pvPrioInit? *pvPrioInit : NULL );
     RetValue = Pdr_ManSolveInt( p );
-    *ppCex = RetValue ? NULL : Pdr_ManDeriveCex( p );
+    if ( ppCex )
+        *ppCex = RetValue ? NULL : Pdr_ManDeriveCex( p );
     if ( p->pPars->fDumpInv )
         Pdr_ManDumpClauses( p, (char *)"inv.pla", RetValue==1 );
 //    if ( *ppCex && pPars->fVerbose )