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

Bug fix for incorrect memory allocation in main SAT solver, leading to crashes in 'dsec'.

This commit is contained in:
Alan Mishchenko 2012-01-22 22:24:23 -08:00
parent fb918249ca
commit 3906e37c12
3 changed files with 6 additions and 6 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

8
src/aig/ivy/ivyFraig.c
View File

@ -2119,9 +2119,9 @@ int Ivy_FraigNodesAreEquiv( Ivy_FraigMan_t * p, Ivy_Obj_t * pOld, Ivy_Obj_t * pN
if ( p->pSat == NULL ) if ( p->pSat == NULL )
{ {
p->pSat = sat_solver_new(); p->pSat = sat_solver_new();
p->pSat->factors = ABC_CALLOC( double, 1 );
p->nSatVars = 1;
sat_solver_setnvars( p->pSat, 1000 ); sat_solver_setnvars( p->pSat, 1000 );
p->pSat->factors = ABC_CALLOC( double, 1000 );
p->nSatVars = 1;
// var 0 is reserved for const1 node - add the clause // var 0 is reserved for const1 node - add the clause
// pLits[0] = toLit( 0 ); // pLits[0] = toLit( 0 );
// sat_solver_addclause( p->pSat, pLits, pLits + 1 ); // sat_solver_addclause( p->pSat, pLits, pLits + 1 );
@ -2271,9 +2271,9 @@ int Ivy_FraigNodeIsConst( Ivy_FraigMan_t * p, Ivy_Obj_t * pNew )
if ( p->pSat == NULL ) if ( p->pSat == NULL )
{ {
p->pSat = sat_solver_new(); p->pSat = sat_solver_new();
p->pSat->factors = ABC_CALLOC( double, 1 );
p->nSatVars = 1;
sat_solver_setnvars( p->pSat, 1000 ); sat_solver_setnvars( p->pSat, 1000 );
p->pSat->factors = ABC_CALLOC( double, 1000 );
p->nSatVars = 1;
// var 0 is reserved for const1 node - add the clause // var 0 is reserved for const1 node - add the clause
// pLits[0] = toLit( 0 ); // pLits[0] = toLit( 0 );
// sat_solver_addclause( p->pSat, pLits, pLits + 1 ); // sat_solver_addclause( p->pSat, pLits, pLits + 1 );

2
src/proof/cec/cecSolve.c
View File

@ -376,8 +376,8 @@ void Cec_ManSatSolverRecycle( Cec_ManSat_t * p )
sat_solver_delete( p->pSat ); sat_solver_delete( p->pSat );
} }
p->pSat = sat_solver_new(); p->pSat = sat_solver_new();
p->pSat->factors = ABC_CALLOC( double, 1 );
sat_solver_setnvars( p->pSat, 1000 ); sat_solver_setnvars( p->pSat, 1000 );
p->pSat->factors = ABC_CALLOC( double, 1000 );
// var 0 is not used // var 0 is not used
// var 1 is reserved for const0 node - add the clause // var 1 is reserved for const0 node - add the clause
p->nSatVars = 1; p->nSatVars = 1;

2
src/proof/fra/fraSat.c
View File

@ -512,7 +512,7 @@ int Fra_SetActivityFactors_rec( Fra_Man_t * p, Aig_Obj_t * pObj, int LevelMin, i
// 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 ) if ( p->pSat->factors == NULL )
p->pSat->factors = ABC_CALLOC( double, p->pSat->size ); p->pSat->factors = ABC_CALLOC( double, p->pSat->cap );
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