diff options
Diffstat (limited to 'src/sat/bsat')
-rw-r--r-- | src/sat/bsat/satSolver.c | 13 | ||||
-rw-r--r-- | src/sat/bsat/satSolver.h | 15 | ||||
-rw-r--r-- | src/sat/bsat/satSolver2.c | 8 | ||||
-rw-r--r-- | src/sat/bsat/satSolver2.h | 10 | ||||
-rw-r--r-- | src/sat/bsat/satUtil.c | 10 |
5 files changed, 25 insertions, 31 deletions
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; } |