Version abc60611

13 files changed, 112 insertions, 20 deletions

diff --git a/src/misc/extra/extra.h b/src/misc/extra/extra.h
index 6336f5ea..d404dbc6 100644
--- a/src/misc/extra/extra.h
+++ b/src/misc/extra/extra.h
@@ -464,9 +464,8 @@ extern unsigned Extra_TruthSemiCanonicize( unsigned * pInOut, unsigned * pAux, i
 #define ALLOC(type, num)     ((type *) malloc(sizeof(type) * (num)))
 #define FREE(obj)             ((obj) ? (free((char *) (obj)), (obj) = 0) : 0)
 #define REALLOC(type, obj, num)    \
-        (obj) ? ((type *) realloc((char *) obj, sizeof(type) * (num))) : \
-        ((type *) malloc(sizeof(type) * (num)))
-
+        ((obj) ? ((type *) realloc((char *)(obj), sizeof(type) * (num))) : \
+         ((type *) malloc(sizeof(type) * (num))))
 
 extern long        Extra_CpuTime();
 extern int         Extra_GetSoftDataLimit();
diff --git a/src/misc/extra/extraUtilBitMatrix.c b/src/misc/extra/extraUtilBitMatrix.c
index 93cbbeac..b860a538 100644
--- a/src/misc/extra/extraUtilBitMatrix.c
+++ b/src/misc/extra/extraUtilBitMatrix.c
@@ -348,7 +348,7 @@ int Extra_BitMatrixCountOnesUpper( Extra_BitMat_t * p )
     int i, k, nTotal = 0;
     for ( i = 0; i < p->nSize; i++ )
         for ( k = i + 1; k < p->nSize; k++ )
-            nTotal += ( (p->ppData[i][k/32] & (1 << (k%32))) > 0 );
+            nTotal += ( (p->ppData[i][k>>5] & (1 << (k&31))) > 0 );
     return nTotal;
 }
 
diff --git a/src/misc/extra/extraUtilMisc.c b/src/misc/extra/extraUtilMisc.c
index bd7f19ec..f62de314 100644
--- a/src/misc/extra/extraUtilMisc.c
+++ b/src/misc/extra/extraUtilMisc.c
@@ -1323,9 +1323,9 @@ void Extra_TruthExpand( int nVars, int nWords, unsigned * puTruth, unsigned uPha
         { 0xF0F0F0F0,0xF0F0F0F0,0xF0F0F0F0,0xF0F0F0F0,0xF0F0F0F0,0xF0F0F0F0,0xF0F0F0F0,0xF0F0F0F0 },
         { 0xFF00FF00,0xFF00FF00,0xFF00FF00,0xFF00FF00,0xFF00FF00,0xFF00FF00,0xFF00FF00,0xFF00FF00 },
         { 0xFFFF0000,0xFFFF0000,0xFFFF0000,0xFFFF0000,0xFFFF0000,0xFFFF0000,0xFFFF0000,0xFFFF0000 }, 
-        { 0xFFFFFFFF,0x00000000,0xFFFFFFFF,0x00000000,0xFFFFFFFF,0x00000000,0xFFFFFFFF,0x00000000 }, 
-        { 0xFFFFFFFF,0xFFFFFFFF,0x00000000,0x00000000,0xFFFFFFFF,0xFFFFFFFF,0x00000000,0x00000000 }, 
-        { 0xFFFFFFFF,0xFFFFFFFF,0xFFFFFFFF,0xFFFFFFFF,0x00000000,0x00000000,0x00000000,0x00000000 } 
+        { 0x00000000,0xFFFFFFFF,0x00000000,0xFFFFFFFF,0x00000000,0xFFFFFFFF,0x00000000,0xFFFFFFFF }, 
+        { 0x00000000,0x00000000,0xFFFFFFFF,0xFFFFFFFF,0x00000000,0x00000000,0xFFFFFFFF,0xFFFFFFFF }, 
+        { 0x00000000,0x00000000,0x00000000,0x00000000,0xFFFFFFFF,0xFFFFFFFF,0xFFFFFFFF,0xFFFFFFFF } 
     };
     static char Cases[256] = {
          0, // 00000000
@@ -1922,12 +1922,12 @@ void Extra_TruthExpand( int nVars, int nWords, unsigned * puTruth, unsigned uPha
             puTruthR[i] = 0;
         nMints = (1 << nVars);
         for ( i = 0; i < nMints; i++ )
-            if ( puTruth[i/32] & (1 << (i%32)) )
+            if ( puTruth[i>>5] & (1 << (i&31)) )
             {
                 for ( iRes = 0, k = 0; k < 5; k++ )
                     if ( i & (1 << pPerm[k]) )
                         iRes |= (1 << k);
-                puTruthR[iRes/32] |= (1 << (iRes%32));
+                puTruthR[iRes>>5] |= (1 << (iRes&31));
             }
     }
 }
@@ -2058,9 +2058,9 @@ unsigned ** Extra_Truths8()
         { 0xF0F0F0F0,0xF0F0F0F0,0xF0F0F0F0,0xF0F0F0F0,0xF0F0F0F0,0xF0F0F0F0,0xF0F0F0F0,0xF0F0F0F0 },
         { 0xFF00FF00,0xFF00FF00,0xFF00FF00,0xFF00FF00,0xFF00FF00,0xFF00FF00,0xFF00FF00,0xFF00FF00 },
         { 0xFFFF0000,0xFFFF0000,0xFFFF0000,0xFFFF0000,0xFFFF0000,0xFFFF0000,0xFFFF0000,0xFFFF0000 }, 
-        { 0xFFFFFFFF,0x00000000,0xFFFFFFFF,0x00000000,0xFFFFFFFF,0x00000000,0xFFFFFFFF,0x00000000 }, 
-        { 0xFFFFFFFF,0xFFFFFFFF,0x00000000,0x00000000,0xFFFFFFFF,0xFFFFFFFF,0x00000000,0x00000000 }, 
-        { 0xFFFFFFFF,0xFFFFFFFF,0xFFFFFFFF,0xFFFFFFFF,0x00000000,0x00000000,0x00000000,0x00000000 } 
+        { 0x00000000,0xFFFFFFFF,0x00000000,0xFFFFFFFF,0x00000000,0xFFFFFFFF,0x00000000,0xFFFFFFFF }, 
+        { 0x00000000,0x00000000,0xFFFFFFFF,0xFFFFFFFF,0x00000000,0x00000000,0xFFFFFFFF,0xFFFFFFFF }, 
+        { 0x00000000,0x00000000,0x00000000,0x00000000,0xFFFFFFFF,0xFFFFFFFF,0xFFFFFFFF,0xFFFFFFFF } 
     };
     static unsigned * puResult[8] = {
         uTruths[0], uTruths[1], uTruths[2], uTruths[3], uTruths[4], uTruths[5], uTruths[6], uTruths[7] 
diff --git a/src/misc/extra/extraUtilTruth.c b/src/misc/extra/extraUtilTruth.c
index 74308ab2..a0c58025 100644
--- a/src/misc/extra/extraUtilTruth.c
+++ b/src/misc/extra/extraUtilTruth.c
@@ -264,15 +264,15 @@ DdNode * Extra_TruthToBdd_rec( DdManager * dd, unsigned * pTruth, int iBit, int
     DdNode * bF0, * bF1, * bF;
     if ( nVars == 0 )
     {
-        if ( pTruth[iBit/32] & (1 << iBit%32) )
+        if ( pTruth[iBit>>5] & (1 << iBit&31) )
             return b1;
         return b0;
     }
     if ( nVars == 5 )
     {
-        if ( pTruth[iBit/32] == 0xFFFFFFFF )
+        if ( pTruth[iBit>>5] == 0xFFFFFFFF )
             return b1;
-        if ( pTruth[iBit/32] == 0 )
+        if ( pTruth[iBit>>5] == 0 )
             return b0;
     }
     // other special cases can be added
diff --git a/src/misc/mvc/mvc.h b/src/misc/mvc/mvc.h
index 650f698d..70834e0a 100644
--- a/src/misc/mvc/mvc.h
+++ b/src/misc/mvc/mvc.h
@@ -49,7 +49,7 @@
 ////////////////////////////////////////////////////////////////////////
 
 // cube/list/cover/data
-typedef unsigned long              Mvc_CubeWord_t;
+typedef unsigned int               Mvc_CubeWord_t;
 typedef struct MvcCubeStruct       Mvc_Cube_t;
 typedef struct MvcListStruct       Mvc_List_t;
 typedef struct MvcCoverStruct      Mvc_Cover_t;
diff --git a/src/misc/nm/module.make b/src/misc/nm/module.make
new file mode 100644
index 00000000..2a3820c7
--- /dev/null
+++ b/src/misc/nm/module.make
@@ -0,0 +1,2 @@
+SRC +=  src/misc/nm/nmApi.c \
+    src/misc/nm/nmTable.c
diff --git a/src/misc/nm/nm.h b/src/misc/nm/nm.h
index 5b17aaed..9c96c8ba 100644
--- a/src/misc/nm/nm.h
+++ b/src/misc/nm/nm.h
@@ -52,10 +52,12 @@ extern Nm_Man_t *   Nm_ManCreate( int nSize );
 extern void         Nm_ManFree( Nm_Man_t * p );
 extern int          Nm_ManNumEntries( Nm_Man_t * p );
 extern char *       Nm_ManStoreIdName( Nm_Man_t * p, int ObjId, char * pName, char * pSuffix );
+extern void         Nm_ManDeleteIdName( Nm_Man_t * p, int ObjId );
 extern char *       Nm_ManCreateUniqueName( Nm_Man_t * p, int ObjId );
 extern char *       Nm_ManFindNameById( Nm_Man_t * p, int ObjId );
 extern int          Nm_ManFindIdByName( Nm_Man_t * p, char * pName, int * pSecond );
 extern void         Nm_ManPrintTables( Nm_Man_t * p );
+extern Vec_Int_t *  Nm_ManReturnNameIds( Nm_Man_t * p );
 
 #ifdef __cplusplus
 }
diff --git a/src/misc/nm/nmApi.c b/src/misc/nm/nmApi.c
index 72ec24e6..3a9ac074 100644
--- a/src/misc/nm/nmApi.c
+++ b/src/misc/nm/nmApi.c
@@ -135,6 +135,31 @@ char * Nm_ManStoreIdName( Nm_Man_t * p, int ObjId, char * pName, char * pSuffix
     return pEntry->Name;
 }
 
+/**Function*************************************************************
+
+  Synopsis    [Creates a new entry in the name manager.]
+
+  Description [Returns 1 if the entry with the given object ID
+  already exists in the name manager.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Nm_ManDeleteIdName( Nm_Man_t * p, int ObjId )
+{
+    Nm_Entry_t * pEntry;
+    pEntry = Nm_ManTableLookupId(p, ObjId);
+    if ( pEntry == NULL )
+    {
+        printf( "Nm_ManDeleteIdName(): This entry is not in the table.\n" );
+        return;
+    }
+    // remove entry from the table
+    Nm_ManTableDelete( p, pEntry );
+}
+
 
 /**Function*************************************************************
 
@@ -255,6 +280,28 @@ void Nm_ManPrintTables( Nm_Man_t * p )
     printf( "\n" );
 }
 
+/**Function*************************************************************
+
+  Synopsis    [Return the IDs of objects with names.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Vec_Int_t * Nm_ManReturnNameIds( Nm_Man_t * p )
+{
+    Vec_Int_t * vNameIds;
+    int i;
+    vNameIds = Vec_IntAlloc( p->nEntries );
+    for ( i = 0; i < p->nBins; i++ )
+        if ( p->pBinsI2N[i] )
+            Vec_IntPush( vNameIds, p->pBinsI2N[i]->ObjId );
+    return vNameIds;
+}
+
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////
diff --git a/src/misc/nm/nmInt.h b/src/misc/nm/nmInt.h
index d0475c23..43901993 100644
--- a/src/misc/nm/nmInt.h
+++ b/src/misc/nm/nmInt.h
@@ -30,6 +30,7 @@ extern "C" {
 ////////////////////////////////////////////////////////////////////////
 
 #include "extra.h"
+#include "vec.h"
 #include "nm.h"
 
 ////////////////////////////////////////////////////////////////////////
diff --git a/src/misc/util/util_hack.h b/src/misc/util/util_hack.h
index a9b90e61..71c77321 100644
--- a/src/misc/util/util_hack.h
+++ b/src/misc/util/util_hack.h
@@ -73,8 +73,8 @@ extern "C" {
 #define ALLOC(type, num)       ((type *) malloc(sizeof(type) * (num)))
 #define FREE(obj)              ((obj) ? (free((char *) (obj)), (obj) = 0) : 0)
 #define REALLOC(type, obj, num) \
-        (obj) ? ((type *) realloc((char *) obj, sizeof(type) * (num))) : \
-        ((type *) malloc(sizeof(type) * (num)))
+        ((obj) ? ((type *) realloc((char *)(obj), sizeof(type) * (num))) : \
+        ((type *) malloc(sizeof(type) * (num))))
 
 extern long        Extra_CpuTime();
 extern int         Extra_GetSoftDataLimit();
diff --git a/src/misc/vec/vecInt.h b/src/misc/vec/vecInt.h
index 5a627623..fd8dbc86 100644
--- a/src/misc/vec/vecInt.h
+++ b/src/misc/vec/vecInt.h
@@ -540,6 +540,27 @@ static inline void Vec_IntPushOrder( Vec_Int_t * p, int Entry )
 
 /**Function*************************************************************
 
+  Synopsis    [Inserts the entry while preserving the increasing order.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline int Vec_IntPushUniqueOrder( Vec_Int_t * p, int Entry )
+{
+    int i;
+    for ( i = 0; i < p->nSize; i++ )
+        if ( p->pArray[i] == Entry )
+            return 1;
+    Vec_IntPushOrder( p, Entry );
+    return 0;
+}
+
+/**Function*************************************************************
+
   Synopsis    []
 
   Description []
diff --git a/src/misc/vec/vecPtr.h b/src/misc/vec/vecPtr.h
index 65314af6..63dcc9b8 100644
--- a/src/misc/vec/vecPtr.h
+++ b/src/misc/vec/vecPtr.h
@@ -472,6 +472,26 @@ static inline void * Vec_PtrPop( Vec_Ptr_t * p )
 
 /**Function*************************************************************
 
+  Synopsis    [Find entry.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline int Vec_PtrFind( Vec_Ptr_t * p, void * Entry )
+{
+    int i;
+    for ( i = 0; i < p->nSize; i++ )
+        if ( p->pArray[i] == Entry )
+            return i;
+    return -1;
+}
+
+/**Function*************************************************************
+
   Synopsis    []
 
   Description []
diff --git a/src/misc/vec/vecStr.h b/src/misc/vec/vecStr.h
index 5549d374..4cda06f0 100644
--- a/src/misc/vec/vecStr.h
+++ b/src/misc/vec/vecStr.h
@@ -494,10 +494,10 @@ static inline int Vec_StrSortCompare2( char * pp1, char * pp2 )
 static inline void Vec_StrSort( Vec_Str_t * p, int fReverse )
 {
     if ( fReverse ) 
-        qsort( (void *)p->pArray, p->nSize, sizeof(int), 
+        qsort( (void *)p->pArray, p->nSize, sizeof(char), 
                 (int (*)(const void *, const void *)) Vec_StrSortCompare2 );
     else
-        qsort( (void *)p->pArray, p->nSize, sizeof(int), 
+        qsort( (void *)p->pArray, p->nSize, sizeof(char), 
                 (int (*)(const void *, const void *)) Vec_StrSortCompare1 );
 }