Skip to content

A
abc
Commit 67300e05 by Alan Mishchenko
Options

Small bug induced by changes in the SAT solver.

parent 25914e41
Showing with 2 additions and 0 deletions
src/aig/fra/fraSat.c
...@@ -511,6 +511,8 @@ int Fra_SetActivityFactors_rec( Fra_Man_t * p, Aig_Obj_t * pObj, int LevelMin, i ...@@ -511,6 +511,8 @@ int Fra_SetActivityFactors_rec( Fra_Man_t * p, Aig_Obj_t * pObj, int LevelMin, i
return 0; return 0;
// set the factor of this variable // set the factor of this variable
// (LevelMax-LevelMin) / (pObj->Level-LevelMin) = p->pPars->dActConeBumpMax / ThisBump // (LevelMax-LevelMin) / (pObj->Level-LevelMin) = p->pPars->dActConeBumpMax / ThisBump
if ( p->pSat->factors == NULL )
p->pSat->factors = ABC_CALLOC( double, p->pSat->size );
p->pSat->factors[Fra_ObjSatNum(pObj)] = p->pPars->dActConeBumpMax * (pObj->Level - LevelMin)/(LevelMax - LevelMin); p->pSat->factors[Fra_ObjSatNum(pObj)] = p->pPars->dActConeBumpMax * (pObj->Level - LevelMin)/(LevelMax - LevelMin);
veci_push(&p->pSat->act_vars, Fra_ObjSatNum(pObj)); veci_push(&p->pSat->act_vars, Fra_ObjSatNum(pObj));
// explore the fanins // explore the fanins
......
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