Skip to content

Commit

Permalink
Perf improvement in satsolver
Browse files Browse the repository at this point in the history
Switch one FP divide to an FP multiply (variable is constant).
Calculate ratio inside of verbosity clause, since that is where it is used.
  • Loading branch information
heshpdx committed Sep 3, 2024
1 parent 5d6a568 commit cd71108
Showing 1 changed file with 4 additions and 3 deletions.
7 changes: 4 additions & 3 deletions src/sat/bsat/satSolver.c
Original file line number Diff line number Diff line change
Expand Up @@ -62,7 +62,8 @@ static inline double drand(double* seed) {
*seed *= 1389796;
q = (int)(*seed / 2147483647);
*seed -= (double)q * 2147483647;
return *seed / 2147483647; }
return *seed * 4.6566128752457969e-10; // 1.0/2147483647.0
}


// Returns a random integer 0 <= x < size. Seed must never be 0.
Expand Down Expand Up @@ -1954,12 +1955,12 @@ int sat_solver_solve_internal(sat_solver* s)

while (status == l_Undef){
ABC_INT64_T nof_conflicts;
double Ratio = (s->stats.learnts == 0)? 0.0 :
s->stats.learnts_literals / (double)s->stats.learnts;
if ( s->nRuntimeLimit && Abc_Clock() > s->nRuntimeLimit )
break;
if (s->verbosity >= 1)
{
double Ratio = (s->stats.learnts == 0)? 0.0 :
s->stats.learnts_literals / (double)s->stats.learnts;
printf("| %9.0f | %7.0f %8.0f | %7.0f %7.0f %8.0f %7.1f | %6.3f %% |\n",
(double)s->stats.conflicts,
(double)s->stats.clauses,
Expand Down

0 comments on commit cd71108

Please sign in to comment.