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

Bug fix related to not properly resizing SAT solver's model array.

This commit is contained in:
Alan Mishchenko 2012-01-06 11:34:06 +07:00
parent 26b87c8c55
commit 10ad89490a
11 changed files with 45 additions and 151 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

3
src/aig/fra/fraClaus.c
View File

@ -1303,7 +1303,8 @@ int Fra_ClausInductiveClauses( Clu_Man_t * p )
if ( RetValue != l_False )
{
// printf( "S- " );
Fra_ClausSimInfoRecord( p, (int*)p->pSatMain->model.ptr + p->nFrames * p->pCnf->nVars );
// Fra_ClausSimInfoRecord( p, (int*)p->pSatMain->model.ptr + p->nFrames * p->pCnf->nVars );
Fra_ClausSimInfoRecord( p, (int*)p->pSatMain->model + p->nFrames * p->pCnf->nVars );
// RetValue = Fra_ClausSimInfoCheck(p, pStart + Beg, End - Beg);
// assert( RetValue );

3
src/aig/fra/fraSim.c
View File

@ -244,7 +244,8 @@ void Fra_SmlSavePattern( Fra_Man_t * p )
int i;
memset( p->pPatWords, 0, sizeof(unsigned) * p->nPatWords );
Aig_ManForEachPi( p->pManFraig, pObj, i )
if ( p->pSat->model.ptr[Fra_ObjSatNum(pObj)] == l_True )
// if ( p->pSat->model.ptr[Fra_ObjSatNum(pObj)] == l_True )
if ( sat_solver_var_value(p->pSat, Fra_ObjSatNum(pObj)) )
Aig_InfoSetBit( p->pPatWords, i );
if ( p->vCex )

112
src/aig/gia/giaAbsVta.c
View File

@ -83,118 +83,6 @@ extern Vec_Int_t * Gia_VtaCollect( Gia_Man_t * p, Vec_Int_t ** pvFraLims, Vec_In
/// FUNCTION DEFINITIONS ///
////////////////////////////////////////////////////////////////////////
static inline int sat_solver2_add_const( sat_solver2 * pSat, int iVar, int fCompl, int fMark )
{
lit Lits[1];
int Cid;
assert( iVar >= 0 );
Lits[0] = toLitCond( iVar, fCompl );
Cid = sat_solver2_addclause( pSat, Lits, Lits + 1 );
if ( fMark )
clause_set_partA( pSat, Cid, 1 );
return 1;
}
static inline int sat_solver2_add_buffer( sat_solver2 * pSat, int iVarA, int iVarB, int fCompl, int fMark )
{
lit Lits[2];
int Cid;
assert( iVarA >= 0 && iVarB >= 0 );
Lits[0] = toLitCond( iVarA, 0 );
Lits[1] = toLitCond( iVarB, !fCompl );
Cid = sat_solver2_addclause( pSat, Lits, Lits + 2 );
if ( fMark )
clause_set_partA( pSat, Cid, 1 );
Lits[0] = toLitCond( iVarA, 1 );
Lits[1] = toLitCond( iVarB, fCompl );
Cid = sat_solver2_addclause( pSat, Lits, Lits + 2 );
if ( fMark )
clause_set_partA( pSat, Cid, 1 );
return 2;
}
static inline int sat_solver2_add_and( sat_solver2 * pSat, int iVar, int iVar0, int iVar1, int fCompl0, int fCompl1, int fMark )
{
lit Lits[3];
int Cid;
Lits[0] = toLitCond( iVar, 1 );
Lits[1] = toLitCond( iVar0, fCompl0 );
Cid = sat_solver2_addclause( pSat, Lits, Lits + 2 );
if ( fMark )
clause_set_partA( pSat, Cid, 1 );
Lits[0] = toLitCond( iVar, 1 );
Lits[1] = toLitCond( iVar1, fCompl1 );
Cid = sat_solver2_addclause( pSat, Lits, Lits + 2 );
if ( fMark )
clause_set_partA( pSat, Cid, 1 );
Lits[0] = toLitCond( iVar, 0 );
Lits[1] = toLitCond( iVar0, !fCompl0 );
Lits[2] = toLitCond( iVar1, !fCompl1 );
Cid = sat_solver2_addclause( pSat, Lits, Lits + 3 );
if ( fMark )
clause_set_partA( pSat, Cid, 1 );
return 3;
}
static inline int sat_solver2_add_xor( sat_solver2 * pSat, int iVarA, int iVarB, int iVarC, int fCompl, int fMark )
{
lit Lits[3];
int Cid;
assert( iVarA >= 0 && iVarB >= 0 && iVarC >= 0 );
Lits[0] = toLitCond( iVarA, !fCompl );
Lits[1] = toLitCond( iVarB, 1 );
Lits[2] = toLitCond( iVarC, 1 );
Cid = sat_solver2_addclause( pSat, Lits, Lits + 3 );
if ( fMark )
clause_set_partA( pSat, Cid, 1 );
Lits[0] = toLitCond( iVarA, !fCompl );
Lits[1] = toLitCond( iVarB, 0 );
Lits[2] = toLitCond( iVarC, 0 );
Cid = sat_solver2_addclause( pSat, Lits, Lits + 3 );
if ( fMark )
clause_set_partA( pSat, Cid, 1 );
Lits[0] = toLitCond( iVarA, fCompl );
Lits[1] = toLitCond( iVarB, 1 );
Lits[2] = toLitCond( iVarC, 0 );
Cid = sat_solver2_addclause( pSat, Lits, Lits + 3 );
if ( fMark )
clause_set_partA( pSat, Cid, 1 );
Lits[0] = toLitCond( iVarA, fCompl );
Lits[1] = toLitCond( iVarB, 0 );
Lits[2] = toLitCond( iVarC, 1 );
Cid = sat_solver2_addclause( pSat, Lits, Lits + 3 );
if ( fMark )
clause_set_partA( pSat, Cid, 1 );
return 4;
}
static inline int sat_solver2_add_constraint( sat_solver2 * pSat, int iVar, int fCompl, int fMark )
{
lit Lits[2];
int Cid;
assert( iVar >= 0 );
Lits[0] = toLitCond( iVar, fCompl );
Lits[1] = toLitCond( iVar+1, 0 );
Cid = sat_solver2_addclause( pSat, Lits, Lits + 2 );
if ( fMark )
clause_set_partA( pSat, Cid, 1 );
Lits[0] = toLitCond( iVar, fCompl );
Lits[1] = toLitCond( iVar+1, 1 );
Cid = sat_solver2_addclause( pSat, Lits, Lits + 2 );
if ( fMark )
clause_set_partA( pSat, Cid, 1 );
return 2;
}
/**Function*************************************************************

7
src/aig/int/intContain.c
View File

@ -274,7 +274,12 @@ int Inter_ManCheckUniqueness( Aig_Man_t * p, sat_solver * pSat, Cnf_Dat_t * pCnf
int Counter;
if ( nFrames == 1 )
return 1;
if ( pSat->model.size == 0 )
// if ( pSat->model.size == 0 )
// possible consequences here!!!
assert( 0 );
if ( sat_solver_nvars(pSat) == 0 )
return 1;
// assert( Saig_ManPoNum(p) == 1 );
assert( Aig_ManRegNum(p) > 0 );

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

@ -1518,7 +1518,8 @@ int * Ivy_FraigCreateModel( Ivy_FraigMan_t * p )
int i;
pModel = ABC_ALLOC( int, Ivy_ManPiNum(p->pManFraig) );
Ivy_ManForEachPi( p->pManFraig, pObj, i )
pModel[i] = ( p->pSat->model.ptr[Ivy_ObjSatNum(pObj)] == l_True );
// pModel[i] = ( p->pSat->model.ptr[Ivy_ObjSatNum(pObj)] == l_True );
pModel[i] = ( p->pSat->model[Ivy_ObjSatNum(pObj)] == l_True );
return pModel;
}
@ -1540,7 +1541,8 @@ void Ivy_FraigSavePattern( Ivy_FraigMan_t * p )
memset( p->pPatWords, 0, sizeof(unsigned) * p->nPatWords );
Ivy_ManForEachPi( p->pManFraig, pObj, i )
// Vec_PtrForEachEntry( Ivy_Obj_t *, p->vPiVars, pObj, i )
if ( p->pSat->model.ptr[Ivy_ObjSatNum(pObj)] == l_True )
// if ( p->pSat->model.ptr[Ivy_ObjSatNum(pObj)] == l_True )
if ( p->pSat->model[Ivy_ObjSatNum(pObj)] == l_True )
Ivy_InfoSetBit( p->pPatWords, i );
// Ivy_InfoSetBit( p->pPatWords, pObj->Id - 1 );
}
@ -1563,7 +1565,8 @@ void Ivy_FraigSavePattern2( Ivy_FraigMan_t * p )
memset( p->pPatWords, 0, sizeof(unsigned) * p->nPatWords );
// Ivy_ManForEachPi( p->pManFraig, pObj, i )
Vec_PtrForEachEntry( Ivy_Obj_t *, p->vPiVars, pObj, i )
if ( p->pSat->model.ptr[Ivy_ObjSatNum(pObj)] == l_True )
// if ( p->pSat->model.ptr[Ivy_ObjSatNum(pObj)] == l_True )
if ( p->pSat->model[Ivy_ObjSatNum(pObj)] == l_True )
// Ivy_InfoSetBit( p->pPatWords, i );
Ivy_InfoSetBit( p->pPatWords, pObj->Id - 1 );
}
@ -1586,7 +1589,8 @@ void Ivy_FraigSavePattern3( Ivy_FraigMan_t * p )
for ( i = 0; i < p->nPatWords; i++ )
p->pPatWords[i] = Ivy_ObjRandomSim();
Vec_PtrForEachEntry( Ivy_Obj_t *, p->vPiVars, pObj, i )
if ( Ivy_InfoHasBit( p->pPatWords, pObj->Id - 1 ) ^ (p->pSat->model.ptr[Ivy_ObjSatNum(pObj)] == l_True) )
// if ( Ivy_InfoHasBit( p->pPatWords, pObj->Id - 1 ) ^ (p->pSat->model.ptr[Ivy_ObjSatNum(pObj)] == l_True) )
if ( Ivy_InfoHasBit( p->pPatWords, pObj->Id - 1 ) ^ sat_solver_var_value(p->pSat, Ivy_ObjSatNum(pObj)) )
Ivy_InfoXorBit( p->pPatWords, pObj->Id - 1 );
}

3
src/opt/res/resSat.c
View File

@ -279,7 +279,8 @@ int Res_SatSimulate( Res_Sim_t * p, int nPatsLimit, int fOnSet )
for ( i = 0; i < p->nTruePis; i++ )
{
Var = (int)(ABC_PTRUINT_T)Abc_NtkPi(p->pAig,i)->pCopy;
value = (int)(pSat->model.ptr[Var] == l_True);
// value = (int)(pSat->model.ptr[Var] == l_True);
value = sat_solver_var_value(pSat, Var);
if ( value )
Abc_InfoSetBit( (unsigned *)Vec_PtrEntry(vPats, i), k );
Lit = toLitCond( Var, value );

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

@ -938,7 +938,7 @@ sat_solver* sat_solver_new(void)
veci_new(&s->trail_lim);
veci_new(&s->tagged);
veci_new(&s->stack);
veci_new(&s->model);
// veci_new(&s->model);
veci_new(&s->act_vars);
veci_new(&s->temp_clause);
veci_new(&s->conf_final);
@ -1010,6 +1010,7 @@ void sat_solver_setnvars(sat_solver* s,int n)
s->orderpos = ABC_REALLOC(int, s->orderpos, s->cap);
s->reasons = ABC_REALLOC(int, s->reasons, s->cap);
s->trail = ABC_REALLOC(lit, s->trail, s->cap);
s->model = ABC_REALLOC(int, s->model, s->cap);
memset( s->wlists + 2*old_cap, 0, 2*(s->cap-old_cap)*sizeof(veci) );
}
@ -1054,7 +1055,7 @@ void sat_solver_delete(sat_solver* s)
veci_delete(&s->trail_lim);
veci_delete(&s->tagged);
veci_delete(&s->stack);
veci_delete(&s->model);
// veci_delete(&s->model);
veci_delete(&s->act_vars);
veci_delete(&s->temp_clause);
veci_delete(&s->conf_final);
@ -1075,6 +1076,7 @@ void sat_solver_delete(sat_solver* s)
ABC_FREE(s->orderpos );
ABC_FREE(s->reasons );
ABC_FREE(s->trail );
ABC_FREE(s->model );
}
sat_solver_store_free(s);
@ -1326,7 +1328,7 @@ static lbool sat_solver_search(sat_solver* s, ABC_INT64_T nof_conflicts, ABC_INT
s->stats.starts++;
// s->var_decay = (float)(1 / var_decay ); // move this to sat_solver_new()
// s->cla_decay = (float)(1 / clause_decay); // move this to sat_solver_new()
veci_resize(&s->model,0);
// veci_resize(&s->model,0);
veci_new(&learnt_clause);
// use activity factors in every even restart
@ -1408,9 +1410,8 @@ static lbool sat_solver_search(sat_solver* s, ABC_INT64_T nof_conflicts, ABC_INT
if (next == var_Undef){
// Model found:
int i;
veci_resize(&s->model, 0);
for (i = 0; i < s->size; i++)
veci_push( &s->model, var_value(s,i)==var1 ? l_True : l_False );
for (i = 0; i < s->size; i++)
s->model[i] = (var_value(s,i)==var1 ? l_True : l_False);
sat_solver_canceluntil(s,s->root_level);
veci_delete(&learnt_clause);

15
src/sat/bsat/satSolver.h
View File

@ -125,7 +125,8 @@ struct sat_solver_t
veci order; // Variable order. (heap) (contains: var)
veci trail_lim; // Separator indices for different decision levels in 'trail'. (contains: int)
veci model; // If problem is solved, this vector contains the model (contains: lbool).
// veci model; // If problem is solved, this vector contains the model (contains: lbool).
int * model; // If problem is solved, this vector contains the model (contains: lbool).
veci conf_final; // If problem is unsatisfiable (possibly under assumptions),
// this vector represent the final conflict clause expressed in the assumptions.
@ -164,15 +165,15 @@ struct sat_solver_t
veci temp_clause; // temporary storage for a CNF clause
};
static int sat_solver_var_value( sat_solver* s, int v )
static int sat_solver_var_value( sat_solver* s, int v )
{
assert( s->model.ptr != NULL && v < s->size );
return (int)(s->model.ptr[v] == l_True);
assert( v >= 0 && v < s->size );
return (int)(s->model[v] == l_True);
}
static int sat_solver_var_literal( sat_solver* s, int v )
static int sat_solver_var_literal( sat_solver* s, int v )
{
assert( s->model.ptr != NULL && v < s->size );
return toLitCond( v, s->model.ptr[v] != l_True );
assert( v >= 0 && v < s->size );
return toLitCond( v, s->model[v] != l_True );
}
static void sat_solver_act_var_clear(sat_solver* s)
{

8
src/sat/bsat/satSolver2.c
View File

@ -1087,7 +1087,6 @@ static lbool solver2_search(sat_solver2* s, ABC_INT64_T nof_conflicts)
s->stats.starts++;
// s->var_decay = (float)(1 / 0.95 );
// s->cla_decay = (float)(1 / 0.999);
veci_resize(&s->model,0);
veci_new(&learnt_clause);
for (;;){
@ -1158,9 +1157,8 @@ static lbool solver2_search(sat_solver2* s, ABC_INT64_T nof_conflicts)
if (next == var_Undef){
// Model found:
int i;
veci_resize(&s->model, 0);
for (i = 0; i < s->size; i++)
veci_push( &s->model, var_value(s,i)==var1 ? l_True : l_False );
s->model[i] = (var_value(s,i)==var1 ? l_True : l_False);
solver2_canceluntil(s,s->root_level);
veci_delete(&learnt_clause);
@ -1197,7 +1195,6 @@ sat_solver2* sat_solver2_new(void)
veci_new(&s->trail_lim);
veci_new(&s->tagged);
veci_new(&s->stack);
veci_new(&s->model);
veci_new(&s->temp_clause);
veci_new(&s->conf_final);
veci_new(&s->mark_levels);
@ -1276,6 +1273,7 @@ void sat_solver2_setnvars(sat_solver2* s,int n)
#else
s->activity = ABC_REALLOC(unsigned, s->activity, s->cap);
#endif
s->model = ABC_REALLOC(int, s->model, s->cap);
memset( s->wlists + 2*old_cap, 0, 2*(s->cap-old_cap)*sizeof(vecp) );
}
@ -1326,7 +1324,6 @@ void sat_solver2_delete(sat_solver2* s)
veci_delete(&s->trail_lim);
veci_delete(&s->tagged);
veci_delete(&s->stack);
veci_delete(&s->model);
veci_delete(&s->temp_clause);
veci_delete(&s->conf_final);
veci_delete(&s->mark_levels);
@ -1354,6 +1351,7 @@ void sat_solver2_delete(sat_solver2* s)
ABC_FREE(s->reasons );
ABC_FREE(s->units );
ABC_FREE(s->activity );
ABC_FREE(s->model );
}
ABC_FREE(s);
}

10
src/sat/bsat/satSolver2.h
View File

@ -132,13 +132,13 @@ struct sat_solver2_t
int* orderpos; // Index in variable order.
cla* reasons; // reason clauses
cla* units; // unit clauses
int* model; // If problem is solved, this vector contains the model (contains: lbool).
veci tagged; // (contains: var)
veci stack; // (contains: var)
veci order; // Variable order. (heap) (contains: var)
veci trail_lim; // Separator indices for different decision levels in 'trail'. (contains: int)
veci temp_clause; // temporary storage for a CNF clause
veci model; // If problem is solved, this vector contains the model (contains: lbool).
veci conf_final; // If problem is unsatisfiable (possibly under assumptions),
// this vector represent the final conflict clause expressed in the assumptions.
veci mark_levels; // temporary storage for labeled levels
@ -213,13 +213,13 @@ static inline int sat_solver2_nconflicts(sat_solver2* s)
static inline int sat_solver2_var_value( sat_solver2* s, int v )
{
assert( s->model.ptr != NULL && v < s->size );
return (int)(s->model.ptr[v] == l_True);
assert( v >= 0 && v < s->size );
return (int)(s->model[v] == l_True);
}
static inline int sat_solver2_var_literal( sat_solver2* s, int v )
{
assert( s->model.ptr != NULL && v < s->size );
return toLitCond( v, s->model.ptr[v] != l_True );
assert( v >= 0 && v < s->size );
return toLitCond( v, s->model[v] != l_True );
}
static inline void sat_solver2_act_var_clear(sat_solver2* s)
{

10
src/sat/bsat/satUtil.c
View File

@ -231,10 +231,7 @@ int * Sat_SolverGetModel( sat_solver * p, int * pVars, int nVars )
int i;
pModel = ABC_CALLOC( int, nVars+1 );
for ( i = 0; i < nVars; i++ )
{
assert( pVars[i] >= 0 && pVars[i] < p->size );
pModel[i] = (int)(p->model.ptr[pVars[i]] == l_True);
}
pModel[i] = sat_solver_var_value(p, pVars[i]);
return pModel;
}
@ -255,10 +252,7 @@ int * Sat_Solver2GetModel( sat_solver2 * p, int * pVars, int nVars )
int i;
pModel = ABC_CALLOC( int, nVars+1 );
for ( i = 0; i < nVars; i++ )
{
assert( pVars[i] >= 0 && pVars[i] < p->size );
pModel[i] = (int)(p->model.ptr[pVars[i]] == l_True);
}
pModel[i] = sat_solver2_var_value(p, pVars[i]);
return pModel;
}