diff options
| author | Alan Mishchenko <alanmi@berkeley.edu> | 2006-09-16 08:01:00 -0700 |
|---|---|---|
| committer | Alan Mishchenko <alanmi@berkeley.edu> | 2006-09-16 08:01:00 -0700 |
| commit | 370578bf1c4504b65f49ab63fcf7ed9c88a15d69 (patch) | |
| tree | d8297df3e080f52c6526fd7ccded9dd4cc601f2d /src/sat/msat/msatActivity.c | |
| parent | aab0c478e4c78c6856919fcd1027583ca148f3eb (diff) | |
| download | abc-370578bf1c4504b65f49ab63fcf7ed9c88a15d69.tar.gz abc-370578bf1c4504b65f49ab63fcf7ed9c88a15d69.tar.bz2 abc-370578bf1c4504b65f49ab63fcf7ed9c88a15d69.zip | |
Version abc60916
Diffstat (limited to 'src/sat/msat/msatActivity.c')
| -rw-r--r-- | src/sat/msat/msatActivity.c | 5 |
1 files changed, 3 insertions, 2 deletions
diff --git a/src/sat/msat/msatActivity.c b/src/sat/msat/msatActivity.c index 23925669..1cd795bd 100644 --- a/src/sat/msat/msatActivity.c +++ b/src/sat/msat/msatActivity.c @@ -45,8 +45,9 @@ void Msat_SolverVarBumpActivity( Msat_Solver_t * p, Msat_Lit_t Lit ) if ( p->dVarDecay < 0 ) // (negative decay means static variable order -- don't bump) return; Var = MSAT_LIT2VAR(Lit); - if ( (p->pdActivity[Var] += p->dVarInc) > 1e100 ) -// if ( (p->pdActivity[Var] += p->dVarInc * (1.0 + 0.005*p->pActLevels[Var])) > 1e100 ) + p->pdActivity[Var] += p->dVarInc; +// p->pdActivity[Var] += p->dVarInc * p->pFactors[Var]; + if ( p->pdActivity[Var] > 1e100 ) Msat_SolverVarRescaleActivity( p ); Msat_OrderUpdate( p->pOrder, Var ); } |