diff options
| author | Alan Mishchenko <alanmi@berkeley.edu> | 2014-06-23 13:11:59 -0700 |
|---|---|---|
| committer | Alan Mishchenko <alanmi@berkeley.edu> | 2014-06-23 13:11:59 -0700 |
| commit | 44d9c7e54307f64cbcdc7c8cd17ff6e219e13b55 (patch) | |
| tree | 2ae1aa5fef6ca8198f0c2fb6123c3d1494dbe2b4 /src/proof/fra/fraCec.c | |
| parent | f93e5244219b75224df0c75b424654bd2424852b (diff) | |
| download | abc-44d9c7e54307f64cbcdc7c8cd17ff6e219e13b55.tar.gz abc-44d9c7e54307f64cbcdc7c8cd17ff6e219e13b55.tar.bz2 abc-44d9c7e54307f64cbcdc7c8cd17ff6e219e13b55.zip | |
Improvements to CNF generation.
Diffstat (limited to 'src/proof/fra/fraCec.c')
| -rw-r--r-- | src/proof/fra/fraCec.c | 12 |
1 files changed, 12 insertions, 0 deletions
diff --git a/src/proof/fra/fraCec.c b/src/proof/fra/fraCec.c index 3e51bf1e..fe113367 100644 --- a/src/proof/fra/fraCec.c +++ b/src/proof/fra/fraCec.c @@ -67,6 +67,12 @@ int Fra_FraigSat( Aig_Man_t * pMan, ABC_INT64_T nConfLimit, ABC_INT64_T nInsLimi if ( fFlipBits ) Cnf_DataTranformPolarity( pCnf, 0 ); + if ( fVerbose ) + { + printf( "CNF stats: Vars = %6d. Clauses = %7d. Literals = %8d. ", pCnf->nVars, pCnf->nClauses, pCnf->nLiterals ); + Abc_PrintTime( 1, "Time", Abc_Clock() - clk ); + } + // convert into SAT solver pSat = (sat_solver2 *)Cnf_DataWriteIntoSolver2( pCnf, 1, 0 ); if ( pSat == NULL ) @@ -173,6 +179,12 @@ int Fra_FraigSat( Aig_Man_t * pMan, ABC_INT64_T nConfLimit, ABC_INT64_T nInsLimi if ( fFlipBits ) Cnf_DataTranformPolarity( pCnf, 0 ); + if ( fVerbose ) + { + printf( "CNF stats: Vars = %6d. Clauses = %7d. Literals = %8d. ", pCnf->nVars, pCnf->nClauses, pCnf->nLiterals ); + Abc_PrintTime( 1, "Time", Abc_Clock() - clk ); + } + // convert into SAT solver pSat = (sat_solver *)Cnf_DataWriteIntoSolver( pCnf, 1, 0 ); if ( pSat == NULL ) |