Cleaning up boolean operators; adding unique name support; minor changes.

3 files changed, 101 insertions, 34 deletions

diff --git a/src/base/cba/cba.h b/src/base/cba/cba.h
index 0086d031..8ae9a81c 100644
--- a/src/base/cba/cba.h
+++ b/src/base/cba/cba.h
@@ -630,33 +630,6 @@ static inline Vec_Int_t * Cba_NtkCollect( Cba_Ntk_t * p )
         Vec_IntPush( vObjs, iObj );
     return vObjs;
 }
-static inline void Cba_NtkCreateFonNames( Cba_Ntk_t * p, char * pPref )
-{
-    int i, iObj, iFon, NameId;
-    Cba_NtkCleanFonNames( p );
-    Cba_NtkForEachPiFon( p, iObj, iFon, i )
-        if ( !Cba_FonName(p, iFon) )
-            Cba_FonSetName( p, iFon, Cba_ObjName(p, iObj) );
-    Cba_NtkForEachPoDriverFon( p, iObj, iFon, i )
-        if ( Cba_FonIsReal(iFon) && !Cba_FonName(p, iFon) )
-            Cba_FonSetName( p, iFon, Cba_ObjName(p, iObj) );
-    Vec_IntForEachEntryStart( &p->vFonName, NameId, iFon, 1 )
-        if ( NameId == 0 )
-            Vec_IntWriteEntry( &p->vFonName, iFon, Cba_NtkNewStrId(p, "%s%d", pPref, iFon) );
-}
-static inline void Cba_NtkMissingFonNames( Cba_Ntk_t * p, char * pPref )
-{
-    int i, iObj, iFon, NameId;
-    Cba_NtkForEachPiFon( p, iObj, iFon, i )
-        if ( !Cba_FonName(p, iFon) )
-            Cba_FonSetName( p, iFon, Cba_ObjName(p, iObj) );
-    Cba_NtkForEachPoDriverFon( p, iObj, iFon, i )
-        if ( Cba_FonIsReal(iFon) && !Cba_FonName(p, iFon) )
-            Cba_FonSetName( p, iFon, Cba_ObjName(p, iObj) );
-    Vec_IntForEachEntryStart( &p->vFonName, NameId, iFon, 1 )
-        if ( NameId == 0 )
-            Cba_FonSetName( p, iFon, Cba_NtkNewStrId(p, "%s%d", pPref, iFon) );
-}
 static inline int Cba_NtkIsSeq( Cba_Ntk_t * p )
 {
     int iObj;
@@ -1046,6 +1019,68 @@ static inline void Cba_ManPrintStats( Cba_Man_t * p, int nModules, int fVerbose
 }
 
 
+/**Function*************************************************************
+
+  Synopsis    [Name handling.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline void Cba_NtkAddMissingFonNames( Cba_Ntk_t * p, char * pPref )
+{
+    int iFon, NameId, Index;
+    // populate map
+    Cba_ManCleanMap( p->pDesign );
+    Vec_IntForEachEntryStart( &p->vFonName, NameId, iFon, 1 )
+        if ( NameId )
+            Cba_ManSetMap( p->pDesign, NameId, iFon );
+    // check remaining ones
+    Vec_IntForEachEntryStart( &p->vFonName, NameId, iFon, 1 )
+    {
+        if ( NameId )
+            continue;
+        NameId = Cba_NtkNewStrId(p, "%s%d", pPref, iFon);
+        for ( Index = 1; Cba_ManGetMap(p->pDesign, NameId); Index++ )
+            NameId = Cba_NtkNewStrId(p, "%s%d_%d", pPref, iFon, Index);
+        Cba_FonSetName( p, iFon, NameId );
+        Cba_ManSetMap( p->pDesign, NameId, iFon );
+    }
+}
+static inline void Cba_NtkCreateFonNames( Cba_Ntk_t * p, char * pPref )
+{
+    int i, iObj, iFon;//, NameId;
+    Cba_NtkCleanFonNames( p );
+    Cba_NtkForEachPiFon( p, iObj, iFon, i )
+        if ( !Cba_FonName(p, iFon) )
+            Cba_FonSetName( p, iFon, Cba_ObjName(p, iObj) );
+    Cba_NtkForEachPoDriverFon( p, iObj, iFon, i )
+        if ( Cba_FonIsReal(iFon) && !Cba_FonName(p, iFon) )
+            Cba_FonSetName( p, iFon, Cba_ObjName(p, iObj) );
+//    Vec_IntForEachEntryStart( &p->vFonName, NameId, iFon, 1 )
+//        if ( NameId == 0 )
+//            Vec_IntWriteEntry( &p->vFonName, iFon, Cba_NtkNewStrId(p, "%s%d", pPref, iFon) );
+    Cba_NtkAddMissingFonNames( p, pPref );
+}
+static inline void Cba_NtkMissingFonNames( Cba_Ntk_t * p, char * pPref )
+{
+    int i, iObj, iFon;//, NameId;
+    Cba_NtkForEachPiFon( p, iObj, iFon, i )
+        if ( !Cba_FonName(p, iFon) )
+            Cba_FonSetName( p, iFon, Cba_ObjName(p, iObj) );
+    Cba_NtkForEachPoDriverFon( p, iObj, iFon, i )
+        if ( Cba_FonIsReal(iFon) && !Cba_FonName(p, iFon) )
+            Cba_FonSetName( p, iFon, Cba_ObjName(p, iObj) );
+//    Vec_IntForEachEntryStart( &p->vFonName, NameId, iFon, 1 )
+//        if ( NameId == 0 )
+//            Cba_FonSetName( p, iFon, Cba_NtkNewStrId(p, "%s%d", pPref, iFon) );
+    Cba_NtkAddMissingFonNames( p, pPref );
+}
+
+
 /*=== cbaBlast.c =============================================================*/
 extern Gia_Man_t *   Cba_ManBlast( Cba_Man_t * p, int fBarBufs, int fSeq, int fVerbose );
 extern Cba_Man_t *   Cba_ManInsertGia( Cba_Man_t * p, Gia_Man_t * pGia );
@@ -1066,7 +1101,7 @@ extern int           Cba_NtkCoFinNum( Cba_Ntk_t * p );
 extern int           Cba_NtkCheckComboLoop( Cba_Ntk_t * p );
 extern int           Cba_ManIsTopoOrder( Cba_Man_t * p );
 extern Vec_Int_t *   Cba_NtkCollectDfs( Cba_Ntk_t * p );
-extern Cba_Man_t *   Cba_ManCollapse( Cba_Man_t * p, int TypeBuf );
+extern Cba_Man_t *   Cba_ManCollapse( Cba_Man_t * p );
 extern Cba_Man_t *   Cba_ManExtractGroup( Cba_Man_t * p, Vec_Int_t * vObjs );
 extern Cba_Man_t *   Cba_ManDeriveFromGia( Gia_Man_t * pGia, int fUseXor );
 extern Cba_Man_t *   Cba_ManInsertGroup( Cba_Man_t * p, Vec_Int_t * vObjs, Cba_Ntk_t * pSyn );
diff --git a/src/base/cba/cbaCom.c b/src/base/cba/cbaCom.c
index 9605975a..0d3868b3 100644
--- a/src/base/cba/cbaCom.c
+++ b/src/base/cba/cbaCom.c
@@ -498,7 +498,7 @@ int Cba_CommandClp( Abc_Frame_t * pAbc, int argc, char ** argv )
         Abc_Print( 1, "Cba_CommandGet(): There is no current design.\n" );
         return 0;
     }
-    pNew = Cba_ManCollapse( p, CBA_BOX_BUF );
+    pNew = Cba_ManCollapse( p );
     Cba_AbcUpdateMan( pAbc, pNew );
     return 0;
 usage:
diff --git a/src/base/cba/cbaNtk.c b/src/base/cba/cbaNtk.c
index 979b59ac..d3ed96f5 100644
--- a/src/base/cba/cbaNtk.c
+++ b/src/base/cba/cbaNtk.c
@@ -589,6 +589,33 @@ int Cba_NtkCheckComboLoop( Cba_Ntk_t * p )
 
 /**Function*************************************************************
 
+  Synopsis    [Find one missing object.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Cba_NtkFindMissing( Vec_Int_t * vObjs, int nObjs )
+{
+    Vec_Int_t * vMap = Vec_IntStartFull( nObjs + 1 );
+    int i, iObj;
+    Vec_IntForEachEntry( vObjs, iObj, i )
+        Vec_IntWriteEntry( vMap, iObj, i );
+    Vec_IntForEachEntryStart( vMap, i, iObj, 1 )
+        if ( i == -1 )
+        {
+            Vec_IntFree( vMap );
+            return iObj;
+        }
+    Vec_IntFree( vMap );
+    return -1;
+}
+
+/**Function*************************************************************
+
   Synopsis    [Collect nodes in the DFS order.]
 
   Description []
@@ -633,7 +660,12 @@ Vec_Int_t * Cba_NtkCollectDfs( Cba_Ntk_t * p )
         Vec_IntPush( vObjs, iObj );
     assert( Vec_IntSize(vObjs) <= Cba_NtkObjNum(p) );
     if ( Vec_IntSize(vObjs) != Cba_NtkObjNum(p) )
+    {
+        int iObj = Cba_NtkFindMissing( vObjs, Cba_NtkObjNum(p) );
         printf( "Warning: DSF ordering for module \"%s\" collected %d out of %d objects.\n", Cba_NtkName(p), Vec_IntSize(vObjs), Cba_NtkObjNum(p) );
+        printf( "         For example, object %d with name \"%s\" is not reachable from outputs.\n", 
+            iObj, iObj > 0 ? Cba_FonNameStr( p, Cba_ObjFon0(p, iObj) ) : "<unknown>" );
+    }
     return vObjs;
 }
 
@@ -697,7 +729,7 @@ void Cba_ManGetClpStats( Cba_Man_t * p, int * nObjs, int * nFins, int * nFons )
   SeeAlso     []
 
 ***********************************************************************/
-void Cba_NtkCollapse_rec( Cba_Ntk_t * pNew, Cba_Ntk_t * p, Vec_Int_t * vSigs, int TypeBuf )
+void Cba_NtkCollapse_rec( Cba_Ntk_t * pNew, Cba_Ntk_t * p, Vec_Int_t * vSigs )
 {
     int i, iObj, iObjNew, iFin, iFon;
     Cba_NtkCleanObjCopies( p );
@@ -720,7 +752,7 @@ void Cba_NtkCollapse_rec( Cba_Ntk_t * pNew, Cba_Ntk_t * p, Vec_Int_t * vSigs, in
         {
             Cba_ObjForEachFon( p, iObj, iFon, i )
             {
-                iObjNew = Cba_ObjAlloc( pNew, TypeBuf, 1, 1 );
+                iObjNew = Cba_ObjAlloc( pNew, CBA_BOX_BUF, 1, 1 );
                 Cba_FonSetCopy( p, iFon, Cba_ObjFon0(pNew, iObjNew) );
             }
         }
@@ -738,7 +770,7 @@ void Cba_NtkCollapse_rec( Cba_Ntk_t * pNew, Cba_Ntk_t * p, Vec_Int_t * vSigs, in
             Cba_ObjForEachFinFon( p, iObj, iFin, iFon, i )
                 Vec_IntPush( vSigs, Cba_FonCopy(p, iFon) );
             assert( Vec_IntSize(vSigs) == Cba_ObjFinNum(p, iObj) );
-            Cba_NtkCollapse_rec( pNew, Cba_ObjNtk(p, iObj), vSigs, TypeBuf );
+            Cba_NtkCollapse_rec( pNew, Cba_ObjNtk(p, iObj), vSigs );
             assert( Vec_IntSize(vSigs) == Cba_ObjFonNum(p, iObj) );
             Cba_ObjForEachFon( p, iObj, iFon, i )
             {
@@ -751,7 +783,7 @@ void Cba_NtkCollapse_rec( Cba_Ntk_t * pNew, Cba_Ntk_t * p, Vec_Int_t * vSigs, in
     Cba_NtkForEachPoDriverFon( p, iObj, iFon, i )
         Vec_IntPush( vSigs, Cba_FonCopy(p, iFon) );
 }
-Cba_Man_t * Cba_ManCollapse( Cba_Man_t * p, int TypeBuf )
+Cba_Man_t * Cba_ManCollapse( Cba_Man_t * p )
 {
     Cba_Man_t * pNew  = Cba_ManAlloc( p->pSpec, 1, Abc_NamRef(p->pStrs), Abc_NamRef(p->pFuns), Abc_NamStart(100, 24), Hash_IntManRef(p->vHash) );
     Cba_Ntk_t * pRoot = Cba_ManRoot( p ), * pRootNew;
@@ -782,7 +814,7 @@ Cba_Man_t * Cba_ManCollapse( Cba_Man_t * p, int TypeBuf )
             Cba_ObjSetAttrs( pRootNew, iObjNew, Cba_ObjAttrArray(pRoot, iObj), Cba_ObjAttrSize(pRoot, iObj) );
     }
     assert( Vec_IntSize(vSigs) == Cba_NtkPiNum(pRoot) );
-    Cba_NtkCollapse_rec( pRootNew, pRoot, vSigs, TypeBuf );
+    Cba_NtkCollapse_rec( pRootNew, pRoot, vSigs );
     assert( Vec_IntSize(vSigs) == Cba_NtkPoNum(pRoot) );
     Cba_NtkForEachPoDriverFon( pRoot, iObj, iFon, i )
     {