summaryrefslogtreecommitdiffstats
path: root/src/misc/extra/extraUtilPerm.c
diff options
context:
space:
mode:
Diffstat (limited to 'src/misc/extra/extraUtilPerm.c')
-rw-r--r--src/misc/extra/extraUtilPerm.c28
1 files changed, 13 insertions, 15 deletions
diff --git a/src/misc/extra/extraUtilPerm.c b/src/misc/extra/extraUtilPerm.c
index ccabdf41..25c221ec 100644
--- a/src/misc/extra/extraUtilPerm.c
+++ b/src/misc/extra/extraUtilPerm.c
@@ -863,16 +863,16 @@ void Abc_EnumerateCubeStatesZdd()
{ {1,10}, {1, 7}, {1, 4}, {3,12}, {3, 9}, {3, 6}, {2,11}, {2, 8}, {2, 5} } };
Abc_ZddMan * p;
int i, k, pComb[9], pPerm[24], nSize;
- int ZddTurn1, ZddTurn2, ZddTurn3, ZddTurns9, ZddAll, ZddReached, ZddNew;
+ int ZddTurn1, ZddTurn2, ZddTurn3, ZddTurns, ZddAll;
abctime clk = Abc_Clock();
printf( "Enumerating states of 2x2x2 cube.\n" );
- p = Abc_ZddManAlloc( 24 * 23 / 2, 1 << 27 );
+ p = Abc_ZddManAlloc( 24 * 23 / 2, 1 << 27 ); // finished with 2^27 (4 GB)
Abc_ZddManCreatePerms( p, 24 );
// init state
printf( "Iter %2d -> %8d ", 0, 1 );
Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
// first 9 states
- ZddTurns9 = 0;
+ ZddTurns = 1;
for ( i = 0; i < 3; i++ )
{
for ( k = 0; k < 24; k++ )
@@ -885,32 +885,30 @@ void Abc_EnumerateCubeStatesZdd()
pComb[k] = Abc_ZddVarIJ( p, pComb[k] >> 16, pComb[k] & 0xffff );
// add first turn
ZddTurn1 = Abc_ZddBuildSet( p, pComb, 9 );
- ZddTurns9 = Abc_ZddUnion( p, ZddTurns9, ZddTurn1 );
+ ZddTurns = Abc_ZddUnion( p, ZddTurns, ZddTurn1 );
//Abc_ZddPrint( p, ZddTurn1 );
// add second turn
ZddTurn2 = Abc_ZddPermProduct( p, ZddTurn1, ZddTurn1 );
- ZddTurns9 = Abc_ZddUnion( p, ZddTurns9, ZddTurn2 );
+ ZddTurns = Abc_ZddUnion( p, ZddTurns, ZddTurn2 );
//Abc_ZddPrint( p, ZddTurn2 );
// add third turn
ZddTurn3 = Abc_ZddPermProduct( p, ZddTurn2, ZddTurn1 );
- ZddTurns9 = Abc_ZddUnion( p, ZddTurns9, ZddTurn3 );
+ ZddTurns = Abc_ZddUnion( p, ZddTurns, ZddTurn3 );
//Abc_ZddPrint( p, ZddTurn3 );
//printf( "\n" );
}
- //Abc_ZddPrint( p, ZddTurns9 );
- printf( "Iter %2d -> %8d ", 1, Abc_ZddCountPaths(p, ZddTurns9) );
+ //Abc_ZddPrint( p, ZddTurns );
+ printf( "Iter %2d -> %8d ", 1, Abc_ZddCountPaths(p, ZddTurns) );
Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
// other states
- ZddNew = ZddTurns9;
- ZddAll = Abc_ZddUnion( p, 1, ZddTurns9 );
+ ZddAll = ZddTurns;
for ( i = 2; i <= 100; i++ )
{
- ZddReached = Abc_ZddPermProduct( p, ZddNew, ZddTurns9 );
- ZddNew = Abc_ZddDiff( p, ZddReached, ZddAll );
- ZddAll = Abc_ZddUnion( p, ZddAll, ZddNew );
- printf( "Iter %2d -> %8d ", i, Abc_ZddCountPaths(p, ZddNew) );
+ int ZddAllPrev = ZddAll;
+ ZddAll = Abc_ZddPermProduct( p, ZddAll, ZddTurns );
+ printf( "Iter %2d -> %8d ", i, Abc_ZddCountPaths(p, ZddAll) );
Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
- if ( ZddNew == 0 )
+ if ( ZddAllPrev == ZddAll )
break;
}
Abc_ZddManFree( p );