diff options
| author | Alan Mishchenko <alanmi@berkeley.edu> | 2011-10-17 10:39:05 +0300 |
|---|---|---|
| committer | Alan Mishchenko <alanmi@berkeley.edu> | 2011-10-17 10:39:05 +0300 |
| commit | 12b70d49463ae87486d1a4080c67140e2aa9fa4e (patch) | |
| tree | abcc25ebae10c58c6d2f046db6c19ff106ec2563 /src/base/abci/abcDar.c | |
| parent | 6f0b87dd5c5c7f4f5dec04e9c146d60188acf3c2 (diff) | |
| download | abc-12b70d49463ae87486d1a4080c67140e2aa9fa4e.tar.gz abc-12b70d49463ae87486d1a4080c67140e2aa9fa4e.tar.bz2 abc-12b70d49463ae87486d1a4080c67140e2aa9fa4e.zip | |
Changes to CNF generation code.
Diffstat (limited to 'src/base/abci/abcDar.c')
| -rw-r--r-- | src/base/abci/abcDar.c | 23 |
1 files changed, 18 insertions, 5 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; } |