Improvements to the new abstraction code.

3 files changed, 138 insertions, 76 deletions

diff --git a/src/aig/gia/giaAbs.c b/src/aig/gia/giaAbs.c
index 54b65484..2432bdbf 100644
--- a/src/aig/gia/giaAbs.c
+++ b/src/aig/gia/giaAbs.c
@@ -379,25 +379,29 @@ int Gia_ManPbaPerform( Gia_Man_t * pGia, int nStart, int nFrames, int nConfLimit
 ***********************************************************************/
 int Gia_ManGlaCbaPerform( Gia_Man_t * pGia, void * pPars, int fNaiveCnf )
 {
-    extern Vec_Int_t * Aig_Gla1ManTest( Aig_Man_t * pAig, int nFramesMax, int nConfLimit, int TimeLimit, int fNaiveCnf, int fVerbose );
+    extern Vec_Int_t * Aig_Gla1ManTest( Aig_Man_t * pAig, Vec_Int_t * vGateClassesOld, int nStart, int nFramesMax, int nConfLimit, int TimeLimit, int fNaiveCnf, int fVerbose );
     Saig_ParBmc_t * p = (Saig_ParBmc_t *)pPars;
-    Vec_Int_t * vGateClasses;
+    Vec_Int_t * vGateClasses, * vGateClassesOld = NULL;
     Aig_Man_t * pAig;
-/*
+
     // check if flop classes are given
     if ( pGia->vGateClasses == NULL )
+        Abc_Print( 0, "Initial gate map is not given. Abstraction begins from scratch.\n" );
+    else
     {
-        Abc_Print( 0, "Initial gate map is not given. Trivial abstraction is assumed.\n" );
-        pGia->vGateClasses = Vec_IntStart( Gia_ManObjNum(pGia) );
+        Abc_Print( 0, "Initial gate map is given. Abstraction refines this map.\n" );
+        vGateClassesOld = pGia->vGateClasses; pGia->vGateClasses = NULL;
+        fNaiveCnf = 1;
     }
-*/
+
     // perform abstraction
     pAig = Gia_ManToAigSimple( pGia );
-    vGateClasses = Aig_Gla1ManTest( pAig, p->nFramesMax, p->nConfLimit, p->nTimeOut, fNaiveCnf, p->fVerbose );
+    assert( vGateClassesOld == NULL || Vec_IntSize(vGateClassesOld) == Aig_ManObjNumMax(pAig) );
+    vGateClasses = Aig_Gla1ManTest( pAig, vGateClassesOld, p->nStart, p->nFramesMax, p->nConfLimit, p->nTimeOut, fNaiveCnf, p->fVerbose );
     Aig_ManStop( pAig );
 
     // update the map
-    Vec_IntFreeP( &pGia->vGateClasses );
+    Vec_IntFreeP( &vGateClassesOld );
     pGia->vGateClasses = vGateClasses;
     return 1;
 }
@@ -415,26 +419,63 @@ int Gia_ManGlaCbaPerform( Gia_Man_t * pGia, void * pPars, int fNaiveCnf )
 ***********************************************************************/
 int Gia_ManGlaPbaPerform( Gia_Man_t * pGia, void * pPars )
 {
-    extern Vec_Int_t * Aig_Gla2ManTest( Aig_Man_t * pAig, int nFramesMax, int nConfLimit, int TimeLimit, int fVerbose );
+    extern Vec_Int_t * Aig_Gla2ManTest( Aig_Man_t * pAig, int nStart, int nFramesMax, int nConfLimit, int TimeLimit, int fVerbose );
     Saig_ParBmc_t * p = (Saig_ParBmc_t *)pPars;
     Vec_Int_t * vGateClasses;
     Aig_Man_t * pAig;
-/*
+
     // check if flop classes are given
     if ( pGia->vGateClasses == NULL )
     {
-        Abc_Print( 0, "Initial gate map is not given. Trivial abstraction is assumed.\n" );
-        pGia->vGateClasses = Vec_IntStart( Gia_ManObjNum(pGia) );
+        Abc_Print( 0, "Initial gate map is not given. Abstraction begins from scratch.\n" );
+        pAig = Gia_ManToAigSimple( pGia );
     }
-*/
+    else
+    {
+        Gia_Man_t * pGiaAbs;
+        Abc_Print( 0, "Initial gate map is given. Abstraction refines this map.\n" );
+        pGiaAbs = Gia_ManDupAbsGates( pGia, pGia->vGateClasses );
+        pAig = Gia_ManToAigSimple( pGiaAbs );
+        Gia_ManStop( pGiaAbs );
+    }
+
     // perform abstraction
-    pAig = Gia_ManToAigSimple( pGia );
-    vGateClasses = Aig_Gla2ManTest( pAig, p->nFramesMax, p->nConfLimit, p->nTimeOut, p->fVerbose );
+    vGateClasses = Aig_Gla2ManTest( pAig, p->nStart, p->nFramesMax, p->nConfLimit, p->nTimeOut, p->fVerbose );
     Aig_ManStop( pAig );
 
-    // update the map
-    Vec_IntFreeP( &pGia->vGateClasses );
-    pGia->vGateClasses = vGateClasses;
+    // update the BMC depth
+    if ( vGateClasses )
+        p->iFrame = p->nFramesMax;
+
+    // update the abstraction map (hint: AIG and GIA have one-to-one obj ID match)
+    if ( pGia->vGateClasses && vGateClasses )
+    {
+        Gia_Obj_t * pObj;
+        int i, Counter = 0;
+        Gia_ManForEachObj1( pGia, pObj, i )
+        {
+            if ( !~pObj->Value )
+                continue;
+            if ( !Vec_IntEntry(pGia->vGateClasses, i) )
+                continue;
+            // this obj was abstracted before
+            assert( Gia_ObjIsAnd(pObj) || Gia_ObjIsRo(pGia, pObj) );
+            // if corresponding AIG object is not abstracted, remove abstraction
+            if ( !Vec_IntEntry(vGateClasses, Gia_Lit2Var(pObj->Value)) )
+            {
+                Vec_IntWriteEntry( pGia->vGateClasses, i, 0 );
+                Counter++;
+            }
+        }
+        Vec_IntFree( vGateClasses );
+        if ( p->fVerbose )
+            Abc_Print( 1, "Repetition of abstraction removed %d entries from the old abstraction map.\n", Counter );
+    }
+    else
+    {
+        Vec_IntFreeP( &pGia->vGateClasses );
+        pGia->vGateClasses = vGateClasses;
+    }
     return 1;
 }
 
diff --git a/src/aig/saig/saigGlaCba.c b/src/aig/saig/saigGlaCba.c
index 8fca4796..fe849a07 100644
--- a/src/aig/saig/saigGlaCba.c
+++ b/src/aig/saig/saigGlaCba.c
@@ -151,43 +151,6 @@ static inline int Aig_Gla1AddNode( sat_solver * pSat, int iVar, int iVar0, int i
 
 /**Function*************************************************************
 
-  Synopsis    [Returns the array of neighbors.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-Vec_Int_t * Aig_Gla1CollectAssigned_( Aig_Man_t * p, Vec_Int_t * vGateClasses )
-{
-    Vec_Int_t * vAssigned;
-    Aig_Obj_t * pObj;
-    int i, Entry;
-    vAssigned = Vec_IntAlloc( 1000 );
-    Vec_IntForEachEntry( vGateClasses, Entry, i )
-    {
-        if ( Entry == 0 )
-            continue;
-        assert( Entry == 1 );
-        pObj = Aig_ManObj( p, i );
-        Vec_IntPush( vAssigned, Aig_ObjId(pObj) );
-        if ( Aig_ObjIsNode(pObj) )
-        {
-            Vec_IntPush( vAssigned, Aig_ObjFaninId0(pObj) );
-            Vec_IntPush( vAssigned, Aig_ObjFaninId1(pObj) );
-        }
-        else if ( Saig_ObjIsLo(p, pObj) )
-            Vec_IntPush( vAssigned, Aig_ObjFaninId0(Saig_ObjLoToLi(p, pObj)) );
-        else assert( Aig_ObjIsConst1(pObj) );
-    }
-    Vec_IntUniqify( vAssigned );
-    return vAssigned;
-}
-
-/**Function*************************************************************
-
   Synopsis    [Derives abstraction components (PIs, PPIs, flops, nodes).]
 
   Description []
@@ -446,6 +409,44 @@ int Aig_Gla1ObjAddToSolver( Aig_Gla1Man_t * p, Aig_Obj_t * pObj, int k )
 
 /**Function*************************************************************
 
+  Synopsis    [Returns the array of neighbors.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Vec_Int_t * Aig_Gla1CollectAssigned( Aig_Man_t * p, Vec_Int_t * vGateClasses )
+{
+    Vec_Int_t * vAssigned;
+    Aig_Obj_t * pObj;
+    int i, Entry;
+    vAssigned = Vec_IntAlloc( 1000 );
+    Vec_IntForEachEntry( vGateClasses, Entry, i )
+    {
+        if ( Entry == 0 )
+            continue;
+        assert( Entry == 1 );
+        pObj = Aig_ManObj( p, i );
+        Vec_IntPush( vAssigned, Aig_ObjId(pObj) );
+        if ( Aig_ObjIsNode(pObj) )
+        {
+            Vec_IntPush( vAssigned, Aig_ObjFaninId0(pObj) );
+            Vec_IntPush( vAssigned, Aig_ObjFaninId1(pObj) );
+        }
+        else if ( Saig_ObjIsLo(p, pObj) )
+            Vec_IntPush( vAssigned, Aig_ObjFaninId0(Saig_ObjLoToLi(p, pObj)) );
+        else assert( Aig_ObjIsConst1(pObj) );
+    }
+    Vec_IntUniqify( vAssigned );
+    Vec_IntReverseOrder( vAssigned );
+    return vAssigned;
+}
+
+/**Function*************************************************************
+
   Synopsis    []
 
   Description []
@@ -455,16 +456,25 @@ int Aig_Gla1ObjAddToSolver( Aig_Gla1Man_t * p, Aig_Obj_t * pObj, int k )
   SeeAlso     []
 
 ***********************************************************************/
-Aig_Gla1Man_t * Aig_Gla1ManStart( Aig_Man_t * pAig, int fNaiveCnf )
+Aig_Gla1Man_t * Aig_Gla1ManStart( Aig_Man_t * pAig, Vec_Int_t * vGateClassesOld, int fNaiveCnf )
 {
     Aig_Gla1Man_t * p;
     int i;
 
     p = ABC_CALLOC( Aig_Gla1Man_t, 1 );
     p->pAig      = pAig;
-    p->vAssigned = Vec_IntAlloc( 1000 );
-    p->vIncluded = Vec_IntStart( Aig_ManObjNumMax(pAig) );
     p->nFrames   = 32;
+    if ( vGateClassesOld )
+    {
+        p->vAssigned = Aig_Gla1CollectAssigned( pAig, vGateClassesOld );
+        p->vIncluded = Vec_IntDup( vGateClassesOld );
+        assert( fNaiveCnf );
+    }
+    else
+    {
+        p->vAssigned = Vec_IntAlloc( 1000 );
+        p->vIncluded = Vec_IntStart( Aig_ManObjNumMax(pAig) );
+    }
 
     p->vPis      = Vec_IntAlloc( 1000 );
     p->vPPis     = Vec_IntAlloc( 1000 );
@@ -651,9 +661,8 @@ void Aig_Gla1ExtendIncluded( Aig_Gla1Man_t * p )
   SeeAlso     []
 
 ***********************************************************************/
-Vec_Int_t * Aig_Gla1ManTest( Aig_Man_t * pAig, int nFramesMax, int nConfLimit, int TimeLimit, int fNaiveCnf, int fVerbose )
+Vec_Int_t * Aig_Gla1ManTest( Aig_Man_t * pAig, Vec_Int_t * vGateClassesOld, int nStart, int nFramesMax, int nConfLimit, int TimeLimit, int fNaiveCnf, int fVerbose )
 {
-    int nStart = 0;
     Vec_Int_t * vResult = NULL;
     Aig_Gla1Man_t * p;
     Aig_Man_t * pAbs;
@@ -664,6 +673,9 @@ Vec_Int_t * Aig_Gla1ManTest( Aig_Man_t * pAig, int nFramesMax, int nConfLimit, i
     int nConfBef, nConfAft, clk, clkTotal = clock();
     assert( Saig_ManPoNum(pAig) == 1 );
 
+    if ( nFramesMax == 0 )
+        nFramesMax = ABC_INFINITY;
+
     if ( fVerbose )
     {
         if ( TimeLimit )
@@ -673,7 +685,7 @@ Vec_Int_t * Aig_Gla1ManTest( Aig_Man_t * pAig, int nFramesMax, int nConfLimit, i
     }
 
     // start the solver
-    p = Aig_Gla1ManStart( pAig, fNaiveCnf );
+    p = Aig_Gla1ManStart( pAig, vGateClassesOld, fNaiveCnf );
     p->nFramesMax = nFramesMax;
     p->nConfLimit = nConfLimit;
     p->fVerbose   = fVerbose;
@@ -695,6 +707,10 @@ Vec_Int_t * Aig_Gla1ManTest( Aig_Man_t * pAig, int nFramesMax, int nConfLimit, i
                 if ( !Aig_Gla1ObjAddToSolver( p, pObj, f ) )
                     printf( "Error!  SAT solver became UNSAT.\n" );
 
+        // skip checking if we are not supposed to
+        if ( f < nStart )
+            continue;
+
         // create output literal to represent property failure
         pObj    = Aig_ManPo( pAig, 0 );
         iSatVar = Aig_Gla1FetchVar( p, Aig_ObjFanin0(pObj), f );
@@ -702,7 +718,7 @@ Vec_Int_t * Aig_Gla1ManTest( Aig_Man_t * pAig, int nFramesMax, int nConfLimit, i
 
         // try solving the abstraction
         Aig_Gla1CollectAbstr( p );
-        for ( r = 0; r < 1000000; r++ )
+        for ( r = 0; r < ABC_INFINITY; r++ )
         {
             // try to find a counter-example
             clk = clock();
@@ -724,7 +740,10 @@ Vec_Int_t * Aig_Gla1ManTest( Aig_Man_t * pAig, int nFramesMax, int nConfLimit, i
                     else if ( RetValue != l_False )
                         printf( "       SAT solver returned UNDECIDED after %5d conflicts.\n", nConfAft - nConfBef );
                     else
-                        printf( "       SAT solver returned UNSAT after %5d conflicts.\n", nConfAft - nConfBef );
+                    {
+                        printf( "       SAT solver returned UNSAT after %5d conflicts.  ", nConfAft - nConfBef );
+                        Abc_PrintTime( 1, "Total time", clock() - clkTotal );
+                    }
                 }
                 break;
             }
diff --git a/src/aig/saig/saigGlaPba.c b/src/aig/saig/saigGlaPba.c
index a7b51cc2..df398f21 100644
--- a/src/aig/saig/saigGlaPba.c
+++ b/src/aig/saig/saigGlaPba.c
@@ -34,7 +34,7 @@ struct Aig_Gla2Man_t_
 {
     // user data
     Aig_Man_t *    pAig;
-    int            nConfMax;
+    int            nStart;
     int            nFramesMax;
     int            fVerbose;
     // unrolling
@@ -226,8 +226,8 @@ int Aig_Gla2CreateSatSolver( Aig_Gla2Man_t * p )
     int i, f, ObjId, nVars, RetValue = 1;
 
     // assign variables
-//    for ( f = p->nFramesMax - 1; f >= 0; f-- )
-    for ( f = 0; f < p->nFramesMax; f++ )
+    for ( f = p->nFramesMax - 1; f >= 0; f-- )
+//    for ( f = 0; f < p->nFramesMax; f++ )
         Aig_Gla2AssignVars_rec( p, Aig_ManPo(p->pAig, 0), f );
 
     // create SAT solver
@@ -301,7 +301,7 @@ int Aig_Gla2CreateSatSolver( Aig_Gla2Man_t * p )
 
     // add output clause
     vPoLits = Vec_IntAlloc( p->nFramesMax );
-    for ( f = 0; f < p->nFramesMax; f++ )
+    for ( f = p->nStart; f < p->nFramesMax; f++ )
         Vec_IntPush( vPoLits, 2 * Aig_Gla2FetchVar(p, Aig_ManPo(p->pAig, 0), f) );
     RetValue &= sat_solver_addclause( p->pSat, Vec_IntArray(vPoLits), Vec_IntArray(vPoLits) + Vec_IntSize(vPoLits) );
     Vec_IntFree( vPoLits );
@@ -311,11 +311,12 @@ int Aig_Gla2CreateSatSolver( Aig_Gla2Man_t * p )
 
     assert( nVars == Vec_IntSize(p->vVar2Inf) );
     assert( ((Sto_Man_t *)p->pSat->pStore)->nClauses == Vec_IntSize(p->vCla2Obj) );
-
 //    Sto_ManDumpClauses( ((Sto_Man_t *)p->pSat->pStore), "temp_sto.cnf" );
-
-
     sat_solver_store_mark_roots( p->pSat ); 
+
+    if ( p->fVerbose )
+        printf( "The resulting SAT problem contains %d vars, %d clauses, and %d literals.\n", 
+            p->pSat->size, p->pSat->stats.clauses, p->pSat->stats.tot_literals );
     return RetValue;
 }
 
@@ -330,7 +331,7 @@ int Aig_Gla2CreateSatSolver( Aig_Gla2Man_t * p )
   SeeAlso     []
 
 ***********************************************************************/
-Aig_Gla2Man_t * Aig_Gla2ManStart( Aig_Man_t * pAig, int nFramesMax )
+Aig_Gla2Man_t * Aig_Gla2ManStart( Aig_Man_t * pAig, int nStart, int nFramesMax, int fVerbose )
 {
     Aig_Gla2Man_t * p;
     int i;
@@ -345,7 +346,9 @@ Aig_Gla2Man_t * Aig_Gla2ManStart( Aig_Man_t * pAig, int nFramesMax )
     p->vCla2Fra   = Vec_IntAlloc( 1 << 20 );
 
     // skip first vector ID
+    p->nStart     = nStart;
     p->nFramesMax = nFramesMax;
+    p->fVerbose   = fVerbose;
     for ( i = 0; i < p->nFramesMax; i++ )
         Vec_IntPush( p->vVec2Var, -1 );
 
@@ -416,7 +419,7 @@ Vec_Int_t * Saig_AbsSolverUnsatCore( sat_solver * pSat, int nConfMax, int fVerbo
     }
     if ( fVerbose )
     {
-        printf( "SAT solver returned UNSAT after %d conflicts.  ", pSat->stats.conflicts );
+        printf( "SAT solver returned UNSAT after %7d conflicts.      ", pSat->stats.conflicts );
         ABC_PRT( "Time", clock() - clk );
     }
     assert( RetValue == l_False );
@@ -428,7 +431,7 @@ Vec_Int_t * Saig_AbsSolverUnsatCore( sat_solver * pSat, int nConfMax, int fVerbo
     Intp_ManFree( pManProof );
     if ( fVerbose )
     {
-        printf( "SAT core contains %d clauses (out of %d).     ", Vec_IntSize(vCore), ((Sto_Man_t *)pSatCnf)->nRoots );
+        printf( "SAT core contains %8d clauses (out of %8d).   ", Vec_IntSize(vCore), ((Sto_Man_t *)pSatCnf)->nRoots );
         ABC_PRT( "Time", clock() - clk );
     }
     Sto_ManFree( (Sto_Man_t *)pSatCnf );
@@ -500,9 +503,8 @@ Vec_Int_t * Aig_Gla2ManCollect( Aig_Gla2Man_t * p, Vec_Int_t * vCore )
   SeeAlso     []
 
 ***********************************************************************/
-Vec_Int_t * Aig_Gla2ManTest( Aig_Man_t * pAig, int nFramesMax, int nConfLimit, int TimeLimit, int fVerbose )
+Vec_Int_t * Aig_Gla2ManTest( Aig_Man_t * pAig, int nStart, int nFramesMax, int nConfLimit, int TimeLimit, int fVerbose )
 {
-    int nStart = 0;
     Aig_Gla2Man_t * p;
     Vec_Int_t * vCore, * vResult;
     int clk, clkTotal = clock();
@@ -518,7 +520,7 @@ Vec_Int_t * Aig_Gla2ManTest( Aig_Man_t * pAig, int nFramesMax, int nConfLimit, i
 
     // start the solver
     clk = clock();
-    p = Aig_Gla2ManStart( pAig, nFramesMax );
+    p = Aig_Gla2ManStart( pAig, nStart, nFramesMax, fVerbose );
     if ( !Aig_Gla2CreateSatSolver( p ) )
     {
         printf( "Error!  SAT solver became UNSAT.\n" );