Commit 6d2efdf2 by Alan Mishchenko

Improvements in Glucose integration.

parent f5cb9d64
...@@ -691,6 +691,7 @@ bool SimpSolver::eliminate(bool turn_off_elim) ...@@ -691,6 +691,7 @@ bool SimpSolver::eliminate(bool turn_off_elim)
printf("c | Eliminated clauses: %10.2f Mb |\n", printf("c | Eliminated clauses: %10.2f Mb |\n",
double(elimclauses.size() * sizeof(uint32_t)) / (1024*1024)); 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 ); Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
return ok; return ok;
} }
...@@ -704,7 +705,6 @@ void SimpSolver::cleanUpClauses() ...@@ -704,7 +705,6 @@ void SimpSolver::cleanUpClauses()
if (ca[clauses[i]].mark() == 0) if (ca[clauses[i]].mark() == 0)
clauses[j++] = clauses[i]; clauses[j++] = clauses[i];
clauses.shrink(i - j); clauses.shrink(i - j);
printf( "Simplication removed %d variables and %d clauses. ", eliminated_vars, i - j );
} }
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment