diff options
author | Alan Mishchenko <alanmi@berkeley.edu> | 2007-08-28 08:01:00 -0700 |
---|---|---|
committer | Alan Mishchenko <alanmi@berkeley.edu> | 2007-08-28 08:01:00 -0700 |
commit | ddc6d1c1682a18e293399b7d6c9f4a9018c30c70 (patch) | |
tree | 165c2a7ebb0561d9272673ce8caaa012f82d4717 /src/opt/fxu/fxuCreate.c | |
parent | 28467823812f63a40f9a322b1fefc7decce4b766 (diff) | |
download | abc-ddc6d1c1682a18e293399b7d6c9f4a9018c30c70.tar.gz abc-ddc6d1c1682a18e293399b7d6c9f4a9018c30c70.tar.bz2 abc-ddc6d1c1682a18e293399b7d6c9f4a9018c30c70.zip |
Version abc70828
Diffstat (limited to 'src/opt/fxu/fxuCreate.c')
-rw-r--r-- | src/opt/fxu/fxuCreate.c | 21 |
1 files changed, 17 insertions, 4 deletions
diff --git a/src/opt/fxu/fxuCreate.c b/src/opt/fxu/fxuCreate.c index 99942a88..e3300df9 100644 --- a/src/opt/fxu/fxuCreate.c +++ b/src/opt/fxu/fxuCreate.c @@ -178,12 +178,26 @@ Fxu_Matrix * Fxu_CreateMatrix( Fxu_Data_t * pData ) // consider the case when cube pairs should be preprocessed // before adding them to the set of divisors +// if ( pData->fVerbose ) +// printf( "The total number of cube pairs is %d.\n", nPairsTotal ); + if ( nPairsTotal > 10000000 ) + { + printf( "The total number of cube pairs of the network is more than 10,000,000.\n" ); + printf( "Command \"fx\" takes a long time to run in such cases. It is suggested\n" ); + printf( "that the user changes the network by reducing the size of logic node and\n" ); + printf( "consequently the number of cube pairs to be processed by this command.\n" ); + printf( "One way to achieve this is to run the commands \"st; multi -m -F <num>\"\n" ); + printf( "as a proprocessing step, while selecting <num> as approapriate.\n" ); + return NULL; + } if ( nPairsTotal > pData->nPairsMax ) if ( !Fxu_PreprocessCubePairs( p, pData->vSops, nPairsTotal, pData->nPairsMax ) ) return NULL; +// if ( pData->fVerbose ) +// printf( "Only %d best cube pairs will be used by the fast extract command.\n", pData->nPairsMax ); // add the var pairs to the heap - Fxu_MatrixComputeSingles( p ); + Fxu_MatrixComputeSingles( p, pData->fUse0, pData->nSingleMax ); // print stats if ( pData->fVerbose ) @@ -194,9 +208,8 @@ Fxu_Matrix * Fxu_CreateMatrix( Fxu_Data_t * pData ) p->lVars.nItems, p->lCubes.nItems ); fprintf( stdout, "Lits = %d Density = %.5f%%\n", p->nEntries, Density ); - fprintf( stdout, "1-cube divisors = %6d. ", p->lSingles.nItems ); - fprintf( stdout, "2-cube divisors = %6d. ", p->nDivsTotal ); - fprintf( stdout, "Cube pairs = %6d.", nPairsTotal ); + fprintf( stdout, "1-cube divs = %6d. (Total = %6d) ", p->lSingles.nItems, p->nSingleTotal ); + fprintf( stdout, "2-cube divs = %6d. (Total = %6d)", p->nDivsTotal, nPairsTotal ); fprintf( stdout, "\n" ); } // Fxu_MatrixPrint( stdout, p ); |