Fixed &gla to work in the bridge mode.

2 files changed, 76 insertions, 29 deletions

diff --git a/src/aig/gia/giaAbsGla.c b/src/aig/gia/giaAbsGla.c
index 970ff26b..efccaae9 100644
--- a/src/aig/gia/giaAbsGla.c
+++ b/src/aig/gia/giaAbsGla.c
@@ -1678,6 +1678,42 @@ void Gla_ManReportMemory( Gla_Man_t * p )
   SeeAlso     []
 
 ***********************************************************************/
+void Gia_GlaSendAbsracted( Gla_Man_t * p, int fVerbose )
+{
+    extern int Gia_ManToBridgeAbsNetlist( FILE * pFile, Gia_Man_t * p );
+    Gia_Man_t * pAbs;
+    Vec_Int_t * vGateClasses;
+    assert( Abc_FrameIsBridgeMode() );
+//    if ( fVerbose )
+//        Abc_Print( 1, "Sending abstracted model...\n" );
+    // create abstraction
+    vGateClasses = Gla_ManTranslate( p );
+    pAbs = Gia_ManDupAbsGates( p->pGia0, vGateClasses );
+    Vec_IntFreeP( &vGateClasses );
+    // send it out
+    Gia_ManToBridgeAbsNetlist( stdout, pAbs );
+    Gia_ManStop( pAbs );
+}
+void Gia_GlaSendCancel( Gla_Man_t * p, int fVerbose )
+{
+    extern int Gia_ManToBridgeBadAbs( FILE * pFile );
+    assert( Abc_FrameIsBridgeMode() );
+//    if ( fVerbose )
+//        Abc_Print( 1, "Cancelling previously sent model...\n" );
+    Gia_ManToBridgeBadAbs( stdout );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Send abstracted model or send cancel.]
+
+  Description [Counter-example will be sent automatically when &vta terminates.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
 void Gia_GlaDumpAbsracted( Gla_Man_t * p, int fVerbose )
 {
     char * pFileName = p->pPars->pFileVabs ? p->pPars->pFileVabs : "glabs.aig";
@@ -1685,8 +1721,6 @@ void Gia_GlaDumpAbsracted( Gla_Man_t * p, int fVerbose )
     Vec_Int_t * vGateClasses;
     if ( fVerbose )
         Abc_Print( 1, "Dumping abstracted model into file \"%s\"...\n", pFileName );
-//    if ( !Abc_FrameIsBridgeMode() )
-//        return;
     // create abstraction
     vGateClasses = Gla_ManTranslate( p );
     pAbs = Gia_ManDupAbsGates( p->pGia0, vGateClasses );
@@ -1714,7 +1748,7 @@ int Gia_GlaPerform( Gia_Man_t * pAig, Gia_ParVta_t * pPars, int fStartVta )
     Gla_Man_t * p;
     Vec_Int_t * vCore, * vPPis;
     Abc_Cex_t * pCex = NULL;
-    int i, f, nConfls, Status, nCoreSize, RetValue = -1;
+    int f, i, iPrev, nConfls, Status, nCoreSize, fOneIsSent = 0, RetValue = -1;
     int clk = clock(), clk2;
     // preconditions
     assert( Gia_ManPoNum(pAig) == 1 );
@@ -1769,7 +1803,7 @@ int Gia_GlaPerform( Gia_Man_t * pAig, Gia_ParVta_t * pPars, int fStartVta )
             pPars->nFramesMax, pPars->nConfLimit, pPars->nLearntMax, pPars->nTimeOut, pPars->nRatioMin );
         Abc_Print( 1, "Frame   %%   Abs  PPI   FF   LUT   Confl  Cex    SatVar   Core     Time\n" );
     }
-    for ( f = i = 0; !p->pPars->nFramesMax || f < p->pPars->nFramesMax; f++ )
+    for ( f = i = iPrev = 0; !p->pPars->nFramesMax || f < p->pPars->nFramesMax; f++, iPrev = i )
     {
         int nConflsBeg = sat_solver2_nconflicts(p->pSat);
         p->pPars->iFrame = f;
@@ -1807,6 +1841,14 @@ int Gia_GlaPerform( Gia_Man_t * pAig, Gia_ParVta_t * pPars, int fStartVta )
             p->timeSat += clock() - clk2;
             assert( Status == 0 );
             p->nCexes++;
+
+            // cancel old one if it was sent
+            if ( Abc_FrameIsBridgeMode() && fOneIsSent )
+            {
+                Gia_GlaSendCancel( p, pPars->fVerbose );
+                fOneIsSent = 0;
+            }
+
             // perform the refinement
             clk2 = clock();
             if ( pPars->fAddLayer )
@@ -1876,13 +1918,26 @@ int Gia_GlaPerform( Gia_Man_t * pAig, Gia_ParVta_t * pPars, int fStartVta )
         if ( p->pPars->fVerbose )
         Gla_ManAbsPrintFrame( p, nCoreSize, f+1, sat_solver2_nconflicts(p->pSat)-nConflsBeg, i, clock() - clk );
 
-        // dump the model
-        if ( p->pPars->fDumpVabs && (f & 1) )
+        if ( f > 2 && iPrev > 0 && i == 0 ) // change has happened
         {
-            Abc_FrameSetCex( NULL );
-            Abc_FrameSetNFrames( f+1 );
-            Cmd_CommandExecute( Abc_FrameGetGlobalFrame(), "write_status gla.status" );
-            Gia_GlaDumpAbsracted( p, pPars->fVerbose );
+            if ( Abc_FrameIsBridgeMode() )
+            {
+                // cancel old one if it was sent
+                if ( fOneIsSent )
+                    Gia_GlaSendCancel( p, pPars->fVerbose );
+                // send new one 
+                Gia_GlaSendAbsracted( p, pPars->fVerbose );
+                fOneIsSent = 1;
+            }
+
+            // dump the model into file
+            if ( p->pPars->fDumpVabs )
+            {
+                Abc_FrameSetCex( NULL );
+                Abc_FrameSetNFrames( f+1 );
+                Cmd_CommandExecute( Abc_FrameGetGlobalFrame(), "write_status gla.status" );
+                Gia_GlaDumpAbsracted( p, pPars->fVerbose );
+            }
         }
 
         // check if the number of objects is below limit
diff --git a/src/aig/gia/giaAbsVta.c b/src/aig/gia/giaAbsVta.c
index 91e609c5..00d239f3 100644
--- a/src/aig/gia/giaAbsVta.c
+++ b/src/aig/gia/giaAbsVta.c
@@ -1433,10 +1433,9 @@ void Gia_VtaSendAbsracted( Vta_Man_t * p, int fVerbose )
 {
     extern int Gia_ManToBridgeAbsNetlist( FILE * pFile, Gia_Man_t * p );
     Gia_Man_t * pAbs;
+    assert( Abc_FrameIsBridgeMode() );
 //    if ( fVerbose )
 //        Abc_Print( 1, "Sending abstracted model...\n" );
-    if ( !Abc_FrameIsBridgeMode() )
-        return;
     // create obj classes
     Vec_IntFreeP( &p->pGia->vObjClasses );
     p->pGia->vObjClasses = Gia_VtaFramesToAbs( (Vec_Vec_t *)p->vCores );
@@ -1454,10 +1453,9 @@ void Gia_VtaSendAbsracted( Vta_Man_t * p, int fVerbose )
 void Gia_VtaSendCancel( Vta_Man_t * p, int fVerbose )
 {
     extern int Gia_ManToBridgeBadAbs( FILE * pFile );
+    assert( Abc_FrameIsBridgeMode() );
 //    if ( fVerbose )
 //        Abc_Print( 1, "Cancelling previously sent model...\n" );
-    if ( !Abc_FrameIsBridgeMode() )
-        return;
     Gia_ManToBridgeBadAbs( stdout );
 }
 
@@ -1478,8 +1476,6 @@ void Gia_VtaDumpAbsracted( Vta_Man_t * p, int fVerbose )
     Gia_Man_t * pAbs;
     if ( fVerbose )
         Abc_Print( 1, "Dumping abstracted model into file \"%s\"...\n", pFileName );
-//    if ( !Abc_FrameIsBridgeMode() )
-//        return;
     // create obj classes
     Vec_IntFreeP( &p->pGia->vObjClasses );
     p->pGia->vObjClasses = Gia_VtaFramesToAbs( (Vec_Vec_t *)p->vCores );
@@ -1674,22 +1670,18 @@ int Gia_VtaPerformInt( Gia_Man_t * pAig, Gia_ParVta_t * pPars )
         {
             // reset the counter of frames without change
             nCountNoChange = 1;
-            // cancel old one if it was sent
-//            if ( fOneIsSent )
-//                Gia_VtaSendCancel( p, pPars->fVerbose );
-//            fOneIsSent = 0;
         }
         else if ( ++nCountNoChange == 2 ) // time to send
         {
-            // cancel old one if it was sent
-            if ( fOneIsSent )
-                Gia_VtaSendCancel( p, pPars->fVerbose );
-            // send new one 
-            Gia_VtaSendAbsracted( p, pPars->fVerbose );
-            fOneIsSent = 1;
-            // dump the model
-//            if ( p->pPars->fDumpVabs )
-//                Gia_VtaDumpAbsracted( p, pPars->fVerbose );
+            if ( Abc_FrameIsBridgeMode() )
+            {
+                // cancel old one if it was sent
+                if ( fOneIsSent )
+                    Gia_VtaSendCancel( p, pPars->fVerbose );
+                // send new one 
+                Gia_VtaSendAbsracted( p, pPars->fVerbose );
+                fOneIsSent = 1;
+            }
         }
         // dump the model
         if ( p->pPars->fDumpVabs && (f & 1) )