Integrating sweeping information.

4 files changed, 139 insertions, 69 deletions

diff --git a/src/aig/gia/gia.h b/src/aig/gia/gia.h
index a3a3564d..02dd5a66 100644
--- a/src/aig/gia/gia.h
+++ b/src/aig/gia/gia.h
@@ -811,6 +811,7 @@ extern Gia_Man_t *         Gia_ManDupOrderDfs( Gia_Man_t * p );
 extern Gia_Man_t *         Gia_ManDupOrderDfsChoices( Gia_Man_t * p );
 extern Gia_Man_t *         Gia_ManDupOrderDfsReverse( Gia_Man_t * p );
 extern Gia_Man_t *         Gia_ManDupOutputGroup( Gia_Man_t * p, int iOutStart, int iOutStop );
+extern Gia_Man_t *         Gia_ManDupOutputVec( Gia_Man_t * p, Vec_Int_t * vOutPres );
 extern Gia_Man_t *         Gia_ManDupOrderAiger( Gia_Man_t * p );
 extern Gia_Man_t *         Gia_ManDupFlip( Gia_Man_t * p, int * pInitState );
 extern Gia_Man_t *         Gia_ManDupCycled( Gia_Man_t * pAig, int nFrames );
@@ -983,6 +984,7 @@ extern Gia_Man_t *         Gia_ManDupWithBoxes( Gia_Man_t * p, Gia_Man_t * pBoxe
 extern int                 Gia_ManLevelWithBoxes( Gia_Man_t * p );
 extern int                 Gia_ManVerifyWithBoxes( Gia_Man_t * pGia, void * pParsInit );
 extern void *              Gia_ManUpdateTimMan( Gia_Man_t * p, Vec_Int_t * vBoxPres );
+extern Gia_Man_t *         Gia_ManUpdateExtraAig( void * pTime, Gia_Man_t * pAig, Vec_Int_t * vBoxPres );
 /*=== giaTruth.c ===========================================================*/
 extern word                Gia_ObjComputeTruthTable6( Gia_Man_t * p, Gia_Obj_t * pObj, Vec_Int_t * vSupp, Vec_Wrd_t * vTruths );
 extern int                 Gia_ObjCollectInternal( Gia_Man_t * p, Gia_Obj_t * pObj );
diff --git a/src/aig/gia/giaDup.c b/src/aig/gia/giaDup.c
index 735bd566..c23cc555 100644
--- a/src/aig/gia/giaDup.c
+++ b/src/aig/gia/giaDup.c
@@ -220,6 +220,40 @@ Gia_Man_t * Gia_ManDupOutputGroup( Gia_Man_t * p, int iOutStart, int iOutStop )
 
 /**Function*************************************************************
 
+  Synopsis    [Duplicates AIG while putting objects in the DFS order.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Gia_Man_t * Gia_ManDupOutputVec( Gia_Man_t * p, Vec_Int_t * vOutPres )
+{
+    Gia_Man_t * pNew;
+    Gia_Obj_t * pObj;
+    int i;
+    assert( Gia_ManRegNum(p) == 0 );
+    assert( Gia_ManPoNum(p) == Vec_IntSize(vOutPres) );
+    Gia_ManFillValue( p );
+    pNew = Gia_ManStart( Gia_ManObjNum(p) );
+    pNew->pName = Abc_UtilStrsav( p->pName );
+    pNew->pSpec = Abc_UtilStrsav( p->pSpec );
+    Gia_ManConst0(p)->Value = 0;
+    Gia_ManForEachPi( p, pObj, i )
+        pObj->Value = Gia_ManAppendCi(pNew);
+    Gia_ManForEachPo( p, pObj, i )
+        if ( Vec_IntEntry(vOutPres, i) )
+            Gia_ManDupOrderDfs_rec( pNew, p, pObj );
+    Gia_ManForEachPo( p, pObj, i )
+        if ( Vec_IntEntry(vOutPres, i) )
+            pObj->Value = Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) );
+    return pNew;
+}
+
+/**Function*************************************************************
+
   Synopsis    [Duplicates the AIG in the DFS order.]
 
   Description []
diff --git a/src/aig/gia/giaSweep.c b/src/aig/gia/giaSweep.c
index 4ed7d3db..fe4c275c 100644
--- a/src/aig/gia/giaSweep.c
+++ b/src/aig/gia/giaSweep.c
@@ -35,18 +35,6 @@ ABC_NAMESPACE_IMPL_START
 
 /**Function*************************************************************
 
-  Synopsis    []
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-
-/**Function*************************************************************
-
   Synopsis    [Mark GIA nodes that feed into POs.]
 
   Description []
@@ -140,6 +128,10 @@ Gia_Man_t * Gia_ManFraigCreateGia( Gia_Man_t * p )
     }
     // update timing manager
     pNew->pManTime = Gia_ManUpdateTimMan( p, vBoxPres );
+    // update extra STG
+    assert( p->pAigExtra != NULL );
+    assert( pNew->pAigExtra == NULL );
+    pNew->pAigExtra = Gia_ManUpdateExtraAig( p->pManTime, p->pAigExtra, vBoxPres );
     Vec_IntFree( vBoxPres );
     return pNew;
 }
@@ -161,7 +153,7 @@ int Gia_ObjFanin0CopyRepr( Gia_Man_t * p, Gia_Obj_t * pObj, int * pReprs )
     if ( pReprs[faninId] == -1 )
         return Gia_ObjFanin0Copy( pObj );
     assert( Abc_Lit2Var(pReprs[faninId]) < Gia_ObjId(p, pObj) );
-    return Abc_LitNotCond( Gia_ObjValue(Gia_ManObj(p, Abc_Lit2Var(pReprs[faninId]))), Abc_LitIsCompl(pReprs[faninId]) );
+    return Abc_LitNotCond( Gia_ObjValue(Gia_ManObj(p, Abc_Lit2Var(pReprs[faninId]))), Gia_ObjFaninC0(pObj) ^ Abc_LitIsCompl(pReprs[faninId]) );
 }
 int Gia_ObjFanin1CopyRepr( Gia_Man_t * p, Gia_Obj_t * pObj, int * pReprs )
 {
@@ -169,7 +161,7 @@ int Gia_ObjFanin1CopyRepr( Gia_Man_t * p, Gia_Obj_t * pObj, int * pReprs )
     if ( pReprs[faninId] == -1 )
         return Gia_ObjFanin1Copy( pObj );
     assert( Abc_Lit2Var(pReprs[faninId]) < Gia_ObjId(p, pObj) );
-    return Abc_LitNotCond( Gia_ObjValue(Gia_ManObj(p, Abc_Lit2Var(pReprs[faninId]))), Abc_LitIsCompl(pReprs[faninId]) );
+    return Abc_LitNotCond( Gia_ObjValue(Gia_ManObj(p, Abc_Lit2Var(pReprs[faninId]))), Gia_ObjFaninC1(pObj) ^ Abc_LitIsCompl(pReprs[faninId]) );
 }
 Gia_Man_t * Gia_ManFraigReduceGia( Gia_Man_t * p, int * pReprs )
 {
@@ -201,52 +193,6 @@ Gia_Man_t * Gia_ManFraigReduceGia( Gia_Man_t * p, int * pReprs )
 
 /**Function*************************************************************
 
-  Synopsis    []
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-Gia_Man_t * Gia_ManFraigReduceGia2( Gia_Man_t * p, int * pReprs )
-{
-    Gia_Man_t * pNew;
-    Gia_Obj_t * pObj;
-    int i;
-    assert( p->pSibls == NULL );
-    assert( Gia_ManRegNum(p) == 0 );
-    pNew = Gia_ManStart( Gia_ManObjNum(p) );
-    pNew->pName = Abc_UtilStrsav( p->pName );
-    pNew->pSpec = Abc_UtilStrsav( p->pSpec );
-    Gia_ManHashAlloc( pNew );
-    // copy const and real PIs
-    Gia_ManFillValue( p );
-    Gia_ManForEachObj( p, pObj, i )
-    {
-        if ( Gia_ObjIsAnd(pObj) )
-        {
-            assert( pReprs[i] == -1 || Abc_Lit2Var(pReprs[i]) < i );
-            if ( pReprs[i] == -1 )
-                pObj->Value = Gia_ManAppendAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) );
-            else
-                pObj->Value = Abc_LitNotCond( Gia_ObjValue(Gia_ManObj(p, Abc_Lit2Var(pReprs[i]))), Abc_LitIsCompl(pReprs[i]) );
-        }
-        else if ( Gia_ObjIsCi(pObj) )
-            pObj->Value = Gia_ManAppendCi( pNew );
-        else if ( Gia_ObjIsCo(pObj) )
-            pObj->Value = Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) );
-        else if ( Gia_ObjIsConst0(pObj) )
-            pObj->Value = 0;
-        else assert( 0 );
-    }
-    Gia_ManHashStop( pNew );
-    return pNew;
-}
-
-/**Function*************************************************************
-
   Synopsis    [Computes representatives in terms of the original objects.]
 
   Description []
@@ -264,6 +210,17 @@ int * Gia_ManFraigSelectReprs( Gia_Man_t * p, Gia_Man_t * pGia, int fVerbose )
     int i, iLitGia, iLitGia2, iReprGia, fCompl;
     int nConsts = 0, nReprs = 0;
     pGia2Abc[0] = 0;
+/*
+    Gia_ManForEachObj( p, pObj, i )
+        printf( "%d %d  ", i, Gia_ObjValue(pObj) );
+    printf( "\n" );
+    printf( "\n" );
+
+    Gia_ManForEachObj( pGia, pObj, i )
+        printf( "%d %d  ", i, Gia_ObjReprSelf(pGia, i) );
+    printf( "\n" );
+    printf( "\n" );
+*/
     Gia_ManSetPhase( pGia );
     Gia_ManForEachObj1( p, pObj, i )
     {
@@ -292,7 +249,7 @@ int * Gia_ManFraigSelectReprs( Gia_Man_t * p, Gia_Man_t * pGia, int fVerbose )
         }
     }
     ABC_FREE( pGia2Abc );
-    if ( fVerbose )
+//    if ( fVerbose )
         printf( "Found %d const reprs and %d other reprs.\n", nConsts, nReprs );
     return pReprs;
 }
@@ -351,8 +308,13 @@ Gia_Man_t * Gia_ManFraigSweep( Gia_Man_t * p, void * pPars )
     pNew = Gia_ManDupWithHierarchy( p, NULL );
     if ( pNew == NULL )
         return NULL;
+    // normalizing AIG
+    pNew = Gia_ManDupNormalize( pTemp = pNew );
+    Gia_ManStop( pTemp );
     // find global equivalences
-    pGia = Gia_ManDupWithBoxes( p, p->pAigExtra );
+    pNew->pManTime = p->pManTime;
+    pGia = Gia_ManDupWithBoxes( pNew, p->pAigExtra );
+    pNew->pManTime = NULL;
     Gia_ManFraigSweepPerform( pGia, pPars );
     // transfer equivalences
     pReprs = Gia_ManFraigSelectReprs( pNew, pGia, ((Dch_Pars_t *)pPars)->fVerbose );
@@ -366,11 +328,22 @@ Gia_Man_t * Gia_ManFraigSweep( Gia_Man_t * p, void * pPars )
     pNew = Gia_ManDupWithHierarchy( pTemp = pNew, NULL );
     pTemp->pManTime = NULL;
     Gia_ManStop( pTemp );
+    if ( pNew == NULL )
+        return NULL;
     // derive new AIG
-    assert( pTemp->pManTime == NULL );
+    assert( pNew->pManTime  == NULL );
+    assert( pNew->pAigExtra == NULL );
+    pNew->pManTime  = p->pManTime;
+    pNew->pAigExtra = p->pAigExtra;
     pNew = Gia_ManFraigCreateGia( pTemp = pNew );
-    assert( pNew->pManTime != NULL );
+    assert( pTemp->pManTime  == p->pManTime );
+    assert( pTemp->pAigExtra == p->pAigExtra );
+    pTemp->pManTime = NULL;
+    pTemp->pAigExtra = NULL;
     Gia_ManStop( pTemp );
+    // return the result
+    assert( pNew->pManTime  != NULL );
+    assert( pNew->pAigExtra != NULL );
     return pNew;
 }
 
diff --git a/src/aig/gia/giaTim.c b/src/aig/gia/giaTim.c
index 6a7f22a9..5d08b783 100644
--- a/src/aig/gia/giaTim.c
+++ b/src/aig/gia/giaTim.c
@@ -233,14 +233,14 @@ Vec_Int_t * Gia_ManDupFindOrderWithHie( Gia_Man_t * p )
             {
                 int iCiNum = (int)(ABC_PTRUINT_T)p->pData2;
                 int iBoxNum = Tim_ManBoxFindFromCiNum( p->pManTime, iCiNum );
-                printf( "Boxes are not in a topological order. The program has to terminate.\n" );
-                printf( "The following information about the network may help the debugging:\n" );
-                printf( "Input %d of BoxA %d (1CI = %d; 1CO = %d) has TFI with CI %d,\n", 
+                printf( "Boxes are not in a topological order. The command has to terminate.\n" );
+                printf( "The following information may help debugging (numbers are 0-based):\n" );
+                printf( "Input %d of BoxA %d (1stCI = %d; 1stCO = %d) has TFI with CI %d,\n", 
                     k, i, Tim_ManBoxOutputFirst(p->pManTime, i), Tim_ManBoxInputFirst(p->pManTime, i), iCiNum );
-                printf( "which corresponds to output %d of BoxB %d (1CI = %d; 1CO = %d).\n", 
+                printf( "which corresponds to output %d of BoxB %d (1stCI = %d; 1stCO = %d).\n", 
                     iCiNum - Tim_ManBoxOutputFirst(p->pManTime, iBoxNum), iBoxNum, 
                     Tim_ManBoxOutputFirst(p->pManTime, iBoxNum), Tim_ManBoxInputFirst(p->pManTime, iBoxNum) );
-                printf( "In a correct topological order, BoxB preceeds BoxA (numbers are 0-based).\n" );
+                printf( "In a correct topological order, BoxB should preceed BoxA.\n" );
                 Vec_IntFree( vNodes );
                 p->pData2 = NULL;
                 return NULL;
@@ -336,6 +336,34 @@ Gia_Man_t * Gia_ManDupWithHierarchy( Gia_Man_t * p, Vec_Int_t ** pvNodes )
 
 /**Function*************************************************************
 
+  Synopsis    [Remaps the AIG from the old manager into the new manager.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Gia_ManCleanupRemap( Gia_Man_t * p, Gia_Man_t * pGia )
+{
+    Gia_Obj_t * pObj, * pObjGia;
+    int i, iPrev;
+    Gia_ManForEachObj1( p, pObj, i )
+    {
+        iPrev = Gia_ObjValue(pObj);
+        if ( iPrev == ~0 )
+            continue;
+        pObjGia = Gia_ManObj( pGia, Abc_Lit2Var(iPrev) );
+        if ( pObjGia->Value == ~0 )
+            Gia_ObjSetValue( pObj, pObjGia->Value ); 
+        else
+            Gia_ObjSetValue( pObj, Abc_LitNotCond(pObjGia->Value, Abc_LitIsCompl(iPrev)) );
+    }
+}
+
+/**Function*************************************************************
+
   Synopsis    []
 
   Description []
@@ -433,6 +461,7 @@ Gia_Man_t * Gia_ManDupWithBoxes( Gia_Man_t * p, Gia_Man_t * pBoxes )
     Gia_ManSetRegNum( pNew, Gia_ManRegNum(p) );
     Gia_ManHashStop( pNew );
     pNew = Gia_ManCleanup( pTemp = pNew );
+    Gia_ManCleanupRemap( p, pTemp );
     Gia_ManStop( pTemp );
     assert( Tim_ManPoNum(pTime) == Gia_ManPoNum(pNew) );
     assert( Tim_ManPiNum(pTime) == Gia_ManPiNum(pNew) );
@@ -613,6 +642,38 @@ void * Gia_ManUpdateTimMan( Gia_Man_t * p, Vec_Int_t * vBoxPres )
 
 }
 
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Gia_Man_t * Gia_ManUpdateExtraAig( void * pTime, Gia_Man_t * pAig, Vec_Int_t * vBoxPres )
+{
+    Gia_Man_t * pNew;
+    Vec_Int_t * vOutPres;
+    Tim_Man_t * pManTime = (Tim_Man_t *)pTime;
+    int i, k, curPo;
+    assert( Vec_IntSize(vBoxPres) == Tim_ManBoxNum(pManTime) );
+    assert( Gia_ManPoNum(pAig) == Tim_ManCoNum(pManTime) - Tim_ManPoNum(pManTime) );
+    vOutPres = Vec_IntAlloc( 100 );
+    for ( curPo = i = 0; i < Tim_ManBoxNum(pManTime); i++, curPo += Tim_ManBoxInputNum(pManTime, i) )
+        if ( Vec_IntEntry(vBoxPres, i) )
+            for ( k = 0; k < Tim_ManBoxInputNum(pManTime, i); k++ )
+                Vec_IntPush( vOutPres, curPo + k );
+    assert( curPo == Tim_ManCoNum(pManTime) - Tim_ManPoNum(pManTime) );
+    for ( k = curPo; k < Tim_ManCoNum(pManTime); k++ )
+        Vec_IntPush( vOutPres, k );
+    pNew = Gia_ManDupOutputVec( pAig, vOutPres );
+    Vec_IntFree( vOutPres );
+    return pNew;
+}
+
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////