summaryrefslogtreecommitdiffstats
path: root/src/sat
diff options
context:
space:
mode:
Diffstat (limited to 'src/sat')
-rw-r--r--src/sat/bsat/satSolver.c13
-rw-r--r--src/sat/bsat/satSolver.h15
-rw-r--r--src/sat/bsat/satSolver2.c8
-rw-r--r--src/sat/bsat/satSolver2.h10
-rw-r--r--src/sat/bsat/satUtil.c10
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;
}
generated by cgit v1.2.3 (git 2.25.1) at 2024-07-04 20:33:01 +0000