Version abc60723

4 files changed, 149 insertions, 5 deletions

diff --git a/src/misc/extra/extra.h b/src/misc/extra/extra.h
index 9f3b4cc7..bdbc3d89 100644
--- a/src/misc/extra/extra.h
+++ b/src/misc/extra/extra.h
@@ -433,6 +433,14 @@ static inline int Extra_TruthIsConst1( unsigned * pIn, int nVars )
             return 0;
     return 1;
 }
+static inline int Extra_TruthIsImply( unsigned * pIn1, unsigned * pIn2, int nVars )
+{
+    int w;
+    for ( w = Extra_TruthWordNum(nVars)-1; w >= 0; w-- )
+        if ( pIn1[w] & ~pIn2[w] )
+            return 0;
+    return 1;
+}
 static inline void Extra_TruthCopy( unsigned * pOut, unsigned * pIn, int nVars )
 {
     int w;
@@ -491,7 +499,9 @@ extern int      Extra_TruthSupportSize( unsigned * pTruth, int nVars );
 extern int      Extra_TruthSupport( unsigned * pTruth, int nVars );
 extern void     Extra_TruthCofactor0( unsigned * pTruth, int nVars, int iVar );
 extern void     Extra_TruthCofactor1( unsigned * pTruth, int nVars, int iVar );
-extern void     Extra_TruthCombine( unsigned * pOut, unsigned * pCof0, unsigned * pCof1, int nVars, int iVar );
+extern void     Extra_TruthExist( unsigned * pTruth, int nVars, int iVar );
+extern void     Extra_TruthForall( unsigned * pTruth, int nVars, int iVar );
+extern void     Extra_TruthMux( unsigned * pOut, unsigned * pCof0, unsigned * pCof1, int nVars, int iVar );
 extern void     Extra_TruthChangePhase( unsigned * pTruth, int nVars, int iVar );
 extern int      Extra_TruthMinCofSuppOverlap( unsigned * pTruth, int nVars, int * pVarMin );
 extern int      Extra_TruthCountOnes( unsigned * pTruth, int nVars );
diff --git a/src/misc/extra/extraUtilTruth.c b/src/misc/extra/extraUtilTruth.c
index a80c0d3d..83153863 100644
--- a/src/misc/extra/extraUtilTruth.c
+++ b/src/misc/extra/extraUtilTruth.c
@@ -506,6 +506,116 @@ void Extra_TruthCofactor0( unsigned * pTruth, int nVars, int iVar )
     }
 }
 
+
+/**Function*************************************************************
+
+  Synopsis    [Existentially quantifies the variable.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Extra_TruthExist( unsigned * pTruth, int nVars, int iVar )
+{
+    int nWords = Extra_TruthWordNum( nVars );
+    int i, k, Step;
+
+    assert( iVar < nVars );
+    switch ( iVar )
+    {
+    case 0:
+        for ( i = 0; i < nWords; i++ )
+            pTruth[i] |=  ((pTruth[i] & 0xAAAAAAAA) >> 1) | ((pTruth[i] & 0x55555555) << 1);
+        return;
+    case 1:
+        for ( i = 0; i < nWords; i++ )
+            pTruth[i] |=  ((pTruth[i] & 0xCCCCCCCC) >> 2) | ((pTruth[i] & 0x33333333) << 2);
+        return;
+    case 2:
+        for ( i = 0; i < nWords; i++ )
+            pTruth[i] |=  ((pTruth[i] & 0xF0F0F0F0) >> 4) | ((pTruth[i] & 0x0F0F0F0F) << 4);
+        return;
+    case 3:
+        for ( i = 0; i < nWords; i++ )
+            pTruth[i] |=  ((pTruth[i] & 0xFF00FF00) >> 8) | ((pTruth[i] & 0x00FF00FF) << 8);
+        return;
+    case 4:
+        for ( i = 0; i < nWords; i++ )
+            pTruth[i] |=  ((pTruth[i] & 0xFFFF0000) >> 16) | ((pTruth[i] & 0x0000FFFF) << 16);
+        return;
+    default:
+        Step = (1 << (iVar - 5));
+        for ( k = 0; k < nWords; k += 2*Step )
+        {
+            for ( i = 0; i < Step; i++ )
+            {
+                pTruth[i]     |= pTruth[Step+i];
+                pTruth[Step+i] = pTruth[i];
+            }
+            pTruth += 2*Step;
+        }
+        return;
+    }
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Existentially quantifies the variable.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Extra_TruthForall( unsigned * pTruth, int nVars, int iVar )
+{
+    int nWords = Extra_TruthWordNum( nVars );
+    int i, k, Step;
+
+    assert( iVar < nVars );
+    switch ( iVar )
+    {
+    case 0:
+        for ( i = 0; i < nWords; i++ )
+            pTruth[i] &=  ((pTruth[i] & 0xAAAAAAAA) >> 1) | ((pTruth[i] & 0x55555555) << 1);
+        return;
+    case 1:
+        for ( i = 0; i < nWords; i++ )
+            pTruth[i] &=  ((pTruth[i] & 0xCCCCCCCC) >> 2) | ((pTruth[i] & 0x33333333) << 2);
+        return;
+    case 2:
+        for ( i = 0; i < nWords; i++ )
+            pTruth[i] &=  ((pTruth[i] & 0xF0F0F0F0) >> 4) | ((pTruth[i] & 0x0F0F0F0F) << 4);
+        return;
+    case 3:
+        for ( i = 0; i < nWords; i++ )
+            pTruth[i] &=  ((pTruth[i] & 0xFF00FF00) >> 8) | ((pTruth[i] & 0x00FF00FF) << 8);
+        return;
+    case 4:
+        for ( i = 0; i < nWords; i++ )
+            pTruth[i] &=  ((pTruth[i] & 0xFFFF0000) >> 16) | ((pTruth[i] & 0x0000FFFF) << 16);
+        return;
+    default:
+        Step = (1 << (iVar - 5));
+        for ( k = 0; k < nWords; k += 2*Step )
+        {
+            for ( i = 0; i < Step; i++ )
+            {
+                pTruth[i]     &= pTruth[Step+i];
+                pTruth[Step+i] = pTruth[i];
+            }
+            pTruth += 2*Step;
+        }
+        return;
+    }
+}
+
+
 /**Function*************************************************************
 
   Synopsis    [Computes negative cofactor of the function.]
@@ -517,7 +627,7 @@ void Extra_TruthCofactor0( unsigned * pTruth, int nVars, int iVar )
   SeeAlso     []
 
 ***********************************************************************/
-void Extra_TruthCombine( unsigned * pOut, unsigned * pCof0, unsigned * pCof1, int nVars, int iVar )
+void Extra_TruthMux( unsigned * pOut, unsigned * pCof0, unsigned * pCof1, int nVars, int iVar )
 {
     int nWords = Extra_TruthWordNum( nVars );
     int i, k, Step;
diff --git a/src/misc/nm/nmTable.c b/src/misc/nm/nmTable.c
index 86c520d8..65f16e04 100644
--- a/src/misc/nm/nmTable.c
+++ b/src/misc/nm/nmTable.c
@@ -44,7 +44,7 @@ static unsigned Nm_HashString( char * pName, int TableSize )
     };
     unsigned i, Key = 0;
     for ( i = 0; pName[i] != '\0'; i++ )
-        Key ^= s_Primes[i%10]*pName[i];
+        Key ^= s_Primes[i%10]*pName[i]*pName[i];
     return Key % TableSize;
 }
 
@@ -142,7 +142,7 @@ Nm_Entry_t * Nm_ManTableLookupId( Nm_Man_t * p, int ObjId )
 Nm_Entry_t * Nm_ManTableLookupName( Nm_Man_t * p, char * pName, Nm_Entry_t ** ppSecond )
 {
     Nm_Entry_t * pFirst, * pSecond;
-    int i;
+    int i, Counter = 0;
     pFirst = pSecond = NULL;
     for ( i = Nm_HashString(pName, p->nBins); p->pBinsN2I[i]; i = (i+1) % p->nBins )
         if ( strcmp(p->pBinsN2I[i]->Name, pName) == 0 )
@@ -154,6 +154,10 @@ Nm_Entry_t * Nm_ManTableLookupName( Nm_Man_t * p, char * pName, Nm_Entry_t ** pp
             else
                 assert( 0 ); // name appears more than 2 times
         }
+        else
+            Counter++;
+    if ( Counter > 100 )
+    printf( "%d ", Counter );
     // save the names
     if ( ppSecond )
         *ppSecond = pSecond;
diff --git a/src/misc/vec/vecPtr.h b/src/misc/vec/vecPtr.h
index 96975ff0..f2413703 100644
--- a/src/misc/vec/vecPtr.h
+++ b/src/misc/vec/vecPtr.h
@@ -293,6 +293,23 @@ static inline void * Vec_PtrEntry( Vec_Ptr_t * p, int i )
   SeeAlso     []
 
 ***********************************************************************/
+static inline void ** Vec_PtrEntryP( Vec_Ptr_t * p, int i )
+{
+    assert( i >= 0 && i < p->nSize );
+    return p->pArray + i;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
 static inline void Vec_PtrWriteEntry( Vec_Ptr_t * p, int i, void * Entry )
 {
     assert( i >= 0 && i < p->nSize );
@@ -371,7 +388,10 @@ static inline void Vec_PtrFillExtra( Vec_Ptr_t * p, int nSize, void * Entry )
     int i;
     if ( p->nSize >= nSize )
         return;
-    Vec_PtrGrow( p, nSize );
+    if ( p->nSize < 2 * nSize )
+        Vec_PtrGrow( p, 2 * nSize );
+    else
+        Vec_PtrGrow( p, p->nSize );
     for ( i = p->nSize; i < nSize; i++ )
         p->pArray[i] = Entry;
     p->nSize = nSize;