merge pyabc changes into mainline

4 files changed, 152 insertions, 8 deletions

diff --git a/src/misc/extra/extra.h b/src/misc/extra/extra.h
index 96ff6072..33303fac 100644
--- a/src/misc/extra/extra.h
+++ b/src/misc/extra/extra.h
@@ -196,6 +196,8 @@ extern DdNode *     Extra_bddCreateExor( DdManager * dd, int nVars );
 extern DdNode *     Extra_zddPrimes( DdManager * dd, DdNode * F );
 extern void         Extra_bddPermuteArray( DdManager * dd, DdNode ** bNodesIn, DdNode ** bNodesOut, int nNodes, int *permut );
 extern DdNode *     Extra_bddComputeCube( DdManager * dd, DdNode ** bXVars, int nVars );
+extern DdNode *     Extra_bddChangePolarity( DdManager * dd, DdNode * bFunc, DdNode * bVars );
+extern DdNode *     extraBddChangePolarity( DdManager * dd, DdNode * bFunc, DdNode * bVars );
 
 #ifndef ABC_PRB
 #define ABC_PRB(dd,f)       printf("%s = ", #f); Extra_bddPrint(dd,f); printf("\n")
diff --git a/src/misc/extra/extraBddMisc.c b/src/misc/extra/extraBddMisc.c
index cdded9b8..69309a4d 100644
--- a/src/misc/extra/extraBddMisc.c
+++ b/src/misc/extra/extraBddMisc.c
@@ -1013,6 +1013,32 @@ DdNode * Extra_bddComputeCube( DdManager * dd, DdNode ** bXVars, int nVars )
     return bRes;
 }
 
+/**Function********************************************************************
+
+  Synopsis    [Changes the polarity of vars listed in the cube.]
+
+  Description []
+
+  SideEffects []
+
+  SeeAlso     []
+
+******************************************************************************/
+DdNode * Extra_bddChangePolarity( 
+  DdManager * dd,   /* the DD manager */
+  DdNode * bFunc,
+  DdNode * bVars) 
+{
+    DdNode  *res;
+    do {
+        dd->reordered = 0;
+        res = extraBddChangePolarity( dd, bFunc, bVars );
+    } while (dd->reordered == 1);
+    return(res);
+
+} /* end of Extra_bddChangePolarity */
+
+
 /*---------------------------------------------------------------------------*/
 /* Definition of internal functions                                          */
 /*---------------------------------------------------------------------------*/
@@ -1659,6 +1685,121 @@ cuddBddPermuteRecur( DdManager * manager /* DD manager */ ,
 }                                /* end of cuddBddPermuteRecur */
 
 
+/**Function********************************************************************
+
+  Synopsis    [Performs the reordering-sensitive step of Extra_bddChangePolarity().]
+
+  Description []
+
+  SideEffects []
+
+  SeeAlso     []
+
+******************************************************************************/
+DdNode * extraBddChangePolarity( 
+  DdManager * dd,    /* the DD manager */
+  DdNode * bFunc, 
+  DdNode * bVars) 
+{
+    DdNode * bRes;
+
+    if ( bVars == b1 )
+        return bFunc;
+    if ( Cudd_IsConstant(bFunc) )
+        return bFunc;
+
+    if ( bRes = cuddCacheLookup2(dd, extraBddChangePolarity, bFunc, bVars) )
+        return bRes;
+    else
+    {
+        DdNode * bFR = Cudd_Regular(bFunc); 
+        int LevelF   = dd->perm[bFR->index];
+        int LevelV   = dd->perm[bVars->index];
+
+        if ( LevelV < LevelF )
+            bRes = extraBddChangePolarity( dd, bFunc, cuddT(bVars) );
+        else // if ( LevelF <= LevelV )
+        {
+            DdNode * bRes0, * bRes1;             
+            DdNode * bF0, * bF1;             
+            DdNode * bVarsNext;
+
+            // cofactor the functions
+            if ( bFR != bFunc ) // bFunc is complemented 
+            {
+                bF0 = Cudd_Not( cuddE(bFR) );
+                bF1 = Cudd_Not( cuddT(bFR) );
+            }
+            else
+            {
+                bF0 = cuddE(bFR);
+                bF1 = cuddT(bFR);
+            }
+
+            if ( LevelF == LevelV )
+                bVarsNext = cuddT(bVars);
+            else
+                bVarsNext = bVars;
+
+            bRes0 = extraBddChangePolarity( dd, bF0, bVarsNext );
+            if ( bRes0 == NULL ) 
+                return NULL;
+            cuddRef( bRes0 );
+
+            bRes1 = extraBddChangePolarity( dd, bF1, bVarsNext );
+            if ( bRes1 == NULL ) 
+            {
+                Cudd_RecursiveDeref( dd, bRes0 );
+                return NULL;
+            }
+            cuddRef( bRes1 );
+
+            if ( LevelF == LevelV )
+            { // swap the cofactors
+                DdNode * bTemp;
+                bTemp = bRes0;
+                bRes0 = bRes1;
+                bRes1 = bTemp;
+            }
+
+            /* only aRes0 and aRes1 are referenced at this point */
+
+            /* consider the case when Res0 and Res1 are the same node */
+            if ( bRes0 == bRes1 )
+                bRes = bRes1;
+            /* consider the case when Res1 is complemented */
+            else if ( Cudd_IsComplement(bRes1) ) 
+            {
+                bRes = cuddUniqueInter(dd, bFR->index, Cudd_Not(bRes1), Cudd_Not(bRes0));
+                if ( bRes == NULL ) 
+                {
+                    Cudd_RecursiveDeref(dd,bRes0);
+                    Cudd_RecursiveDeref(dd,bRes1);
+                    return NULL;
+                }
+                bRes = Cudd_Not(bRes);
+            } 
+            else 
+            {
+                bRes = cuddUniqueInter( dd, bFR->index, bRes1, bRes0 );
+                if ( bRes == NULL ) 
+                {
+                    Cudd_RecursiveDeref(dd,bRes0);
+                    Cudd_RecursiveDeref(dd,bRes1);
+                    return NULL;
+                }
+            }
+            cuddDeref( bRes0 );
+            cuddDeref( bRes1 );
+        }
+            
+        /* insert the result into cache */
+        cuddCacheInsert2(dd, extraBddChangePolarity, bFunc, bVars, bRes);
+        return bRes;
+    }
+} /* end of extraBddChangePolarity */
+
+
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////
diff --git a/src/misc/hash/hashFlt.h b/src/misc/hash/hashFlt.h
index b4a8fb49..74e8503d 100644
--- a/src/misc/hash/hashFlt.h
+++ b/src/misc/hash/hashFlt.h
@@ -311,14 +311,15 @@ static inline void Hash_FltRemove( Hash_Flt_t *p, int key )
 ***********************************************************************/
 static inline void Hash_FltFree( Hash_Flt_t *p ) {
   int bin;
-  Hash_Flt_Entry_t *pEntry;
+  Hash_Flt_Entry_t *pEntry, *pTemp;
 
   // free bins
   for(bin = 0; bin < p->nBins; bin++) {
     pEntry = p->pArray[bin];
     while(pEntry) {
+      pTemp = pEntry;
       pEntry = pEntry->pNext;
-      ABC_FREE( pEntry );
+      ABC_FREE( pTemp );
     }
   }
  
diff --git a/src/misc/hash/hashPtr.h b/src/misc/hash/hashPtr.h
index 9e510866..a10fb548 100644
--- a/src/misc/hash/hashPtr.h
+++ b/src/misc/hash/hashPtr.h
@@ -115,19 +115,17 @@ static inline Hash_Ptr_t * Hash_PtrAlloc( int nBins )
 static inline int Hash_PtrExists( Hash_Ptr_t *p, int key )
 {
   int bin;
-  Hash_Ptr_Entry_t *pEntry, **pLast;
+  Hash_Ptr_Entry_t *pEntry;
 
   // find the bin where this key would live
   bin = (*(p->fHash))(key, p->nBins);
 
   // search for key
-  pLast = &(p->pArray[bin]);
   pEntry = p->pArray[bin];
   while(pEntry) {
     if (pEntry->key == key) {
       return 1;
     }
-    pLast = &(pEntry->pNext);
     pEntry = pEntry->pNext;
   }
 
@@ -310,16 +308,18 @@ static inline void* Hash_PtrRemove( Hash_Ptr_t *p, int key )
   SeeAlso     []
 
 ***********************************************************************/
-static inline void Hash_PtrFree( Hash_Ptr_t *p ) {
+static inline void Hash_PtrFree( Hash_Ptr_t *p ) 
+{
   int bin;
-  Hash_Ptr_Entry_t *pEntry;
+  Hash_Ptr_Entry_t *pEntry, *pTemp;
 
   // free bins
   for(bin = 0; bin < p->nBins; bin++) {
     pEntry = p->pArray[bin];
     while(pEntry) {
+      pTemp = pEntry;
       pEntry = pEntry->pNext;
-      ABC_FREE( pEntry );
+      ABC_FREE( pTemp );
     }
   }