Making GLA PBA and GLA CBA communicate information.

3 files changed, 14 insertions, 12 deletions

diff --git a/src/aig/gia/giaAbs.c b/src/aig/gia/giaAbs.c
index ab964c51..165bc996 100644
--- a/src/aig/gia/giaAbs.c
+++ b/src/aig/gia/giaAbs.c
@@ -484,8 +484,11 @@ int Gia_ManGlaPbaPerform( Gia_Man_t * pGia, void * pPars )
         pGia->vGateClasses = vGateClasses;
     }
     // clean up the abstraction map
-    pGiaAbs = Gia_ManDupAbsGates( pGia, pGia->vGateClasses );
-    Gia_ManStop( pGiaAbs );
+    if ( pGia->vGateClasses )
+    {
+        pGiaAbs = Gia_ManDupAbsGates( pGia, pGia->vGateClasses );
+        Gia_ManStop( pGiaAbs );
+    }
     if ( p->fVerbose )
         Gia_ManPrintStats( pGia, 0 );
     return 1;
diff --git a/src/aig/saig/saigGlaPba.c b/src/aig/saig/saigGlaPba.c
index fce2372f..50f6fce8 100644
--- a/src/aig/saig/saigGlaPba.c
+++ b/src/aig/saig/saigGlaPba.c
@@ -579,7 +579,7 @@ Vec_Int_t * Aig_Gla2ManPerform( Aig_Man_t * pAig, int nStart, int nFramesMax, in
         return NULL;
     }
     sat_solver_set_random( p->pSat, fSkipRand );
-    p->timePre += Abc_Clock(1,0);
+    p->timePre += (Abc_Clock(1,0)/ABC_CPS)*CLOCKS_PER_SEC;
 
     // set runtime limit
     if ( TimeLimit )
@@ -593,8 +593,8 @@ Vec_Int_t * Aig_Gla2ManPerform( Aig_Man_t * pAig, int nStart, int nFramesMax, in
         Aig_Gla2ManStop( p );
         return NULL;
     }
-    p->timeSat += Abc_Clock(1,0);
-    p->timeTotal = Abc_Clock(0,0);
+    p->timeSat += (Abc_Clock(1,0)/ABC_CPS)*CLOCKS_PER_SEC;
+    p->timeTotal = (Abc_Clock(0,0)/ABC_CPS)*CLOCKS_PER_SEC;
 
     // print stats
     if ( fVerbose )
diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c
index 81b82f73..32ed17eb 100644
--- a/src/base/abci/abc.c
+++ b/src/base/abci/abc.c
@@ -28952,8 +28952,8 @@ int Abc_CommandAbc9GlaCba( Abc_Frame_t * pAbc, int argc, char ** argv )
     Saig_ParBmc_t Pars, * pPars = &Pars;
     int c, fNaiveCnf = 0;
     Saig_ParBmcSetDefaultParams( pPars );
-    pPars->nStart     =  0;  // (pAbc->nFrames >= 0) ? pAbc->nFrames : 0;
-    pPars->nFramesMax =  0;  // pPars->nStart + 10;
+    pPars->nStart     =  (pAbc->nFrames >= 0) ? pAbc->nFrames : 0;
+    pPars->nFramesMax =  0;  
     pPars->nConfLimit =  0;
     pPars->nTimeOut   = 60;
     Extra_UtilGetoptReset();
@@ -29054,10 +29054,9 @@ int Abc_CommandAbc9GlaCba( Abc_Frame_t * pAbc, int argc, char ** argv )
         return 0;
     }
     pAbc->Status = Gia_ManGlaCbaPerform( pAbc->pGia, pPars, fNaiveCnf );
-    if ( pPars->nStart == 0 )
+//    if ( pPars->nStart == 0 )
        pAbc->nFrames = pPars->iFrame;
     Abc_FrameReplaceCex( pAbc, &pAbc->pGia->pCexSeq );
-//    printf( "This command is currently not enabled.\n" );
     return 0;
 
 usage:
@@ -29090,8 +29089,8 @@ int Abc_CommandAbc9GlaPba( Abc_Frame_t * pAbc, int argc, char ** argv )
     Saig_ParBmc_t Pars, * pPars = &Pars;
     int c;
     Saig_ParBmcSetDefaultParams( pPars );
-    pPars->nStart     =  0;  //(pAbc->nFrames >= 0) ? pAbc->nFrames : 0;
-    pPars->nFramesMax = 10; //pPars->nStart + 10;
+    pPars->nStart     =  0;  
+    pPars->nFramesMax = (pAbc->nFrames >= 0) ? pAbc->nFrames : 10;
     pPars->nConfLimit =  0;
     pPars->fSkipRand  =  0;
     Extra_UtilGetoptReset();
@@ -29183,7 +29182,7 @@ int Abc_CommandAbc9GlaPba( Abc_Frame_t * pAbc, int argc, char ** argv )
     if ( pPars->nStart )
         Abc_Print( 0, "The starting frame is specified. The resulting abstraction may be unsound.\n" );
     pAbc->Status = Gia_ManGlaPbaPerform( pAbc->pGia, pPars );
-    if ( pPars->nStart == 0 )
+//    if ( pPars->nStart == 0 )
        pAbc->nFrames = pPars->iFrame;
     Abc_FrameReplaceCex( pAbc, &pAbc->pGia->pCexSeq );
     return 0;