diff options
Diffstat (limited to 'src/base')
-rw-r--r-- | src/base/abci/abc.c | 19 | ||||
-rw-r--r-- | src/base/abci/abcDar.c | 4 | ||||
-rw-r--r-- | src/base/io/io.c | 44 |
3 files changed, 55 insertions, 12 deletions
diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c index 0fb1e406..2bb1d470 100644 --- a/src/base/abci/abc.c +++ b/src/base/abci/abc.c @@ -20965,6 +20965,22 @@ int Abc_CommandDSat( Abc_Frame_t * pAbc, int argc, char ** argv ) } } + if ( argc == globalUtilOptind + 1 ) + { + extern int Cnf_DataSolveFromFile( char * pFileName, int nConfLimit, int fVerbose ); + // get the input file name + char * pFileName = argv[globalUtilOptind]; + FILE * pFile = fopen( pFileName, "rb" ); + if ( pFile == NULL ) + { + printf( "Cannot open file \"%s\" for writing.\n", pFileName ); + return 0; + } + fclose( pFile ); + Cnf_DataSolveFromFile( pFileName, nConfLimit, fVerbose ); + return 0; + } + if ( pNtk == NULL ) { Abc_Print( -1, "Empty network.\n" ); @@ -20987,7 +21003,6 @@ int Abc_CommandDSat( Abc_Frame_t * pAbc, int argc, char ** argv ) Abc_Print( -1, "Currently only works for structurally hashed circuits.\n" ); return 0; } - clk = Abc_Clock(); RetValue = Abc_NtkDSat( pNtk, (ABC_INT64_T)nConfLimit, (ABC_INT64_T)nInsLimit, nLearnedStart, nLearnedDelta, nLearnedPerce, fAlignPol, fAndOuts, fNewSolver, fVerbose ); // verify that the pattern is correct @@ -31406,6 +31421,8 @@ int Abc_CommandAbc9Mf( Abc_Frame_t * pAbc, int argc, char ** argv ) Abc_Print( -1, "Abc_CommandAbc9Lf(): Mapping into LUTs has failed.\n" ); return 1; } + if ( pPars->fGenCnf ) + Cnf_DataFree( pAbc->pGia->pData ), pAbc->pGia->pData = NULL; Abc_FrameUpdateGia( pAbc, pNew ); return 0; diff --git a/src/base/abci/abcDar.c b/src/base/abci/abcDar.c index 894c9d17..e45c604d 100644 --- a/src/base/abci/abcDar.c +++ b/src/base/abci/abcDar.c @@ -1561,9 +1561,9 @@ Abc_Ntk_t * Abc_NtkDarToCnf( Abc_Ntk_t * pNtk, char * pFileName, int fFastAlgo, Cnf_DataTranformPolarity( pCnf, 0 ); // print stats - if ( fVerbose ) +// if ( fVerbose ) { - Abc_Print( 1, "Vars = %6d. Clauses = %7d. Literals = %8d. ", pCnf->nVars, pCnf->nClauses, pCnf->nLiterals ); + Abc_Print( 1, "CNF stats: Vars = %6d. Clauses = %7d. Literals = %8d. ", pCnf->nVars, pCnf->nClauses, pCnf->nLiterals ); Abc_PrintTime( 1, "Time", Abc_Clock() - clk ); } diff --git a/src/base/io/io.c b/src/base/io/io.c index d5ef65b8..2e796cd6 100644 --- a/src/base/io/io.c +++ b/src/base/io/io.c @@ -1938,15 +1938,30 @@ usage: ***********************************************************************/ int IoCommandWriteCnf2( Abc_Frame_t * pAbc, int argc, char **argv ) { - extern void Jf_ManDumpCnf( Gia_Man_t * p, char * pFileName ); + extern void Jf_ManDumpCnf( Gia_Man_t * p, char * pFileName, int fVerbose ); + extern void Mf_ManDumpCnf( Gia_Man_t * p, char * pFileName, int nLutSize, int fVerbose ); FILE * pFile; char * pFileName; + int nLutSize = 6; + int fNewAlgo = 1; int c, fVerbose = 0; Extra_UtilGetoptReset(); - while ( ( c = Extra_UtilGetopt( argc, argv, "vh" ) ) != EOF ) + while ( ( c = Extra_UtilGetopt( argc, argv, "Kavh" ) ) != EOF ) { switch ( c ) { + case 'K': + if ( globalUtilOptind >= argc ) + { + Abc_Print( -1, "Command line switch \"-K\" should be followed by an integer.\n" ); + goto usage; + } + nLutSize = atoi(argv[globalUtilOptind]); + globalUtilOptind++; + break; + case 'a': + fNewAlgo ^= 1; + break; case 'v': fVerbose ^= 1; break; @@ -1966,7 +1981,12 @@ int IoCommandWriteCnf2( Abc_Frame_t * pAbc, int argc, char **argv ) Abc_Print( -1, "IoCommandWriteCnf2(): Works only for combinational miters.\n" ); return 0; } - if ( !Sdm_ManCanRead() ) + if ( nLutSize < 3 || nLutSize > 8 ) + { + Abc_Print( -1, "IoCommandWriteCnf2(): Invalid LUT size (%d).\n", nLutSize ); + return 0; + } + if ( !fNewAlgo && !Sdm_ManCanRead() ) { Abc_Print( -1, "IoCommandWriteCnf2(): Cannot input precomputed DSD information.\n" ); return 0; @@ -1981,15 +2001,21 @@ int IoCommandWriteCnf2( Abc_Frame_t * pAbc, int argc, char **argv ) printf( "Cannot open file \"%s\" for writing.\n", pFileName ); return 0; } - Jf_ManDumpCnf( pAbc->pGia, pFileName ); + fclose( pFile ); + if ( fNewAlgo ) + Mf_ManDumpCnf( pAbc->pGia, pFileName, nLutSize, fVerbose ); + else + Jf_ManDumpCnf( pAbc->pGia, pFileName, fVerbose ); return 0; usage: - fprintf( pAbc->Err, "usage: &write_cnf [-vh] <file>\n" ); - fprintf( pAbc->Err, "\t writes CNF produced by new DSD-based generator\n" ); - 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" ); + fprintf( pAbc->Err, "usage: &write_cnf [-Kavh] <file>\n" ); + fprintf( pAbc->Err, "\t writes CNF produced by a new generator\n" ); + fprintf( pAbc->Err, "\t-K <num> : the LUT size (3 <= num <= 8) [default = %d]\n", nLutSize ); + fprintf( pAbc->Err, "\t-a : toggle using new algorithm [default = %s]\n", fNewAlgo? "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; } |