luke
/
abc
mirror of https://github.com/YosysHQ/abc.git
1
0
Fork 0
Code Issues Packages Projects Releases Wiki Activity

Merge pull request #328 from heshpdx/master 

Perf improvement in satsolver
This commit is contained in:
alanminko 2024-10-21 01:38:40 -07:00 committed by GitHub
parent f1773bd612 ad8f8a2aab
commit a239dd8c0b
No known key found for this signature in database
GPG Key ID: B5690EEEBB952194
1 changed files with 5 additions and 4 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

9
src/sat/bsat/satSolver.c
View File

@ -60,9 +60,10 @@ static void printlits(lit* begin, lit* end)
static inline double drand(double* seed) {
int q;
*seed *= 1389796;
q = (int)(*seed / 2147483647);
q = (int)(*seed * 4.6566128752457969e-10); // 1.0/2147483647.0;
*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.
@ -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,