diff options
Diffstat (limited to 'src/base')
| -rw-r--r-- | src/base/abci/abcDar.c | 23 | ||||
| -rw-r--r-- | src/base/io/io.c | 32 |
2 files changed, 44 insertions, 11 deletions
diff --git a/src/base/abci/abcDar.c b/src/base/abci/abcDar.c index 7efc062e..13aeaaa0 100644 --- a/src/base/abci/abcDar.c +++ b/src/base/abci/abcDar.c @@ -1172,13 +1172,14 @@ Abc_Ntk_t * Abc_NtkConstructFromCnf( Abc_Ntk_t * pNtk, Cnf_Man_t * p, Vec_Ptr_t SeeAlso [] ***********************************************************************/ -Abc_Ntk_t * Abc_NtkDarToCnf( Abc_Ntk_t * pNtk, char * pFileName ) +Abc_Ntk_t * Abc_NtkDarToCnf( Abc_Ntk_t * pNtk, char * pFileName, int fFastAlgo, int fChangePol, int fVerbose ) { Vec_Ptr_t * vMapped = NULL; Aig_Man_t * pMan; Cnf_Man_t * pManCnf = NULL; Cnf_Dat_t * pCnf; Abc_Ntk_t * pNtkNew = NULL; + int clk = clock(); assert( Abc_NtkIsStrash(pNtk) ); // convert to the AIG manager @@ -1192,12 +1193,25 @@ Abc_Ntk_t * Abc_NtkDarToCnf( Abc_Ntk_t * pNtk, char * pFileName ) return NULL; } // perform balance + if ( fVerbose ) Aig_ManPrintStats( pMan ); // derive CNF - pCnf = Cnf_Derive( pMan, 0 ); - Cnf_DataTranformPolarity( pCnf, 0 ); - printf( "Vars = %6d. Clauses = %7d. Literals = %8d.\n", pCnf->nVars, pCnf->nClauses, pCnf->nLiterals ); + if ( fFastAlgo ) + pCnf = Cnf_DeriveFast( pMan, 0 ); + else + pCnf = Cnf_Derive( pMan, 0 ); + + // adjust polarity + if ( fChangePol ) + Cnf_DataTranformPolarity( pCnf, 0 ); + + // print stats + if ( fVerbose ) + { + printf( "Vars = %6d. Clauses = %7d. Literals = %8d. ", pCnf->nVars, pCnf->nClauses, pCnf->nLiterals ); + Abc_PrintTime( 1, "Time", clock() - clk ); + } /* // write the network for verification @@ -1210,7 +1224,6 @@ Abc_Ntk_t * Abc_NtkDarToCnf( Abc_Ntk_t * pNtk, char * pFileName ) Cnf_DataWriteIntoFile( pCnf, pFileName, 0 ); Cnf_DataFree( pCnf ); Cnf_ClearMemory(); - Aig_ManStop( pMan ); return pNtkNew; } diff --git a/src/base/io/io.c b/src/base/io/io.c index 3b85a020..60085168 100644 --- a/src/base/io/io.c +++ b/src/base/io/io.c @@ -1865,23 +1865,38 @@ int IoCommandWriteCnf( Abc_Frame_t * pAbc, int argc, char **argv ) { char * pFileName; int c; - int fAllPrimes; int fNewAlgo; - extern Abc_Ntk_t * Abc_NtkDarToCnf( Abc_Ntk_t * pNtk, char * pFileName ); + int fFastAlgo; + int fAllPrimes; + int fChangePol; + int fVerbose; + extern Abc_Ntk_t * Abc_NtkDarToCnf( Abc_Ntk_t * pNtk, char * pFileName, int fFastAlgo, int fChangePol, int fVerbose ); fNewAlgo = 1; + fFastAlgo = 0; fAllPrimes = 0; + fChangePol = 1; + fVerbose = 0; Extra_UtilGetoptReset(); - while ( ( c = Extra_UtilGetopt( argc, argv, "nph" ) ) != EOF ) + while ( ( c = Extra_UtilGetopt( argc, argv, "nfpcvh" ) ) != EOF ) { switch ( c ) { case 'n': fNewAlgo ^= 1; break; + case 'f': + fFastAlgo ^= 1; + break; case 'p': fAllPrimes ^= 1; break; + case 'c': + fChangePol ^= 1; + break; + case 'v': + fVerbose ^= 1; + break; case 'h': goto usage; default: @@ -1904,8 +1919,10 @@ int IoCommandWriteCnf( Abc_Frame_t * pAbc, int argc, char **argv ) printf( "Warning: Selected option to write all primes has no effect when deriving CNF from AIG.\n" ); } // call the corresponding file writer - if ( fNewAlgo ) - Abc_NtkDarToCnf( pAbc->pNtkCur, pFileName ); + if ( fFastAlgo ) + Abc_NtkDarToCnf( pAbc->pNtkCur, pFileName, 1, fChangePol, fVerbose ); + else if ( fNewAlgo ) + Abc_NtkDarToCnf( pAbc->pNtkCur, pFileName, 0, fChangePol, fVerbose ); else if ( fAllPrimes ) Io_WriteCnf( pAbc->pNtkCur, pFileName, 1 ); else @@ -1913,10 +1930,13 @@ int IoCommandWriteCnf( Abc_Frame_t * pAbc, int argc, char **argv ) return 0; usage: - fprintf( pAbc->Err, "usage: write_cnf [-nph] <file>\n" ); + fprintf( pAbc->Err, "usage: write_cnf [-nfpcvh] <file>\n" ); fprintf( pAbc->Err, "\t writes the miter cone into a CNF file\n" ); fprintf( pAbc->Err, "\t-n : toggle using new algorithm [default = %s]\n", fNewAlgo? "yes" : "no" ); + fprintf( pAbc->Err, "\t-f : toggle using fast algorithm [default = %s]\n", fFastAlgo? "yes" : "no" ); fprintf( pAbc->Err, "\t-p : toggle using all primes to enhance implicativity [default = %s]\n", fAllPrimes? "yes" : "no" ); + fprintf( pAbc->Err, "\t-c : toggle adjasting polarity of internal variables [default = %s]\n", fChangePol? "yes" : "no" ); + fprintf( pAbc->Err, "\t-v : toggle printing verbose information [default = %s]\n", fVerbose? "yes" : "no" ); fprintf( pAbc->Err, "\t-h : print the help massage\n" ); fprintf( pAbc->Err, "\tfile : the name of the file to write\n" ); return 1; |