Enabling &gla for combinational miters.

3 files changed, 13 insertions, 22 deletions

diff --git a/src/aig/gia/giaAbsGla.c b/src/aig/gia/giaAbsGla.c
index bc9a0505..9891a904 100644
--- a/src/aig/gia/giaAbsGla.c
+++ b/src/aig/gia/giaAbsGla.c
@@ -1391,6 +1391,8 @@ Vec_Int_t * Gla_ManTranslate( Gla_Man_t * p )
     {
         nUsageCount = Vec_IntEntry(p->vCoreCounts, pObj->iGiaObj);
         assert( nUsageCount >= 0 );
+        if ( nUsageCount == 0 )
+            nUsageCount++;
         pGiaObj = Gla_ManGiaObj( p, pObj );
         if ( Gia_ObjIsConst0(pGiaObj) || Gia_ObjIsRo(p->pGia, pGiaObj) )
         {
@@ -1918,15 +1920,10 @@ int Gia_GlaPerform( Gia_Man_t * pAig, Gia_ParVta_t * pPars, int fStartVta )
             clk2 = clock();
             vCore = Gla_ManUnsatCore( p, f, p->pSat, pPars->nConfLimit, pPars->fVerbose, &Status, &nConfls );
             assert( (vCore != NULL) == (Status == 1) );
-            if ( Status == -1 ) // resource limit is reached
+            if ( Status == -1 || (p->pSat->nRuntimeLimit && clock() > p->pSat->nRuntimeLimit) ) // resource limit is reached
             {
-                Gla_ManRollBack( p );
-                goto finish;
-            }
-            // check timeout
-            if ( p->pSat->nRuntimeLimit && clock() > p->pSat->nRuntimeLimit )
-            {
-                Gla_ManRollBack( p );
+                if ( Gia_ManRegNum(p->pGia) > 1 ) // for comb cases, return the abstration
+                    Gla_ManRollBack( p );
                 goto finish;
             }
             if ( vCore != NULL )
@@ -2053,6 +2050,8 @@ int Gia_GlaPerform( Gia_Man_t * pAig, Gia_ParVta_t * pPars, int fStartVta )
     }
 finish:
     // analize the results
+    if ( p->pPars->fVerbose )
+        printf( "\n" );
     if ( pCex == NULL )
     {
         if ( pAig->vGateClasses != NULL )
diff --git a/src/aig/gia/giaAbsVta.c b/src/aig/gia/giaAbsVta.c
index 85d51a42..7d4bc65a 100644
--- a/src/aig/gia/giaAbsVta.c
+++ b/src/aig/gia/giaAbsVta.c
@@ -1698,6 +1698,8 @@ int Gia_VtaPerformInt( Gia_Man_t * pAig, Gia_ParVta_t * pPars )
     }
 finish:
     // analize the results
+    if ( p->pPars->fVerbose )
+        printf( "\n" );
     if ( pCex == NULL )
     {
         if ( Vec_PtrSize(p->vCores) == 0 )
diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c
index 006f3a55..db971203 100644
--- a/src/base/abci/abc.c
+++ b/src/base/abci/abc.c
@@ -27576,24 +27576,12 @@ int Abc_CommandAbc9GlaDerive( Abc_Frame_t * pAbc, int argc, char ** argv )
         Abc_Print( -1, "Abc_CommandAbc9GlaDerive(): There is no AIG.\n" );
         return 1;
     } 
+/*
     if ( Gia_ManRegNum(pAbc->pGia) == 0 )
     {
         Abc_Print( -1, "The network is combinational.\n" );
         return 0;
     }
-/*
-    {
-        int i;
-        assert( pAbc->pGia->vGateClasses == NULL );
-        pAbc->pGia->vGateClasses = Vec_IntStart( Gia_ManObjNum(pAbc->pGia) );
-        for ( i = 0; i < Gia_ManObjNum(pAbc->pGia); i++ )
-        {
-            if ( rand() % 3 == i % 3 )
-            {
-                Vec_IntWriteEntry( pAbc->pGia->vGateClasses, i, rand() % 5 );
-            }
-        }
-    }
 */
     if ( pAbc->pGia->vGateClasses == NULL )
     {
@@ -28174,12 +28162,14 @@ int Abc_CommandAbc9Gla( Abc_Frame_t * pAbc, int argc, char ** argv )
     {
         Abc_Print( -1, "There is no AIG.\n" );
         return 0;
-    } 
+    }
+/*    
     if ( Gia_ManRegNum(pAbc->pGia) == 0 )
     {
         Abc_Print( -1, "The network is combinational.\n" );
         return 0;
     }
+*/
     if ( Gia_ManPoNum(pAbc->pGia) > 1 )
     {
         Abc_Print( 1, "The network is more than one PO (run \"orpos\").\n" );