Version abc80130

6 files changed, 28 insertions, 263 deletions

diff --git a/src/bdd/reo/module.make b/src/bdd/reo/module.make
index 3a636980..7eb41e0e 100644
--- a/src/bdd/reo/module.make
+++ b/src/bdd/reo/module.make
@@ -1,7 +1,6 @@
 SRC +=    src/bdd/reo/reoApi.c \
     src/bdd/reo/reoCore.c \
     src/bdd/reo/reoProfile.c \
-    src/bdd/reo/reoShuffle.c \
     src/bdd/reo/reoSift.c \
     src/bdd/reo/reoSwap.c \
     src/bdd/reo/reoTransfer.c \
diff --git a/src/bdd/reo/reo.h b/src/bdd/reo/reo.h
index 1a31242a..7e4be855 100644
--- a/src/bdd/reo/reo.h
+++ b/src/bdd/reo/reo.h
@@ -19,16 +19,10 @@
 #ifndef __REO_H__
 #define __REO_H__
 
-#ifdef __cplusplus
-extern "C" {
-#endif
-
 #include <stdio.h>
 #include <stdlib.h>
 #include "extra.h"
 
-//#pragma warning( disable : 4514 )
-
 ////////////////////////////////////////////////////////////////////////
 ///                     MACRO DEFINITIONS                            ///
 ////////////////////////////////////////////////////////////////////////
@@ -93,9 +87,9 @@ struct _reo_plane
 struct _reo_hash
 {
     int         Sign;            // signature of the current cache operation
-    reo_unit *  Arg1;            // the first argument
-    reo_unit *  Arg2;            // the second argument
-    reo_unit *  Arg3;            // the third argument
+    unsigned    Arg1;            // the first argument
+    unsigned    Arg2;            // the second argument
+    unsigned    Arg3;            // the second argument
 };
 
 struct _reo_man
@@ -172,8 +166,8 @@ struct _reo_man
 
 // used to manipulate units
 #define Unit_Regular(u)     ((reo_unit *)((unsigned long)(u) & ~01))
-#define Unit_Not(u)         ((reo_unit *)((unsigned long)(u) ^ 01))
-#define Unit_NotCond(u,c)   ((reo_unit *)((unsigned long)(u) ^ (c)))
+#define Unit_Not(u)         ((reo_unit *)((long)(u) ^ 01))
+#define Unit_NotCond(u,c)   ((reo_unit *)((long)(u) ^ (c)))
 #define Unit_IsConstant(u)  ((int)((u)->lev == REO_CONST_LEVEL))
 
 ////////////////////////////////////////////////////////////////////////
@@ -221,12 +215,8 @@ extern DdNode *   Extra_ReorderCudd( DdManager * dd, DdNode * aFunc, int pPermut
 extern int        Extra_bddReorderTest( DdManager * dd, DdNode * bF ); 
 extern int        Extra_addReorderTest( DdManager * dd, DdNode * aF ); 
 
-#ifdef __cplusplus
-}
-#endif
-
-#endif
-
 ////////////////////////////////////////////////////////////////////////
 ///                         END OF FILE                              ///
 ////////////////////////////////////////////////////////////////////////
+
+#endif
diff --git a/src/bdd/reo/reoProfile.c b/src/bdd/reo/reoProfile.c
index 84a0bc19..b38575f0 100644
--- a/src/bdd/reo/reoProfile.c
+++ b/src/bdd/reo/reoProfile.c
@@ -330,7 +330,7 @@ void reoProfileWidthPrint( reo_man * p )
              WidthMax = p->pPlanes[i].statsWidth;
         TotalWidth += p->pPlanes[i].statsWidth;
     }
-    assert( p->nWidthCur == TotalWidth );
+    assert( p->nWidthCur = TotalWidth );
     printf( "WIDTH:  " );
     printf( "Maximum = %5d.  ", WidthMax );
     printf( "Total = %7d.  ", p->nWidthCur );
diff --git a/src/bdd/reo/reoShuffle.c b/src/bdd/reo/reoShuffle.c
deleted file mode 100644
index 8dab67a4..00000000
--- a/src/bdd/reo/reoShuffle.c
+++ /dev/null
@@ -1,224 +0,0 @@
-/**CFile****************************************************************
-
-  FileName    [reoShuffle.c]
-
-  PackageName [REO: A specialized DD reordering engine.]
-
-  Synopsis    [Implementation of the two-variable swap.]
-
-  Author      [Alan Mishchenko]
-  
-  Affiliation [UC Berkeley]
-
-  Date        [Ver. 1.0. Started - October 15, 2002.]
-
-  Revision    [$Id: reoShuffle.c,v 1.0 2002/15/10 03:00:00 alanmi Exp $]
-
-***********************************************************************/
-
-#include "reo.h"
-
-////////////////////////////////////////////////////////////////////////
-///                        DECLARATIONS                              ///
-////////////////////////////////////////////////////////////////////////
-
-////////////////////////////////////////////////////////////////////////
-///                    FUNCTION DEFINITIONS                          ///
-////////////////////////////////////////////////////////////////////////
-
-/**Function*************************************************************
-
-  Synopsis    [This procedure is similar to Cudd_ShuffleHeap() and Cudd_bddPermute().]
-
-  Description [The first argument is the REO manager. The 2nd/3d
-  arguments are the function and its CUDD manager. The last argument
-  is the permutation to be implemented. The i-th entry of the permutation 
-  array contains the index of the variable that should be brought to the 
-  i-th level.  The size of the array should be equal or greater to 
-  the number of variables currently in use (that is, the size of CUDD
-  manager and the size of REO manager).]
-
-  SideEffects [Note that the resulting BDD is not referenced.]
-
-  SeeAlso     []
-
-***********************************************************************/
-DdNode * reoShuffle( reo_man * p, DdManager * dd, DdNode * bFunc, int * pPerm, int * pPermInv )
-{
-    DdNode * bFuncRes = NULL;
-    int i, k, v;
-
-    if ( Cudd_IsConstant(bFunc) )
-        return bFunc;
-
-    // set the initial parameters
-    p->dd    = dd;
-    p->nSupp = Cudd_SupportSize( dd, bFunc );
-    p->nTops = 1;
-//    p->nNodesBeg = Cudd_DagSize( bFunc );
-
-    // set the starting permutation
-    for ( i = 0; i < p->nSupp; i++ )
-    {
-        p->pOrderInt[i] = i;
-        p->pMapToPlanes[ dd->invperm[i] ] = i;
-        p->pMapToDdVarsFinal[i] = dd->invperm[i];
-    }
-
-    // set the initial parameters
-    p->nUnitsUsed = 0;
-    p->nNodesCur  = 0;
-    p->fThisIsAdd = 0;
-    p->Signature++;
-
-    // transfer the function from the CUDD package into REO's internal data structure
-    p->pTops[0] = reoTransferNodesToUnits_rec( p, bFunc );
-//    assert( p->nNodesBeg == p->nNodesCur );
-
-    // reorder one variable at a time
-    for ( i = 0; i < p->nSupp; i++ )
-    {
-        if ( p->pOrderInt[i] == pPerm[i] )
-            continue;
-        // find where is variable number pPerm[i]
-        for ( k = i + 1; k < p->nSupp; k++ )
-            if ( pPerm[i] == p->pOrderInt[k] )
-                break;
-        if ( k == p->nSupp )
-        {
-            printf( "reoShuffle() Error: Cannot find a variable.\n" );
-            goto finish;
-        }
-        // move the variable up
-        for ( v = k - 1; v >= i; v-- )
-        {
-            reoReorderSwapAdjacentVars( p, v, 1 );
-            // check if the number of nodes is not too large
-            if ( p->nNodesCur > 10000 )
-            {
-                printf( "reoShuffle() Error: BDD size is too large.\n" );
-                goto finish;
-            }
-        }
-        assert( p->pOrderInt[i] == pPerm[i] );
-    }
-
-    // set the initial parameters
-    p->nRefNodes  = 0;
-    p->nNodesCur  = 0;
-    p->Signature++;
-    // transfer the BDDs from REO's internal data structure to CUDD
-    bFuncRes = reoTransferUnitsToNodes_rec( p, p->pTops[0] ); Cudd_Ref( bFuncRes );
-    // undo the DDs referenced for storing in the cache
-    for ( i = 0; i < p->nRefNodes; i++ )
-        Cudd_RecursiveDeref( dd, p->pRefNodes[i] );
-
-    // verify zero refs of the terminal nodes
-//    assert( reoRecursiveDeref( p->pTops[0] ) );
-//    assert( reoCheckZeroRefs( &(p->pPlanes[p->nSupp]) ) );
-
-    // perform verification
-    if ( p->fVerify )
-    {
-        DdNode * bFuncPerm;
-        bFuncPerm = Cudd_bddPermute( dd, bFunc, pPermInv );  Cudd_Ref( bFuncPerm );
-        if ( bFuncPerm != bFuncRes )
-        {
-            printf( "REO: Internal verification has failed!\n" );
-            fflush( stdout );
-        }
-        Cudd_RecursiveDeref( dd, bFuncPerm );
-    }
-
-    // recycle the data structure
-    for ( i = 0; i <= p->nSupp; i++ )
-        reoUnitsRecycleUnitList( p, p->pPlanes + i );
-
-finish :
-    if ( bFuncRes )
-        Cudd_Deref( bFuncRes );
-    return bFuncRes;
-}
-
-
-
-/**Function*************************************************************
-
-  Synopsis    [Reorders the DD using REO and CUDD.]
-
-  Description [This function can be used to test the performance of the reordering package.]
-
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Extra_ShuffleTest( reo_man * pReo, DdManager * dd, DdNode * Func )
-{
-//    extern int runtime1, runtime2;
-
-    DdNode * Temp, * bRemap;
-    int nSuppSize, OffSet, Num, i, clk;
-    int pOrder[1000], pOrderInv[1000];
-    assert( dd->size < 1000 );
-
-    srand( 0x12341234 );
-    nSuppSize = Cudd_SupportSize( dd, Func );
-    if ( nSuppSize < 2 )
-        return;
-
-    for ( i = 0; i < nSuppSize; i++ )
-        pOrder[i] = i;
-    for ( i = 0; i < 120; i++ )
-    {
-        OffSet = rand() % (nSuppSize - 1);
-        Num = pOrder[OffSet];
-        pOrder[OffSet] = pOrder[OffSet+1];
-        pOrder[OffSet+1] = Num;
-    }
-    for ( i = 0; i < nSuppSize; i++ )
-        pOrderInv[pOrder[i]] = i;
-
-/*
-    printf( "Permutation: " );
-    for ( i = 0; i < nSuppSize; i++ )
-        printf( "%d ", pOrder[i] );
-    printf( "\n" );
-    printf( "Inverse permutation: " );
-    for ( i = 0; i < nSuppSize; i++ )
-        printf( "%d ", pOrderInv[i] );
-    printf( "\n" );
-*/
-
-    // create permutation
-//    Extra_ReorderSetVerification( pReo, 1 );
-    bRemap = Extra_bddRemapUp( dd, Func );  Cudd_Ref( bRemap );
-
-clk = clock();
-    Temp  = reoShuffle( pReo, dd, bRemap, pOrder, pOrderInv );  Cudd_Ref( Temp );
-//runtime1 += clock() - clk;
-
-//printf( "Initial = %d. Final = %d.\n", Cudd_DagSize(bRemap), Cudd_DagSize(Temp)  );
-
-    {
-        DdNode * bFuncPerm;
-clk = clock();
-        bFuncPerm = Cudd_bddPermute( dd, bRemap, pOrderInv );  Cudd_Ref( bFuncPerm );
-//runtime2 += clock() - clk;
-        if ( bFuncPerm != Temp )
-        {
-            printf( "REO: Internal verification has failed!\n" );
-            fflush( stdout );
-        }
-        Cudd_RecursiveDeref( dd, bFuncPerm );
-    }
-
-    Cudd_RecursiveDeref( dd, Temp );
-    Cudd_RecursiveDeref( dd, bRemap );
-}
-
-
-////////////////////////////////////////////////////////////////////////
-///                         END OF FILE                              ///
-////////////////////////////////////////////////////////////////////////
-
diff --git a/src/bdd/reo/reoSwap.c b/src/bdd/reo/reoSwap.c
index 4afa650c..cb730d8e 100644
--- a/src/bdd/reo/reoSwap.c
+++ b/src/bdd/reo/reoSwap.c
@@ -271,9 +271,9 @@ double reoReorderSwapAdjacentVars( reo_man * p, int lev0, int fMovingUp )
                    HKey = (HKey+1) % p->nTableSize );
             assert( p->HTable[HKey].Sign != p->Signature );
             p->HTable[HKey].Sign = p->Signature;
-            p->HTable[HKey].Arg1 = pUnitE;
-            p->HTable[HKey].Arg2 = pUnitT;
-            p->HTable[HKey].Arg3 = pUnit;
+            p->HTable[HKey].Arg1 = (unsigned)pUnitE;
+            p->HTable[HKey].Arg2 = (unsigned)pUnitT;
+            p->HTable[HKey].Arg3 = (unsigned)pUnit;
 
             nNodesUpMovedDown++;
 
@@ -512,10 +512,10 @@ double reoReorderSwapAdjacentVars( reo_man * p, int lev0, int fMovingUp )
             for (  HKey = hashKey3(p->Signature, pNew1E, pNew1T, p->nTableSize);
                    p->HTable[HKey].Sign == p->Signature;
                    HKey = (HKey+1) % p->nTableSize )
-            if ( p->HTable[HKey].Arg1 == pNew1E && p->HTable[HKey].Arg2 == pNew1T )
+            if ( p->HTable[HKey].Arg1 == (unsigned)pNew1E && p->HTable[HKey].Arg2 == (unsigned)pNew1T )
             { // the entry is present 
                 // assign this entry
-                pNewPlane20 = p->HTable[HKey].Arg3;
+                pNewPlane20 = (reo_unit *)p->HTable[HKey].Arg3;
                 assert( pNewPlane20->lev == lev1 );
                 fFound = 1;
                 p->HashSuccess++;
@@ -549,9 +549,9 @@ double reoReorderSwapAdjacentVars( reo_man * p, int lev0, int fMovingUp )
                 // add this entry to cache
                 assert( p->HTable[HKey].Sign != p->Signature );
                 p->HTable[HKey].Sign = p->Signature;
-                p->HTable[HKey].Arg1 = pNew1E;
-                p->HTable[HKey].Arg2 = pNew1T;
-                p->HTable[HKey].Arg3 = pNewPlane20;
+                p->HTable[HKey].Arg1 = (unsigned)pNew1E;
+                p->HTable[HKey].Arg2 = (unsigned)pNew1T;
+                p->HTable[HKey].Arg3 = (unsigned)pNewPlane20;
 
                 nNodesUnrefAdded++;
                         
@@ -637,10 +637,10 @@ double reoReorderSwapAdjacentVars( reo_man * p, int lev0, int fMovingUp )
             for (  HKey = hashKey3(p->Signature, pNew2E, pNew2T, p->nTableSize);
                    p->HTable[HKey].Sign == p->Signature;
                    HKey = (HKey+1) % p->nTableSize )
-            if ( p->HTable[HKey].Arg1 == pNew2E && p->HTable[HKey].Arg2 == pNew2T )
+            if ( p->HTable[HKey].Arg1 == (unsigned)pNew2E && p->HTable[HKey].Arg2 == (unsigned)pNew2T )
             { // the entry is present 
                 // assign this entry
-                pNewPlane21 = p->HTable[HKey].Arg3;
+                pNewPlane21 = (reo_unit *)p->HTable[HKey].Arg3;
                 assert( pNewPlane21->lev == lev1 );
                 fFound = 1;
                 p->HashSuccess++;
@@ -675,9 +675,9 @@ double reoReorderSwapAdjacentVars( reo_man * p, int lev0, int fMovingUp )
                 // add this entry to cache
                 assert( p->HTable[HKey].Sign != p->Signature );
                 p->HTable[HKey].Sign = p->Signature;
-                p->HTable[HKey].Arg1 = pNew2E;
-                p->HTable[HKey].Arg2 = pNew2T;
-                p->HTable[HKey].Arg3 = pNewPlane21;
+                p->HTable[HKey].Arg1 = (unsigned)pNew2E;
+                p->HTable[HKey].Arg2 = (unsigned)pNew2T;
+                p->HTable[HKey].Arg3 = (unsigned)pNewPlane21;
 
                 nNodesUnrefAdded++;
 
diff --git a/src/bdd/reo/reoTransfer.c b/src/bdd/reo/reoTransfer.c
index 65d31d01..752cd3d7 100644
--- a/src/bdd/reo/reoTransfer.c
+++ b/src/bdd/reo/reoTransfer.c
@@ -51,9 +51,9 @@ reo_unit * reoTransferNodesToUnits_rec( reo_man * p, DdNode * F )
     {
         // search cache - use linear probing
         for ( HKey = hashKey2(p->Signature,F,p->nTableSize); p->HTable[HKey].Sign == p->Signature; HKey = (HKey+1) % p->nTableSize )
-            if ( p->HTable[HKey].Arg1 == (reo_unit *)F )
+            if ( p->HTable[HKey].Arg1 == (unsigned)F )
             {
-                pUnit = p->HTable[HKey].Arg2;  
+                pUnit = (reo_unit*) p->HTable[HKey].Arg2;  
                 assert( pUnit );
                 // increment the edge counter
                 pUnit->n++;
@@ -93,8 +93,8 @@ reo_unit * reoTransferNodesToUnits_rec( reo_man * p, DdNode * F )
         // might have been used. Make sure that its signature is different.
         for ( ; p->HTable[HKey].Sign == p->Signature; HKey = (HKey+1) % p->nTableSize );
         p->HTable[HKey].Sign = p->Signature;
-        p->HTable[HKey].Arg1 = (reo_unit *)F;
-        p->HTable[HKey].Arg2 = pUnit;
+        p->HTable[HKey].Arg1 = (unsigned)F;
+        p->HTable[HKey].Arg2 = (unsigned)pUnit;
     }
 
     // increment the counter of nodes
@@ -126,7 +126,7 @@ DdNode * reoTransferUnitsToNodes_rec( reo_man * p, reo_unit * pUnit )
     if ( pUnit->n != 1 )
     {
         for ( HKey = hashKey2(p->Signature,pUnit,p->nTableSize); p->HTable[HKey].Sign == p->Signature; HKey = (HKey+1) % p->nTableSize )
-            if ( p->HTable[HKey].Arg1 == pUnit )
+            if ( p->HTable[HKey].Arg1 == (unsigned)pUnit )
             {
                 bRes = (DdNode*) p->HTable[HKey].Arg2;  
                 assert( bRes );
@@ -179,8 +179,8 @@ DdNode * reoTransferUnitsToNodes_rec( reo_man * p, reo_unit * pUnit )
          // might have been used. Make sure that its signature is different.
          for ( ; p->HTable[HKey].Sign == p->Signature; HKey = (HKey+1) % p->nTableSize );
          p->HTable[HKey].Sign = p->Signature;
-         p->HTable[HKey].Arg1 = pUnit;
-         p->HTable[HKey].Arg2 = (reo_unit *)bRes;  
+         p->HTable[HKey].Arg1 = (unsigned)pUnit;
+         p->HTable[HKey].Arg2 = (unsigned)bRes;  
 
          // add the DD to the referenced DD list in order to be able to store it in cache
          p->pRefNodes[p->nRefNodes++] = bRes;  Cudd_Ref( bRes );