Version abc50809

6 files changed, 468 insertions, 3 deletions

diff --git a/src/misc/extra/extra.h b/src/misc/extra/extra.h
index 568eef7d..5913e40e 100644
--- a/src/misc/extra/extra.h
+++ b/src/misc/extra/extra.h
@@ -113,6 +113,24 @@ extern DdNode *     Extra_bddFindOneCube( DdManager * dd, DdNode * bF );
 extern DdNode *     Extra_bddGetOneCube( DdManager * dd, DdNode * bFunc );
 extern DdNode *     Extra_bddComputeRangeCube( DdManager * dd, int iStart, int iStop );
 
+/*=== extraUtilBitMatrix.c ================================================================*/
+
+typedef struct Extra_BitMat_t_ Extra_BitMat_t;
+extern Extra_BitMat_t * Extra_BitMatrixStart( int nSize );
+extern void         Extra_BitMatrixClean( Extra_BitMat_t * p );
+extern void         Extra_BitMatrixStop( Extra_BitMat_t * p );
+extern void         Extra_BitMatrixPrint( Extra_BitMat_t * p );
+extern int          Extra_BitMatrixReadSize( Extra_BitMat_t * p );
+extern void         Extra_BitMatrixInsert1( Extra_BitMat_t * p, int i, int k );
+extern int          Extra_BitMatrixLookup1( Extra_BitMat_t * p, int i, int k );
+extern void         Extra_BitMatrixDelete1( Extra_BitMat_t * p, int i, int k );
+extern void         Extra_BitMatrixInsert2( Extra_BitMat_t * p, int i, int k );
+extern int          Extra_BitMatrixLookup2( Extra_BitMat_t * p, int i, int k );
+extern void         Extra_BitMatrixDelete2( Extra_BitMat_t * p, int i, int k );
+extern void         Extra_BitMatrixOr( Extra_BitMat_t * p, int i, unsigned * pInfo );
+extern void         Extra_BitMatrixOrTwo( Extra_BitMat_t * p, int i, int j );
+extern int          Extra_BitMatrixCountOnesUpper( Extra_BitMat_t * p );
+
 /*=== extraUtilFile.c ========================================================*/
 
 extern char *       Extra_FileGetSimilarName( char * pFileNameWrong, char * pS1, char * pS2, char * pS3, char * pS4, char * pS5 );
diff --git a/src/misc/extra/extraUtilBitMatrix.c b/src/misc/extra/extraUtilBitMatrix.c
new file mode 100644
index 00000000..f0532dba
--- /dev/null
+++ b/src/misc/extra/extraUtilBitMatrix.c
@@ -0,0 +1,359 @@
+/**CFile****************************************************************
+
+  FileName    [extraUtilBitMatrix.c]
+
+  PackageName [extra]
+
+  Synopsis    [Various reusable software utilities.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - September 1, 2003.]
+
+  Revision    [$Id: extraUtilBitMatrix.c,v 1.0 2003/09/01 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "extra.h"
+
+/*---------------------------------------------------------------------------*/
+/* Constant declarations                                                     */
+/*---------------------------------------------------------------------------*/
+
+/*---------------------------------------------------------------------------*/
+/* Stucture declarations                                                     */
+/*---------------------------------------------------------------------------*/
+
+struct Extra_BitMat_t_
+{
+    unsigned ** ppData;
+    int         nSize;
+    int         nWords;
+    int         nBitShift;
+    unsigned    uMask;
+    int         nLookups;
+    int         nInserts;
+    int         nDeletes;
+};
+
+/*---------------------------------------------------------------------------*/
+/* Type declarations                                                         */
+/*---------------------------------------------------------------------------*/
+
+/*---------------------------------------------------------------------------*/
+/* Variable declarations                                                     */
+/*---------------------------------------------------------------------------*/
+
+/*---------------------------------------------------------------------------*/
+/* Macro declarations                                                        */
+/*---------------------------------------------------------------------------*/
+
+
+/**AutomaticStart*************************************************************/
+
+/*---------------------------------------------------------------------------*/
+/* Static function prototypes                                                */
+/*---------------------------------------------------------------------------*/
+
+/**AutomaticEnd***************************************************************/
+
+
+/*---------------------------------------------------------------------------*/
+/* Definition of exported functions                                          */
+/*---------------------------------------------------------------------------*/
+
+/**Function*************************************************************
+
+  Synopsis    [Starts the bit matrix.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Extra_BitMat_t * Extra_BitMatrixStart( int nSize )
+{
+    Extra_BitMat_t * p;
+    int i;
+    p = ALLOC( Extra_BitMat_t, 1 );
+    memset( p, 0, sizeof(Extra_BitMat_t) );
+    p->nSize     = nSize;
+    p->nBitShift = (sizeof(unsigned) == 4) ?  5:  6;
+    p->uMask     = (sizeof(unsigned) == 4) ? 31: 63;
+    p->nWords    = nSize / (8 * sizeof(unsigned)) + ((nSize % (8 * sizeof(unsigned))) > 0);
+    p->ppData    = ALLOC( unsigned *, nSize );
+    p->ppData[0] = ALLOC( unsigned, nSize * p->nWords );
+    memset( p->ppData[0], 0, sizeof(unsigned) * nSize * p->nWords );
+    for ( i = 1; i < nSize; i++ )
+        p->ppData[i] = p->ppData[i-1] + p->nWords;
+    return p;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Stops the bit matrix.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Extra_BitMatrixClean( Extra_BitMat_t * p )
+{
+    memset( p->ppData[0], 0, sizeof(unsigned) * p->nSize * p->nWords );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Stops the bit matrix.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Extra_BitMatrixStop( Extra_BitMat_t * p )
+{
+    FREE( p->ppData[0] );
+    FREE( p->ppData );
+    FREE( p );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Prints the bit-matrix.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Extra_BitMatrixPrint( Extra_BitMat_t * pMat )
+{
+    int i, k, nVars;
+    printf( "\n" );
+    nVars = Extra_BitMatrixReadSize( pMat );
+    for ( i = 0; i < nVars; i++ )
+    {
+        for ( k = 0; k <= i; k++ )
+            printf( " " );
+        for ( k = i+1; k < nVars; k++ )
+            if ( Extra_BitMatrixLookup1( pMat, i, k ) )
+                printf( "1" );
+            else
+                printf( "." );
+        printf( "\n" );
+    }
+}
+
+
+/**Function*************************************************************
+
+  Synopsis    [Reads the matrix size.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Extra_BitMatrixReadSize( Extra_BitMat_t * p )
+{
+    return p->nSize;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Inserts the element into the upper part.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Extra_BitMatrixInsert1( Extra_BitMat_t * p, int i, int k )
+{
+    p->nInserts++;
+    if ( i < k )
+        p->ppData[i][k>>p->nBitShift] |= (1<<(k & p->uMask));
+    else
+        p->ppData[k][i>>p->nBitShift] |= (1<<(i & p->uMask));
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Inserts the element into the upper part.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Extra_BitMatrixLookup1( Extra_BitMat_t * p, int i, int k )
+{
+    p->nLookups++;
+    if ( i < k )
+        return ((p->ppData[i][k>>p->nBitShift] & (1<<(k & p->uMask))) > 0);
+    else
+        return ((p->ppData[k][i>>p->nBitShift] & (1<<(i & p->uMask))) > 0);
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Inserts the element into the upper part.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Extra_BitMatrixDelete1( Extra_BitMat_t * p, int i, int k )
+{
+    p->nDeletes++;
+    if ( i < k )
+        p->ppData[i][k>>p->nBitShift] &= ~(1<<(k & p->uMask));
+    else
+        p->ppData[k][i>>p->nBitShift] &= ~(1<<(i & p->uMask));
+}
+
+
+
+/**Function*************************************************************
+
+  Synopsis    [Inserts the element into the upper part.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Extra_BitMatrixInsert2( Extra_BitMat_t * p, int i, int k )
+{
+    p->nInserts++;
+    if ( i > k )
+        p->ppData[i][k>>p->nBitShift] |= (1<<(k & p->uMask));
+    else
+        p->ppData[k][i>>p->nBitShift] |= (1<<(i & p->uMask));
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Inserts the element into the upper part.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Extra_BitMatrixLookup2( Extra_BitMat_t * p, int i, int k )
+{
+    p->nLookups++;
+    if ( i > k )
+        return ((p->ppData[i][k>>p->nBitShift] & (1<<(k & p->uMask))) > 0);
+    else
+        return ((p->ppData[k][i>>p->nBitShift] & (1<<(i & p->uMask))) > 0);
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Inserts the element into the upper part.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Extra_BitMatrixDelete2( Extra_BitMat_t * p, int i, int k )
+{
+    p->nDeletes++;
+    if ( i > k )
+        p->ppData[i][k>>p->nBitShift] &= ~(1<<(k & p->uMask));
+    else
+        p->ppData[k][i>>p->nBitShift] &= ~(1<<(i & p->uMask));
+}
+
+
+/**Function*************************************************************
+
+  Synopsis    [Inserts the element into the upper part.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Extra_BitMatrixOr( Extra_BitMat_t * p, int i, unsigned * pInfo )
+{
+    int w;
+    for ( w = 0; w < p->nWords; w++ )
+        p->ppData[i][w] |= pInfo[w];
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Inserts the element into the upper part.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Extra_BitMatrixOrTwo( Extra_BitMat_t * p, int i, int j )
+{
+    int w;
+    for ( w = 0; w < p->nWords; w++ )
+        p->ppData[i][w] = p->ppData[j][w] = (p->ppData[i][w] | p->ppData[j][w]);
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Counts the number of 1's in the upper rectangle.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+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 );
+    return nTotal;
+}
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+
diff --git a/src/misc/extra/module.make b/src/misc/extra/module.make
index 0c7d36a2..bfc9d0ad 100644
--- a/src/misc/extra/module.make
+++ b/src/misc/extra/module.make
@@ -1,4 +1,5 @@
 SRC +=    src/misc/extra/extraUtilBdd.c \
+    src/misc/extra/extraUtilBitMatrix.c \
     src/misc/extra/extraUtilFile.c \
     src/misc/extra/extraUtilMemory.c \
     src/misc/extra/extraUtilMisc.c \
diff --git a/src/misc/vec/vecInt.h b/src/misc/vec/vecInt.h
index 975b61cf..76fce02e 100644
--- a/src/misc/vec/vecInt.h
+++ b/src/misc/vec/vecInt.h
@@ -430,6 +430,29 @@ static inline int Vec_IntPop( Vec_Int_t * p )
 
 /**Function*************************************************************
 
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline void Vec_IntRemove( Vec_Int_t * p, int Entry )
+{
+    int i;
+    for ( i = 0; i < p->nSize; i++ )
+        if ( p->pArray[i] == Entry )
+            break;
+    assert( i < p->nSize );
+    for ( i++; i < p->nSize; i++ )
+        p->pArray[i-1] = p->pArray[i];
+    p->nSize--;
+}
+
+/**Function*************************************************************
+
   Synopsis    [Comparison procedure for two integers.]
 
   Description []
diff --git a/src/misc/vec/vecPtr.h b/src/misc/vec/vecPtr.h
index eb551d1c..3914cf99 100644
--- a/src/misc/vec/vecPtr.h
+++ b/src/misc/vec/vecPtr.h
@@ -51,6 +51,10 @@ struct Vec_Ptr_t_
 #define Vec_PtrForEachEntry( vVec, pEntry, i )                                               \
     for ( i = 0; (i < Vec_PtrSize(vVec)) && (((pEntry) = Vec_PtrEntry(vVec, i)), 1); i++ )
 
+#define Vec_PtrForEachEntryByLevel( vVec, pEntry, i, k )                                     \
+    for ( i = 0; i < Vec_PtrSize(vVec); i++ )                                                \
+        Vec_PtrForEachEntry( ((Vec_Ptr_t *)Vec_PtrEntry(vVec, i)), pEntry, k ) 
+
 ////////////////////////////////////////////////////////////////////////
 ///                     FUNCTION DEFITIONS                           ///
 ////////////////////////////////////////////////////////////////////////
@@ -169,7 +173,7 @@ static inline Vec_Ptr_t * Vec_PtrDupArray( Vec_Ptr_t * pVec )
 
 /**Function*************************************************************
 
-  Synopsis    []
+  Synopsis    [Frees the vector.]
 
   Description []
                
@@ -463,6 +467,46 @@ static inline void Vec_PtrReorder( Vec_Ptr_t * p, int nItems )
 
 /**Function*************************************************************
 
+  Synopsis    [Frees the vector of vectors.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline void Vec_PtrFreeFree( Vec_Ptr_t * p )
+{
+    Vec_Ptr_t * vVec;
+    int i;
+    Vec_PtrForEachEntry( p, vVec, i )
+        Vec_PtrFree( vVec );
+    Vec_PtrFree( p );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Frees the vector of vectors.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline int Vec_PtrSizeSize( Vec_Ptr_t * p )
+{
+    Vec_Ptr_t * vVec;
+    int i, Counter = 0;
+    Vec_PtrForEachEntry( p, vVec, i )
+        Counter += vVec->nSize;
+    return Counter;
+}
+
+/**Function*************************************************************
+
   Synopsis    [Sorting the entries by their integer value.]
 
   Description []
diff --git a/src/misc/vec/vecStr.h b/src/misc/vec/vecStr.h
index 33be5f1d..2a9dc7a0 100644
--- a/src/misc/vec/vecStr.h
+++ b/src/misc/vec/vecStr.h
@@ -301,8 +301,8 @@ static inline void Vec_StrGrow( Vec_Str_t * p, int nCapMin )
 {
     if ( p->nCap >= nCapMin )
         return;
-    p->pArray = REALLOC( char, p->pArray, nCapMin ); 
-    p->nCap   = nCapMin;
+    p->pArray = REALLOC( char, p->pArray, 2 * nCapMin ); 
+    p->nCap   = 2 * nCapMin;
 }
 
 /**Function*************************************************************
@@ -383,6 +383,26 @@ static inline void Vec_StrPush( Vec_Str_t * p, char Entry )
 
 /**Function*************************************************************
 
+  Synopsis    [Appends the string to the char vector.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline void Vec_StrAppend( Vec_Str_t * p, char * pString )
+{
+    int i, nLength = strlen(pString);
+    Vec_StrGrow( p, p->nSize + nLength );
+    for ( i = 0; i < nLength; i++ )
+        p->pArray[p->nSize + i] = pString[i];
+    p->nSize += nLength;
+}
+
+/**Function*************************************************************
+
   Synopsis    [Returns the last entry and removes it from the list.]
 
   Description []