diff options
| author | Alan Mishchenko <alanmi@berkeley.edu> | 2017-09-16 12:48:23 -0700 |
|---|---|---|
| committer | Alan Mishchenko <alanmi@berkeley.edu> | 2017-09-16 12:48:23 -0700 |
| commit | 6d2efdf28f95867119708b7361418c749daedf37 (patch) | |
| tree | da46388f568cf0cf03fbb63e96e179f3d8a92fb5 /src/sat/glucose | |
| parent | f5cb9d6448a9c1d450fd9f578c18b7b51c290fd4 (diff) | |
| download | abc-6d2efdf28f95867119708b7361418c749daedf37.tar.gz abc-6d2efdf28f95867119708b7361418c749daedf37.tar.bz2 abc-6d2efdf28f95867119708b7361418c749daedf37.zip | |
Improvements in Glucose integration.
Diffstat (limited to 'src/sat/glucose')
| -rw-r--r-- | src/sat/glucose/SimpSolver.cpp | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/src/sat/glucose/SimpSolver.cpp b/src/sat/glucose/SimpSolver.cpp index 83d97e77..43d98146 100644 --- a/src/sat/glucose/SimpSolver.cpp +++ b/src/sat/glucose/SimpSolver.cpp @@ -691,6 +691,7 @@ bool SimpSolver::eliminate(bool turn_off_elim) printf("c | Eliminated clauses: %10.2f Mb |\n", double(elimclauses.size() * sizeof(uint32_t)) / (1024*1024)); + printf( "c Simplication removed %d variables and %d clauses. ", eliminated_vars, elimclauses.size() ); Abc_PrintTime( 1, "Time", Abc_Clock() - clk ); return ok; } @@ -704,7 +705,6 @@ void SimpSolver::cleanUpClauses() if (ca[clauses[i]].mark() == 0) clauses[j++] = clauses[i]; clauses.shrink(i - j); - printf( "Simplication removed %d variables and %d clauses. ", eliminated_vars, i - j ); } |