Bug fix in &gla -d.

2 files changed, 22 insertions, 14 deletions

diff --git a/src/aig/gia/giaAbsGla.c b/src/aig/gia/giaAbsGla.c
index 893f4f3e..1732c92e 100644
--- a/src/aig/gia/giaAbsGla.c
+++ b/src/aig/gia/giaAbsGla.c
@@ -57,6 +57,7 @@ struct Gla_Man_t_
     Gia_ParVta_t* pPars;           // parameters
     // internal data
     Vec_Int_t *   vAbs;            // abstracted objects
+    Gla_Obj_t *   pObjRoot;        // the primary output
     Gla_Obj_t *   pObjs;           // objects
     int           nObjs;           // the number of objects
     int           nAbsOld;         // previous abstraction
@@ -340,6 +341,7 @@ Gla_Man_t * Gla_ManStart( Gia_Man_t * pGia, Gia_ParVta_t * pPars )
         pGla->Fanins[0] = Gia_ObjFanin0( Gia_ObjRoToRi(p->pGia, pObj) )->Value;
         pGla->fCompl0   = Gia_ObjFaninC0( Gia_ObjRoToRi(p->pGia, pObj) );
     }
+    p->pObjRoot = Gla_ManObj( p, Gia_ManPo(p->pGia, 0)->Value );
     // abstraction 
     assert( pGia->vGateClasses != NULL );
     Gla_ManForEachObj( p, pGla )
@@ -667,12 +669,10 @@ void Gla_ManRollBack( Gla_Man_t * p )
 ***********************************************************************/
 int Gla_ManGetOutLit( Gla_Man_t * p, int f )
 {
-    Gia_Obj_t * pObj   = Gia_ManPo(p->pGia, 0);
-    Gia_Obj_t * pFanin = Gia_ObjFanin0(pObj);
-    Gla_Obj_t * pGla   = Gla_ManObj(p, pFanin->Value);
-    int iSat = Vec_IntEntry( &pGla->vFrames, f );
+    Gla_Obj_t * pFanin = Gla_ManObj( p, p->pObjRoot->Fanins[0] );
+    int iSat = Vec_IntEntry( &pFanin->vFrames, f );
     assert( iSat > 0 );
-    return Abc_Var2Lit( iSat, Gia_ObjFaninC0(pObj) );
+    return Abc_Var2Lit( iSat, p->pObjRoot->fCompl0 );
 }
 Vec_Int_t * Gla_ManUnsatCore( Gla_Man_t * p, int f, Vec_Int_t * vCla2Obj, sat_solver2 * pSat, int nConfMax, int fVerbose, int * piRetValue, int * pnConfls )
 {
@@ -799,17 +799,16 @@ void Gia_GlaDumpAbsracted( Gla_Man_t * p, int fVerbose )
 {
     char * pFileName = p->pPars->pFileVabs ? p->pPars->pFileVabs : "glabs.aig";
     Gia_Man_t * pAbs;
+    Vec_Int_t * vGateClasses;
     if ( fVerbose )
         Abc_Print( 1, "Dumping abstracted model into file \"%s\"...\n", pFileName );
 //    if ( !Abc_FrameIsBridgeMode() )
 //        return;
-    // create gate classes
-    Vec_IntFreeP( &p->pGia->vGateClasses );
-    p->pGia->vGateClasses = Gla_ManTranslate( p );
-    // create abstrated model
-    pAbs = Gia_ManDupAbsGates( p->pGia, p->pGia->vGateClasses );
-    Vec_IntFreeP( &p->pGia->vGateClasses );
-    // send it out
+    // create abstraction
+    vGateClasses = Gla_ManTranslate( p );
+    pAbs = Gia_ManDupAbsGates( p->pGia, vGateClasses );
+    Vec_IntFreeP( &vGateClasses );
+    // write into file
     Gia_WriteAiger( pAbs, pFileName, 0, 0 );
     Gia_ManStop( pAbs );
 }
@@ -843,19 +842,22 @@ int Gia_GlaPerform( Gia_Man_t * pAig, Gia_ParVta_t * pPars )
         int nFramesMaxOld   = pPars->nFramesMax;
         int nFramesStartOld = pPars->nFramesStart;
         int nTimeOutOld     = pPars->nTimeOut;
+        int nDumpOld        = pPars->fDumpVabs;
         pPars->nFramesMax   = pPars->nFramesStart;
         pPars->nFramesStart = Abc_MinInt( pPars->nFramesStart/2 + 1, 3 );
-        pPars->nTimeOut     = 10;
+        pPars->nTimeOut     = 15;
+        pPars->fDumpVabs    = 0;
         RetValue = Gia_VtaPerformInt( pAig, pPars );
         pPars->nFramesMax   = nFramesMaxOld;
         pPars->nFramesStart = nFramesStartOld;
         pPars->nTimeOut     = nTimeOutOld;
+        pPars->fDumpVabs    = nDumpOld;
         // create gate classes
         Vec_IntFreeP( &pAig->vGateClasses );
         pAig->vGateClasses = Gia_VtaConvertToGla( pAig, pAig->vObjClasses );
         Vec_IntFreeP( &pAig->vObjClasses );
     }
-    if ( RetValue == 0 )
+    if ( RetValue == 0 || pAig->vGateClasses == NULL )
         return RetValue;
     // start the manager
     clk = clock();
@@ -893,7 +895,10 @@ int Gia_GlaPerform( Gia_Man_t * pAig, Gia_ParVta_t * pPars )
             vCore = Gla_ManUnsatCore( p, f, p->vCla2Obj, p->pSat, pPars->nConfLimit, pPars->fVerbose, &Status, &nConfls );
             assert( (vCore != NULL) == (Status == 1) );
             if ( Status == -1 ) // resource limit is reached
+            {
+                Gla_ManRollBack( p );
                 goto finish;
+            }
             if ( vCore != NULL )
             {
                 p->timeUnsat += clock() - clk2;
diff --git a/src/aig/gia/giaAbsVta.c b/src/aig/gia/giaAbsVta.c
index 3195c160..7e4288fc 100644
--- a/src/aig/gia/giaAbsVta.c
+++ b/src/aig/gia/giaAbsVta.c
@@ -1531,7 +1531,10 @@ int Gia_VtaPerformInt( Gia_Man_t * pAig, Gia_ParVta_t * pPars )
                 vCore = Vta_ManUnsatCore( Vga_ManGetOutLit(p, f), p->vCla2Var, p->pSat, pPars->nConfLimit, pPars->fVerbose, &Status, &nConfls );
                 assert( (vCore != NULL) == (Status == 1) );
                 if ( Status == -1 ) // resource limit is reached
+                {
+                    Vga_ManRollBack( p, nObjOld );
                     goto finish;
+                }
                 if ( vCore != NULL )
                 {
                     p->timeUnsat += clock() - clk2;