Bug fix in &vta.

3 files changed, 69 insertions, 45 deletions

diff --git a/src/aig/gia/giaAbsGla.c b/src/aig/gia/giaAbsGla.c
index 18ef8942..6f3731a1 100644
--- a/src/aig/gia/giaAbsGla.c
+++ b/src/aig/gia/giaAbsGla.c
@@ -855,7 +855,7 @@ int Gia_GlaPerform( Gia_Man_t * pAig, Gia_ParVta_t * pPars )
         int nDumpOld        = pPars->fDumpVabs;
         pPars->nFramesMax   = pPars->nFramesStart;
         pPars->nFramesStart = Abc_MinInt( pPars->nFramesStart/2 + 1, 3 );
-        pPars->nTimeOut     = 15;
+        pPars->nTimeOut     = 20;
         pPars->fDumpVabs    = 0;
         RetValue = Gia_VtaPerformInt( pAig, pPars );
         pPars->nFramesMax   = nFramesMaxOld;
diff --git a/src/aig/gia/giaAbsVta.c b/src/aig/gia/giaAbsVta.c
index 24856d17..9a9dc56f 100644
--- a/src/aig/gia/giaAbsVta.c
+++ b/src/aig/gia/giaAbsVta.c
@@ -1056,6 +1056,27 @@ void Vga_ManStop( Vta_Man_t * p )
 
 /**Function*************************************************************
 
+  Synopsis    [Returns the output literal.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline int Vga_ManGetOutLit( Vta_Man_t * p, int f )
+{
+    Gia_Obj_t * pObj = Gia_ManPo(p->pGia, 0);
+    Vta_Obj_t * pThis = Vga_ManFind( p, Gia_ObjFaninId0p(p->pGia, pObj), f );
+    assert( pThis != NULL && pThis->fAdded );
+    if ( f == 0 && Gia_ObjIsRo(p->pGia, Gia_ObjFanin0(pObj)) && !Gia_ObjFaninC0(pObj) )
+        return -Vta_ObjId(p, pThis);
+    return Abc_Var2Lit( Vta_ObjId(p, pThis), Gia_ObjFaninC0(pObj) );
+}
+
+/**Function*************************************************************
+
   Synopsis    [Finds the set of clauses involved in the UNSAT core.]
 
   Description []
@@ -1073,6 +1094,14 @@ Vec_Int_t * Vta_ManUnsatCore( int iLit, Vec_Int_t * vCla2Var, sat_solver2 * pSat
     int nConfPrev = pSat->stats.conflicts;
     if ( piRetValue )
         *piRetValue = 1;
+    // consider special case when PO points to the flop
+    // this leads to immediate conflict in the first timeframe
+    if ( iLit < 0 )
+    {
+        vCore = Vec_IntAlloc( 1 );
+        Vec_IntPush( vCore, -iLit );
+        return vCore;
+    }
     // solve the problem
     RetValue = sat_solver2_solve( pSat, &iLit, &iLit+1, (ABC_INT64_T)nConfMax, (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0 );
     if ( pnConfls )
@@ -1318,25 +1347,6 @@ void Vga_ManLoadSlice( Vta_Man_t * p, Vec_Int_t * vOne, int Lift )
 
 /**Function*************************************************************
 
-  Synopsis    [Returns the output literal.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-static inline int Vga_ManGetOutLit( Vta_Man_t * p, int f )
-{
-    Gia_Obj_t * pObj = Gia_ManPo(p->pGia, 0);
-    Vta_Obj_t * pThis = Vga_ManFind( p, Gia_ObjFaninId0p(p->pGia, pObj), f );
-    assert( pThis != NULL && pThis->fAdded );
-    return Abc_Var2Lit( Vta_ObjId(p, pThis), Gia_ObjFaninC0(pObj) );
-}
-
-/**Function*************************************************************
-
   Synopsis    []
 
   Description []
@@ -1464,6 +1474,42 @@ void Gia_VtaDumpAbsracted( Vta_Man_t * p, int fVerbose )
     Gia_ManStop( pAbs );
 }
 
+    
+/**Function*************************************************************
+
+  Synopsis    [Print memory report.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Gia_VtaPrintMemory( Vta_Man_t * p )
+{
+    double memTot = 0;
+    double memAig = Gia_ManObjNum(p->pGia) * sizeof(Gia_Obj_t);
+    double memSat = sat_solver2_memory( p->pSat );
+    double memPro = sat_solver2_memory_proof( p->pSat );
+    double memMap = p->nObjsAlloc * sizeof(Vta_Obj_t) + p->nBins * sizeof(int);
+    double memOth = sizeof(Vta_Man_t);
+    memOth += Vec_IntCap(p->vOrder) * sizeof(int);
+    memOth += Vec_VecMemoryInt( (Vec_Vec_t *)p->vFrames );
+    memOth += Vec_BitCap(p->vSeenGla) * sizeof(int);
+    memOth += Vec_IntCap(p->vCla2Var) * sizeof(int);
+    memOth += Vec_VecMemoryInt( (Vec_Vec_t *)p->vCores );
+    memOth += Vec_IntCap(p->vAddedNew) * sizeof(int);
+    memTot = memAig + memSat + memPro + memMap + memOth;
+    ABC_PRMP( "Memory: AIG  ", memAig, memTot );
+    ABC_PRMP( "Memory: SAT  ", memSat, memTot );
+    ABC_PRMP( "Memory: Proof", memPro, memTot );
+    ABC_PRMP( "Memory: Map  ", memMap, memTot );
+    ABC_PRMP( "Memory: Other", memOth, memTot );
+    ABC_PRMP( "Memory: TOTAL", memTot, memTot );
+}
+
+
 /**Function*************************************************************
 
   Synopsis    [Collect nodes/flops involved in different timeframes.]
@@ -1671,29 +1717,7 @@ finish:
     ABC_PRTP( "Runtime: Refinement  ", p->timeCex,    clock() - clk );
     ABC_PRTP( "Runtime: Other       ", p->timeOther,  clock() - clk );
     ABC_PRTP( "Runtime: TOTAL       ", clock() - clk, clock() - clk );
-
-    
-    { // memory report
-    double memTot = 0;
-    double memAig = Gia_ManObjNum(p->pGia) * sizeof(Gia_Obj_t);
-    double memSat = sat_solver2_memory( p->pSat );
-    double memPro = sat_solver2_memory_proof( p->pSat );
-    double memMap = p->nObjsAlloc * sizeof(Vta_Obj_t) + p->nBins * sizeof(int);
-    double memOth = sizeof(Vta_Man_t);
-    memOth += Vec_IntCap(p->vOrder) * sizeof(int);
-    memOth += Vec_VecMemoryInt( (Vec_Vec_t *)p->vFrames );
-    memOth += Vec_BitCap(p->vSeenGla) * sizeof(int);
-    memOth += Vec_IntCap(p->vCla2Var) * sizeof(int);
-    memOth += Vec_VecMemoryInt( (Vec_Vec_t *)p->vCores );
-    memOth += Vec_IntCap(p->vAddedNew) * sizeof(int);
-    memTot = memAig + memSat + memPro + memMap + memOth;
-    ABC_PRMP( "Memory: AIG  ", memAig, memTot );
-    ABC_PRMP( "Memory: SAT  ", memSat, memTot );
-    ABC_PRMP( "Memory: Proof", memPro, memTot );
-    ABC_PRMP( "Memory: Map  ", memMap, memTot );
-    ABC_PRMP( "Memory: Other", memOth, memTot );
-    ABC_PRMP( "Memory: TOTAL", memTot, memTot );
-    }
+    Gia_VtaPrintMemory( p );
 
     Vga_ManStop( p );
     fflush( stdout );
diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c
index c6784fd6..fa2aa375 100644
--- a/src/base/abci/abc.c
+++ b/src/base/abci/abc.c
@@ -27372,8 +27372,8 @@ int Abc_CommandAbc9Gla( Abc_Frame_t * pAbc, int argc, char ** argv )
     Gia_ParVta_t Pars, * pPars = &Pars;
     int c;
     Gia_VtaSetDefaultParams( pPars );
-    pPars->nFramesStart = 20;
-    pPars->nLearntMax = 100000;
+    pPars->nFramesStart = 30;
+    pPars->nLearntMax   = 100000;
     Extra_UtilGetoptReset();
     while ( ( c = Extra_UtilGetopt( argc, argv, "FSPCLTRAtrdvh" ) ) != EOF )
     {