summaryrefslogtreecommitdiffstats
path: root/src/bdd/reo
diff options
context:
space:
mode:
Diffstat (limited to 'src/bdd/reo')
-rw-r--r--src/bdd/reo/module.make1
-rw-r--r--src/bdd/reo/reo.h24
-rw-r--r--src/bdd/reo/reoProfile.c2
-rw-r--r--src/bdd/reo/reoShuffle.c224
-rw-r--r--src/bdd/reo/reoSwap.c26
-rw-r--r--src/bdd/reo/reoTransfer.c14
6 files changed, 263 insertions, 28 deletions
diff --git a/src/bdd/reo/module.make b/src/bdd/reo/module.make
index 7eb41e0e..3a636980 100644
--- a/src/bdd/reo/module.make
+++ b/src/bdd/reo/module.make
@@ -1,6 +1,7 @@
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 7e4be855..1a31242a 100644
--- a/src/bdd/reo/reo.h
+++ b/src/bdd/reo/reo.h
@@ -19,10 +19,16 @@
#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 ///
////////////////////////////////////////////////////////////////////////
@@ -87,9 +93,9 @@ struct _reo_plane
struct _reo_hash
{
int Sign; // signature of the current cache operation
- unsigned Arg1; // the first argument
- unsigned Arg2; // the second argument
- unsigned Arg3; // the second argument
+ reo_unit * Arg1; // the first argument
+ reo_unit * Arg2; // the second argument
+ reo_unit * Arg3; // the third argument
};
struct _reo_man
@@ -166,8 +172,8 @@ struct _reo_man
// used to manipulate units
#define Unit_Regular(u) ((reo_unit *)((unsigned long)(u) & ~01))
-#define Unit_Not(u) ((reo_unit *)((long)(u) ^ 01))
-#define Unit_NotCond(u,c) ((reo_unit *)((long)(u) ^ (c)))
+#define Unit_Not(u) ((reo_unit *)((unsigned long)(u) ^ 01))
+#define Unit_NotCond(u,c) ((reo_unit *)((unsigned long)(u) ^ (c)))
#define Unit_IsConstant(u) ((int)((u)->lev == REO_CONST_LEVEL))
////////////////////////////////////////////////////////////////////////
@@ -215,8 +221,12 @@ 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 b38575f0..84a0bc19 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
new file mode 100644
index 00000000..8dab67a4
--- /dev/null
+++ b/src/bdd/reo/reoShuffle.c
@@ -0,0 +1,224 @@
+/**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 cb730d8e..4afa650c 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 = (unsigned)pUnitE;
- p->HTable[HKey].Arg2 = (unsigned)pUnitT;
- p->HTable[HKey].Arg3 = (unsigned)pUnit;
+ p->HTable[HKey].Arg1 = pUnitE;
+ p->HTable[HKey].Arg2 = pUnitT;
+ p->HTable[HKey].Arg3 = 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 == (unsigned)pNew1E && p->HTable[HKey].Arg2 == (unsigned)pNew1T )
+ if ( p->HTable[HKey].Arg1 == pNew1E && p->HTable[HKey].Arg2 == pNew1T )
{ // the entry is present
// assign this entry
- pNewPlane20 = (reo_unit *)p->HTable[HKey].Arg3;
+ pNewPlane20 = 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 = (unsigned)pNew1E;
- p->HTable[HKey].Arg2 = (unsigned)pNew1T;
- p->HTable[HKey].Arg3 = (unsigned)pNewPlane20;
+ p->HTable[HKey].Arg1 = pNew1E;
+ p->HTable[HKey].Arg2 = pNew1T;
+ p->HTable[HKey].Arg3 = 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 == (unsigned)pNew2E && p->HTable[HKey].Arg2 == (unsigned)pNew2T )
+ if ( p->HTable[HKey].Arg1 == pNew2E && p->HTable[HKey].Arg2 == pNew2T )
{ // the entry is present
// assign this entry
- pNewPlane21 = (reo_unit *)p->HTable[HKey].Arg3;
+ pNewPlane21 = 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 = (unsigned)pNew2E;
- p->HTable[HKey].Arg2 = (unsigned)pNew2T;
- p->HTable[HKey].Arg3 = (unsigned)pNewPlane21;
+ p->HTable[HKey].Arg1 = pNew2E;
+ p->HTable[HKey].Arg2 = pNew2T;
+ p->HTable[HKey].Arg3 = pNewPlane21;
nNodesUnrefAdded++;
diff --git a/src/bdd/reo/reoTransfer.c b/src/bdd/reo/reoTransfer.c
index 752cd3d7..65d31d01 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 == (unsigned)F )
+ if ( p->HTable[HKey].Arg1 == (reo_unit *)F )
{
- pUnit = (reo_unit*) p->HTable[HKey].Arg2;
+ pUnit = 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 = (unsigned)F;
- p->HTable[HKey].Arg2 = (unsigned)pUnit;
+ p->HTable[HKey].Arg1 = (reo_unit *)F;
+ p->HTable[HKey].Arg2 = 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 == (unsigned)pUnit )
+ if ( p->HTable[HKey].Arg1 == 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 = (unsigned)pUnit;
- p->HTable[HKey].Arg2 = (unsigned)bRes;
+ p->HTable[HKey].Arg1 = pUnit;
+ p->HTable[HKey].Arg2 = (reo_unit *)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 );
generated by cgit v1.2.3 (git 2.25.1) at 2024-11-07 16:07:52 +0000