From 10ad89490a6596dc51e27b6d7ebd0f2f0c606ed8 Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Fri, 6 Jan 2012 11:34:06 +0700 Subject: Bug fix related to not properly resizing SAT solver's model array. --- src/aig/fra/fraClaus.c | 3 +- src/aig/fra/fraSim.c | 3 +- src/aig/gia/giaAbsVta.c | 112 ---------------------------------------------- src/aig/int/intContain.c | 7 ++- src/aig/ivy/ivyFraig.c | 12 +++-- src/opt/res/resSat.c | 3 +- src/sat/bsat/satSolver.c | 13 +++--- src/sat/bsat/satSolver.h | 15 ++++--- src/sat/bsat/satSolver2.c | 8 ++-- src/sat/bsat/satSolver2.h | 10 ++--- src/sat/bsat/satUtil.c | 10 +---- 11 files changed, 45 insertions(+), 151 deletions(-) diff --git a/src/aig/fra/fraClaus.c b/src/aig/fra/fraClaus.c index 90659333..9548c166 100644 --- a/src/aig/fra/fraClaus.c +++ b/src/aig/fra/fraClaus.c @@ -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 ); diff --git a/src/aig/fra/fraSim.c b/src/aig/fra/fraSim.c index 37620a16..8f912915 100644 --- a/src/aig/fra/fraSim.c +++ b/src/aig/fra/fraSim.c @@ -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 ) diff --git a/src/aig/gia/giaAbsVta.c b/src/aig/gia/giaAbsVta.c index 48e09ae9..7cc00556 100644 --- a/src/aig/gia/giaAbsVta.c +++ b/src/aig/gia/giaAbsVta.c @@ -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************************************************************* diff --git a/src/aig/int/intContain.c b/src/aig/int/intContain.c index d4af0ae8..77b057a7 100644 --- a/src/aig/int/intContain.c +++ b/src/aig/int/intContain.c @@ -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 ); diff --git a/src/aig/ivy/ivyFraig.c b/src/aig/ivy/ivyFraig.c index f7c0743b..7cf97132 100644 --- a/src/aig/ivy/ivyFraig.c +++ b/src/aig/ivy/ivyFraig.c @@ -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 ); } diff --git a/src/opt/res/resSat.c b/src/opt/res/resSat.c index a17f92fa..17f3d661 100644 --- a/src/opt/res/resSat.c +++ b/src/opt/res/resSat.c @@ -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 ); diff --git a/src/sat/bsat/satSolver.c b/src/sat/bsat/satSolver.c index 5a05e3b0..a4bd29cd 100644 --- a/src/sat/bsat/satSolver.c +++ b/src/sat/bsat/satSolver.c @@ -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); diff --git a/src/sat/bsat/satSolver.h b/src/sat/bsat/satSolver.h index ce597271..1437f5c1 100644 --- a/src/sat/bsat/satSolver.h +++ b/src/sat/bsat/satSolver.h @@ -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) { diff --git a/src/sat/bsat/satSolver2.c b/src/sat/bsat/satSolver2.c index a4166fef..0da59fda 100644 --- a/src/sat/bsat/satSolver2.c +++ b/src/sat/bsat/satSolver2.c @@ -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); } diff --git a/src/sat/bsat/satSolver2.h b/src/sat/bsat/satSolver2.h index f3d70deb..4b26f55f 100644 --- a/src/sat/bsat/satSolver2.h +++ b/src/sat/bsat/satSolver2.h @@ -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) { diff --git a/src/sat/bsat/satUtil.c b/src/sat/bsat/satUtil.c index 5e809172..70d09638 100644 --- a/src/sat/bsat/satUtil.c +++ b/src/sat/bsat/satUtil.c @@ -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; } -- cgit v1.2.3