Prepared &gla to try abstracting and proving concurrently.

1 files changed, 78 insertions, 38 deletions

diff --git a/src/aig/gia/giaAbsGla2.c b/src/aig/gia/giaAbsGla2.c
index 9ca58bb9..55f79ac7 100644
--- a/src/aig/gia/giaAbsGla2.c
+++ b/src/aig/gia/giaAbsGla2.c
@@ -125,6 +125,12 @@ static inline int Ga2_ObjFindOrAddLit( Ga2_Man_t * p, Gia_Obj_t * pObj, int f )
     return Lit;
 }
 
+
+// calling pthreads
+extern void Gia_Ga2ProveAbsracted( char * pFileName, int fVerbose );
+extern void Gia_Ga2ProveCancel( int fVerbose );
+extern int  Gia_Ga2ProveCheck( int fVerbose );
+
 ////////////////////////////////////////////////////////////////////////
 ///                     FUNCTION DEFINITIONS                         ///
 ////////////////////////////////////////////////////////////////////////
@@ -1423,26 +1429,33 @@ char * Ga2_GlaGetFileName( Ga2_Man_t * p, int fAbs )
 
 void Ga2_GlaDumpAbsracted( Ga2_Man_t * p, int fVerbose )
 {
-//    if ( fVerbose )
-//        Abc_Print( 1, "Dumping abstracted model into file \"%s\"...\n", pFileName );
-    if ( p->pPars->fDumpVabs )
+    char * pFileName;
+    assert( p->pPars->fDumpMabs || p->pPars->fDumpVabs || p->pPars->fCallProver );
+    if ( p->pPars->fDumpMabs )
     {
+        pFileName = Ga2_GlaGetFileName(p, 0);
+        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 );
+        Gia_WriteAiger( p->pGia, pFileName, 0, 0 );
+    }
+    if ( p->pPars->fDumpVabs || p->pPars->fCallProver )
+    {
+        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 );
         // dump absracted model
-        Vec_Int_t * vGateClasses = Ga2_ManAbsTranslate( p );
-        Gia_Man_t * pAbs = Gia_ManDupAbsGates( p->pGia, vGateClasses );
+        vGateClasses = Ga2_ManAbsTranslate( p );
+        pAbs = Gia_ManDupAbsGates( p->pGia, vGateClasses );
         Gia_ManCleanValue( p->pGia );
-        Gia_WriteAiger( pAbs, Ga2_GlaGetFileName(p, 1), 0, 0 );
+        Gia_WriteAiger( pAbs, pFileName, 0, 0 );
         Gia_ManStop( pAbs );
         Vec_IntFreeP( &vGateClasses );
     }
-    else if ( p->pPars->fDumpMabs )
-    {
-        // dump abstraction map
-        Vec_IntFreeP( &p->pGia->vGateClasses );
-        p->pGia->vGateClasses = Ga2_ManAbsTranslate( p );
-        Gia_WriteAiger( p->pGia, Ga2_GlaGetFileName(p, 0), 0, 0 );
-    }
-    else assert( 0 );
 }
 
 /**Function*************************************************************
@@ -1499,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, fOneIsSent = 0;
+    int Status = l_Undef, RetValue = -1, iFrameTryProve = -1, fOneIsSent = 0;
     int i, c, f, Lit;
     // check trivial case 
     assert( Gia_ManPoNum(pAig) == 1 ); 
@@ -1618,6 +1631,11 @@ int Ga2_ManPerform( Gia_Man_t * pAig, Gia_ParVta_t * pPars )
                         Gia_Ga2SendCancel( p, pPars->fVerbose );
                         fOneIsSent = 0;
                     }
+                    if ( iFrameTryProve >= 0 )
+                    {
+                        Gia_Ga2ProveCancel( pPars->fVerbose );
+                        iFrameTryProve = -1;
+                    }
 
                     if ( c == 0 )
                     {
@@ -1723,8 +1741,16 @@ int Ga2_ManPerform( Gia_Man_t * pAig, Gia_ParVta_t * pPars )
             // print statistics
             if ( pPars->fVerbose )
                 Ga2_ManAbsPrintFrame( p, f, sat_solver2_nconflicts(p->pSat)-nConflsBeg, c, clock() - clk, 1 );
-            if ( c > 0 )
+            // check if abstraction was proved
+            if ( Gia_Ga2ProveCheck( pPars->fVerbose ) )
+            {
+                RetValue = 1;
+                goto finish;
+            }
+            if ( c > 0 ) 
             {
+                if ( p->pPars->fVeryVerbose )
+                    Abc_Print( 1, "\n" );
                 // recompute the abstraction
                 Vec_IntFreeP( &pAig->vGateClasses );
                 pAig->vGateClasses = Ga2_ManAbsTranslate( p );
@@ -1734,18 +1760,12 @@ int Ga2_ManPerform( Gia_Man_t * pAig, Gia_ParVta_t * pPars )
                     Status = l_Undef;
                     goto finish;
                 }
-                // speak to the bridge
-                if ( Abc_FrameIsBridgeMode() )
-                {
-                    // cancel old one if it was sent
-                    if ( fOneIsSent )
-                        Gia_Ga2SendCancel( p, pPars->fVerbose );
-                    // send new one 
-                    Gia_Ga2SendAbsracted( p, pPars->fVerbose );
-                    fOneIsSent = 1;
-                }
+            }
+            // check the number of stable frames
+            if ( p->pPars->nFramesNoChange == p->pPars->nFramesNoChangeLim )
+            {
                 // dump the model into file
-                if ( p->pPars->fDumpVabs || p->pPars->fDumpMabs )
+                if ( p->pPars->fDumpVabs || p->pPars->fDumpMabs || p->pPars->fCallProver )
                 {
                     char Command[1000];
                     Abc_FrameSetStatus( -1 );
@@ -1755,25 +1775,45 @@ int Ga2_ManPerform( Gia_Man_t * pAig, Gia_ParVta_t * pPars )
                     Cmd_CommandExecute( Abc_FrameGetGlobalFrame(), Command );
                     Ga2_GlaDumpAbsracted( p, pPars->fVerbose );
                 }
-                if ( p->pPars->fVeryVerbose )
-                    Abc_Print( 1, "\n" );
-                // if abstraction grew more than a certain percentage, force a restart
-                if ( pPars->nRatioMax == 0 )
-                    break;
-                if ( (f > 20 || Vec_IntSize(p->vAbs) > 100) && Vec_IntSize(p->vAbs) - nAbsOld >= nAbsOld * pPars->nRatioMax / 100 )
+                // call the prover
+                if ( p->pPars->fCallProver )
                 {
-                    if ( p->pPars->fVerbose )
-                    Abc_Print( 1, "Forcing restart because abstraction grew from %d to %d (more than %d %%).\n", 
-                        nAbsOld, Vec_IntSize(p->vAbs), pPars->nRatioMax );
-                    break;
+                    // cancel old one if it is proving
+                    if ( iFrameTryProve >= 0 )
+                        Gia_Ga2ProveCancel( pPars->fVerbose );
+                    // prove new one
+                    Gia_Ga2ProveAbsracted( Ga2_GlaGetFileName(p, 1), pPars->fVerbose );
+                    iFrameTryProve = f;
+                }
+                // speak to the bridge
+                if ( Abc_FrameIsBridgeMode() )
+                {
+                    // cancel old one if it was sent
+                    if ( fOneIsSent )
+                        Gia_Ga2SendCancel( p, pPars->fVerbose );
+                    // send new one 
+                    Gia_Ga2SendAbsracted( p, pPars->fVerbose );
+                    fOneIsSent = 1;
                 }
             }
+            // if abstraction grew more than a certain percentage, force a restart
+            if ( pPars->nRatioMax == 0 )
+                break;
+            if ( c > 0 && (f > 20 || Vec_IntSize(p->vAbs) > 100) && Vec_IntSize(p->vAbs) - nAbsOld >= nAbsOld * pPars->nRatioMax / 100 )
+            {
+                if ( p->pPars->fVerbose )
+                Abc_Print( 1, "Forcing restart because abstraction grew from %d to %d (more than %d %%).\n", 
+                    nAbsOld, Vec_IntSize(p->vAbs), pPars->nRatioMax );
+                break;
+            }
         }
     }
 finish:
     Prf_ManStopP( &p->pSat->pPrf2 );
     // analize the results
-    if ( pAig->pCexSeq == NULL )
+    if ( RetValue == 1 )
+        Abc_Print( 1, "GLA completed %d frames and proved abstraction derived in frame %d.  ", p->pPars->iFrameProved+1, iFrameTryProve );
+    else if ( pAig->pCexSeq == NULL )
     {
 //        if ( pAig->vGateClasses != NULL )
 //            Abc_Print( 1, "Replacing the old abstraction by a new one.\n" );