diff options
Diffstat (limited to 'src/misc/extra/extraUtilPerm.c')
-rw-r--r-- | src/misc/extra/extraUtilPerm.c | 28 |
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 ); |