Performance improvement in &gla.

5 files changed, 274 insertions, 7 deletions

diff --git a/src/aig/gia/giaAbsGla.c b/src/aig/gia/giaAbsGla.c
index 01b41312..3b3799ea 100644
--- a/src/aig/gia/giaAbsGla.c
+++ b/src/aig/gia/giaAbsGla.c
@@ -62,7 +62,8 @@ typedef struct Gla_Man_t_ Gla_Man_t; // manager
 struct Gla_Man_t_
 {
     // user data
-    Gia_Man_t *    pGia;            // AIG manager
+    Gia_Man_t *    pGia0;           // starting AIG manager
+    Gia_Man_t *    pGia;            // working AIG manager
     Gia_ParVta_t*  pPars;           // parameters
     // internal data
     Vec_Int_t *    vAbs;            // abstracted objects
@@ -882,6 +883,226 @@ void Gla_ManCollectFanins( Gla_Man_t * p, Gla_Obj_t * pGla, int iObj, Vec_Int_t
     Vec_IntSort( vFanins, 0 );
 }
 
+
+/**Function*************************************************************
+
+  Synopsis    [Duplicates AIG while decoupling nodes duplicated in the mapping.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Gia_ManDupMapped_rec( Gia_Man_t * p, Gia_Obj_t * pObj, Gia_Man_t * pNew )
+{
+    if ( Gia_ObjIsTravIdCurrent(p, pObj) )
+        return;
+    Gia_ObjSetTravIdCurrent(p, pObj);
+    assert( Gia_ObjIsAnd(pObj) );
+    Gia_ManDupMapped_rec( p, Gia_ObjFanin0(pObj), pNew );
+    Gia_ManDupMapped_rec( p, Gia_ObjFanin1(pObj), pNew );
+    pObj->Value = Gia_ManAppendAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) );
+    Vec_IntPush( pNew->vLutConfigs, Gia_ObjId(p, pObj) );
+}
+Gia_Man_t * Gia_ManDupMapped( Gia_Man_t * p, Vec_Int_t * vMapping )
+{
+    Gia_Man_t * pNew;
+    Gia_Obj_t * pObj, * pFanin;
+    int i, k, * pMapping, * pObj2Obj;
+    // start new manager
+    pNew = Gia_ManStart( Gia_ManObjNum(p) );
+    pNew->pName = Abc_UtilStrsav( p->pName );
+    // start mapping
+    Gia_ManFillValue( p );
+    pObj2Obj = ABC_FALLOC( int, Gia_ManObjNum(p) );
+    pObj2Obj[0] = 0;
+    // create reverse mapping and attach it to the node
+    pNew->vLutConfigs = Vec_IntAlloc( Gia_ManObjNum(p) * 4 / 3 );
+    Vec_IntPush( pNew->vLutConfigs, 0 );
+    Gia_ManForEachObj1( p, pObj, i )
+    {
+        if ( Gia_ObjIsAnd(pObj) )
+        {
+            int Offset = Vec_IntEntry(vMapping, Gia_ObjId(p, pObj));
+            if ( Offset == 0 )
+                continue;
+            pMapping = Vec_IntEntryP( vMapping, Offset );
+            Gia_ManIncrementTravId( p );
+            for ( k = 1; k <= 4; k++ )
+            {
+                if ( pMapping[k] == -1 )
+                    continue;
+                pFanin = Gia_ManObj(p, pMapping[k]);
+                Gia_ObjSetTravIdCurrent( p, pFanin );
+                pFanin->Value = pObj2Obj[pMapping[k]];
+                assert( ~pFanin->Value );
+            }
+            assert( !Gia_ObjIsTravIdCurrent(p, pObj) );
+            assert( !~pObj->Value );
+            Gia_ManDupMapped_rec( p, pObj, pNew );
+            pObj2Obj[i] = pObj->Value;
+            assert( ~pObj->Value );
+        }
+        else if ( Gia_ObjIsCi(pObj) )
+        {
+            pObj2Obj[i] = Gia_ManAppendCi( pNew );
+            Vec_IntPush( pNew->vLutConfigs, i );
+        }
+        else if ( Gia_ObjIsCo(pObj) )
+        {
+            Gia_ObjFanin0(pObj)->Value = pObj2Obj[Gia_ObjFaninId0p(p, pObj)];
+            assert( Gia_ObjFanin0(pObj)->Value >= 0 );
+            pObj2Obj[i] = Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) );
+            Vec_IntPush( pNew->vLutConfigs, i );
+        }
+    }
+    assert( Vec_IntSize(pNew->vLutConfigs) == Gia_ManObjNum(pNew) );
+    Gia_ManSetRegNum( pNew, Gia_ManRegNum(p) );
+    // map original AIG into the new AIG
+    Gia_ManForEachObj( p, pObj, i )
+        pObj->Value = pObj2Obj[i];
+    ABC_FREE( pObj2Obj );
+    return pNew;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Creates a new manager.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Gla_Man_t * Gla_ManStart2( Gia_Man_t * pGia0, Gia_ParVta_t * pPars )
+{
+    Gla_Man_t * p;
+    Aig_Man_t * pAig;
+    Gia_Obj_t * pObj;
+    Gla_Obj_t * pGla;
+    Vec_Int_t * vMappingNew;
+    int i, * pLits, * pObj2Count, * pObj2Clause;
+
+    // start
+    p = ABC_CALLOC( Gla_Man_t, 1 );
+    p->pGia0 = pGia0;
+    p->pPars = pPars;
+    p->vAbs  = Vec_IntAlloc( 100 );
+    p->vTemp = Vec_IntAlloc( 100 );
+    p->vAddedNew = Vec_IntAlloc( 100 );
+    p->vPrioSels = Vec_IntAlloc( 100 );
+
+    // internal data
+    pAig = Gia_ManToAigSimple( pGia0 );
+    p->pCnf = Cnf_DeriveOther( pAig );
+    Aig_ManStop( pAig );
+
+    // create working GIA
+    p->pGia = Gia_ManDupMapped( pGia0, p->pCnf->vMapping );
+//printf( "Old GIA = %d.  New GIA = %d.\n", Gia_ManObjNum(pGia0), Gia_ManObjNum(p->pGia) );
+
+    // derive new gate map
+    assert( pGia0->vGateClasses != 0 );
+    p->pGia->vGateClasses = Vec_IntStart( Gia_ManObjNum(p->pGia) );
+    // update p->pCnf->vMapping, p->pCnf->pObj2Count, p->pCnf->pObj2Clause 
+    vMappingNew = Vec_IntStart( Gia_ManObjNum(p->pGia) );
+    pObj2Count  = ABC_ALLOC( int, Gia_ManObjNum(p->pGia) );
+    pObj2Clause = ABC_ALLOC( int, Gia_ManObjNum(p->pGia) );
+    Gia_ManForEachObj( pGia0, pObj, i )
+    {
+        if ( !~pObj->Value )
+            continue;
+        // replace positive literal by variable
+        assert( !Abc_LitIsCompl(pObj->Value) );
+        pObj->Value = Abc_Lit2Var(pObj->Value);
+        assert( (int)pObj->Value < Gia_ManObjNum(p->pGia) );
+        // update mappings
+        Vec_IntWriteEntry( vMappingNew, pObj->Value, Vec_IntEntry(p->pCnf->vMapping, i) );
+        pObj2Count[pObj->Value] = p->pCnf->pObj2Count[i];
+        pObj2Clause[pObj->Value] = p->pCnf->pObj2Clause[i];
+        if ( Vec_IntEntry(pGia0->vGateClasses, i) )
+            Vec_IntWriteEntry( p->pGia->vGateClasses, pObj->Value, 1 );
+    }
+    Vec_IntFree( p->pCnf->vMapping );  p->pCnf->vMapping    = vMappingNew;
+    ABC_FREE( p->pCnf->pObj2Count );   p->pCnf->pObj2Count  = pObj2Count;
+    ABC_FREE( p->pCnf->pObj2Clause );  p->pCnf->pObj2Clause = pObj2Clause;
+
+
+    // count the number of variables
+    p->nObjs = 1;
+    Gia_ManForEachObj( p->pGia, pObj, i )
+        if ( p->pCnf->pObj2Count[i] >= 0 )
+            pObj->Value = p->nObjs++;
+        else
+            pObj->Value = ~0;
+
+    // re-express CNF using new variable IDs
+    pLits = p->pCnf->pClauses[0];
+    for ( i = 0; i < p->pCnf->nLiterals; i++ )
+    {
+        // find the original AIG object
+        pObj = Gia_ManObj( pGia0, lit_var(pLits[i]) );
+        assert( ~pObj->Value );
+        // find the working AIG object
+        pObj = Gia_ManObj( p->pGia, pObj->Value );
+        assert( ~pObj->Value );
+        // express literal in terms of LUT variables
+        pLits[i] = toLitCond( pObj->Value, lit_sign(pLits[i]) );
+    }
+
+    // create objects 
+    p->pObjs    = ABC_CALLOC( Gla_Obj_t, p->nObjs );
+    p->pObj2Obj = ABC_FALLOC( unsigned, Gia_ManObjNum(p->pGia) );
+    p->pvRefis  = ABC_CALLOC( Vec_Int_t, Gia_ManObjNum(p->pGia) );
+    Gia_ManForEachObj( p->pGia, pObj, i )
+    {
+        p->pObj2Obj[i] = pObj->Value;
+        if ( !~pObj->Value )
+            continue;
+        pGla = Gla_ManObj( p, pObj->Value );
+        pGla->iGiaObj = i;
+        pGla->fCompl0 = Gia_ObjFaninC0(pObj);
+        pGla->fConst  = Gia_ObjIsConst0(pObj);
+        pGla->fPi     = Gia_ObjIsPi(p->pGia, pObj);
+        pGla->fPo     = Gia_ObjIsPo(p->pGia, pObj);
+        pGla->fRi     = Gia_ObjIsRi(p->pGia, pObj);
+        pGla->fRo     = Gia_ObjIsRo(p->pGia, pObj);
+        pGla->fAnd    = Gia_ObjIsAnd(pObj);
+        if ( Gia_ObjIsConst0(pObj) || Gia_ObjIsPi(p->pGia, pObj) )
+            continue;
+        if ( Gia_ObjIsAnd(pObj) || Gia_ObjIsCo(pObj) )
+        {
+            Gla_ManCollectFanins( p, pGla, pObj->Value, p->vTemp );
+            pGla->nFanins = Vec_IntSize( p->vTemp );
+            memcpy( pGla->Fanins, Vec_IntArray(p->vTemp), sizeof(int) * Vec_IntSize(p->vTemp) );
+            continue;
+        }
+        assert( Gia_ObjIsRo(p->pGia, pObj) );
+        pGla->nFanins   = 1;
+        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( p->pGia->vGateClasses != NULL );
+    Gla_ManForEachObj( p, pGla )
+    {
+        if ( Vec_IntEntry( p->pGia->vGateClasses, pGla->iGiaObj ) == 0 )
+            continue;
+        pGla->fAbs = 1;
+        Vec_IntPush( p->vAbs, Gla_ObjId(p, pGla) );
+    }
+    // other 
+    p->vCla2Obj  = Vec_IntAlloc( 1000 );  Vec_IntPush( p->vCla2Obj, -1 );
+    p->pSat      = sat_solver2_new();
+    p->nSatVars  = 1;
+    return p;
+}
+
 /**Function*************************************************************
 
   Synopsis    [Creates a new manager.]
@@ -996,6 +1217,8 @@ void Gla_ManStop( Gla_Man_t * p )
     Gla_ManForEachObj( p, pGla )
         ABC_FREE( pGla->vFrames.pArray );
     Cnf_DataFree( p->pCnf );
+    if ( p->pGia0 != NULL )
+        Gia_ManStop( p->pGia );
     sat_solver2_delete( p->pSat );
     Vec_IntFreeP( &p->vCla2Obj );
     Vec_IntFreeP( &p->vPrevCore );
@@ -1065,7 +1288,7 @@ int Gla_ManTranslate_rec( Gia_Man_t * p, Gia_Obj_t * pObj, Vec_Int_t * vMap )
 }
 Vec_Int_t * Gla_ManTranslate( Gla_Man_t * p )
 {
-    Vec_Int_t * vRes;
+    Vec_Int_t * vRes, * vRes2;
     Gla_Obj_t * pObj, * pFanin;
     Gia_Obj_t * pGiaObj;
     int i, k;
@@ -1082,6 +1305,15 @@ Vec_Int_t * Gla_ManTranslate( Gla_Man_t * p )
             Gia_ObjSetTravIdCurrent( p->pGia, Gla_ManGiaObj(p, pFanin) );
         Gla_ManTranslate_rec( p->pGia, pGiaObj, vRes );
     }
+    if ( p->pGia->vLutConfigs )
+    {
+        vRes2 = Vec_IntStart( Gia_ManObjNum(p->pGia0) );
+        for ( i = 0; i < Gia_ManObjNum(p->pGia); i++ )
+            if ( Vec_IntEntry(vRes, i) )
+                Vec_IntWriteEntry( vRes2, Vec_IntEntry(p->pGia->vLutConfigs, i), 1 );
+        Vec_IntFree( vRes );
+        return vRes2;
+    }
     return vRes;
 }
 
@@ -1548,7 +1780,7 @@ void Gia_GlaDumpAbsracted( Gla_Man_t * p, int fVerbose )
 //        return;
     // create abstraction
     vGateClasses = Gla_ManTranslate( p );
-    pAbs = Gia_ManDupAbsGates( p->pGia, vGateClasses );
+    pAbs = Gia_ManDupAbsGates( p->pGia0, vGateClasses );
     Vec_IntFreeP( &vGateClasses );
     // write into file
     Gia_WriteAiger( pAbs, pFileName, 0, 0 );
diff --git a/src/aig/gia/giaAbsVta.c b/src/aig/gia/giaAbsVta.c
index 44169f23..8a41ec40 100644
--- a/src/aig/gia/giaAbsVta.c
+++ b/src/aig/gia/giaAbsVta.c
@@ -647,6 +647,30 @@ void Vta_ManSatVerify( Vta_Man_t * p )
   SeeAlso     []
 
 ***********************************************************************/
+void Vta_ManProfileAddition( Vta_Man_t * p, Vec_Int_t * vTermsToAdd )
+{
+    Vta_Obj_t * pThis;
+    Gia_Obj_t * pObj;
+    // profile the added ones
+    int i, * pCounters = ABC_CALLOC( int, p->pPars->iFrame+1 );
+    Vta_ManForEachObjObjVec( vTermsToAdd, p, pThis, pObj, i )
+        pCounters[pThis->iFrame]++;
+    for ( i = 0; i <= p->pPars->iFrame; i++ )
+        printf( "%2d", pCounters[i] );
+    printf( "***\n" );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Refines abstraction.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
 Abc_Cex_t * Vta_ManRefineAbstraction( Vta_Man_t * p, int f )
 {
     int fVerify = 0;
@@ -733,7 +757,12 @@ Abc_Cex_t * Vta_ManRefineAbstraction( Vta_Man_t * p, int f )
     }
 
 /*
-    // update priorities according to reconvergest counters
+    Vta_ManForEachObjObjVecReverse( vOrder, p, pThis, pObj, i )
+        if ( pThis->Prio > 0 )
+            pThis->Prio = 10;
+*/
+/*
+    // update priorities according to reconvergence counters
     Vec_PtrForEachEntry( Vta_Obj_t *, vTermsUsed, pThis, i )
     {
         Vta_Obj_t * pThis0, * pThis1;
@@ -758,13 +787,13 @@ Abc_Cex_t * Vta_ManRefineAbstraction( Vta_Man_t * p, int f )
     }
 */
 
-/*
-    // update priorities according to reconvergest counters
+
+    // update priorities according to reconvergence counters
     Vec_PtrForEachEntry( Vta_Obj_t *, vTermsUsed, pThis, i )
         pThis->Prio = pThis->iObj;
     Vec_PtrForEachEntry( Vta_Obj_t *, vTermsUnused, pThis, i )
         pThis->Prio = pThis->iObj;
-*/
+
 
     // objects with equal distance should receive priority based on number
     // those objects whose prototypes have been added in other timeframes
@@ -943,6 +972,7 @@ Abc_Cex_t * Vta_ManRefineAbstraction( Vta_Man_t * p, int f )
 //Vec_IntReverseOrder( vTermsToAdd );
 //Vec_IntSort( vTermsToAdd, 1 );
 
+
     // cleanup
     Vec_PtrFree( vTermsUsed );
     Vec_PtrFree( vTermsUnused );
@@ -1017,6 +1047,8 @@ Abc_Cex_t * Vta_ManRefineAbstraction( Vta_Man_t * p, int f )
         pCex = Vga_ManDeriveCex( p );
     else
     {
+//       Vta_ManProfileAddition( p, vTermsToAdd );
+
         Vta_ManForEachObjObjVec( vTermsToAdd, p, pThis, pObj, i )
             if ( !Gia_ObjIsPi(p->pGia, pObj) )
                 Vga_ManAddClausesOne( p, pThis->iObj, pThis->iFrame );
diff --git a/src/sat/cnf/cnf.h b/src/sat/cnf/cnf.h
index 0b6fc8c2..54aaf5ca 100644
--- a/src/sat/cnf/cnf.h
+++ b/src/sat/cnf/cnf.h
@@ -64,6 +64,7 @@ struct Cnf_Dat_t_
     int *           pVarNums;        // the number of CNF variable for each node ID (-1 if unused)
     int *           pObj2Clause;     // the mapping of objects into clauses
     int *           pObj2Count;      // the mapping of objects into clause number
+    Vec_Int_t *     vMapping;        // mapping of internal nodes
 };
 
 // the cut used to represent node in the AIG
diff --git a/src/sat/cnf/cnfCore.c b/src/sat/cnf/cnfCore.c
index eb46e704..d1dd8561 100644
--- a/src/sat/cnf/cnfCore.c
+++ b/src/sat/cnf/cnfCore.c
@@ -180,6 +180,7 @@ clk = clock();
     Cnf_ManTransferCuts( p );
     vMapped = Cnf_ManScanMapping( p, 1, 1 );
     pCnf = Cnf_ManWriteCnfOther( p, vMapped );
+    pCnf->vMapping = Cnf_ManWriteCnfMapping( p, vMapped );
     Vec_PtrFree( vMapped );
     Aig_MmFixedStop( pMemCuts, 0 );
 p->timeSave = clock() - clk;
diff --git a/src/sat/cnf/cnfMan.c b/src/sat/cnf/cnfMan.c
index a4081f86..c3099d1e 100644
--- a/src/sat/cnf/cnfMan.c
+++ b/src/sat/cnf/cnfMan.c
@@ -181,6 +181,7 @@ void Cnf_DataFree( Cnf_Dat_t * p )
 {
     if ( p == NULL )
         return;
+    Vec_IntFreeP( &p->vMapping );
     ABC_FREE( p->pObj2Clause );
     ABC_FREE( p->pObj2Count );
     ABC_FREE( p->pClauses[0] );