diff options
| author | Alan Mishchenko <alanmi@berkeley.edu> | 2007-11-30 08:01:00 -0800 |
|---|---|---|
| committer | Alan Mishchenko <alanmi@berkeley.edu> | 2007-11-30 08:01:00 -0800 |
| commit | 369f008e69a4f201cbc7c890a08221086bee4698 (patch) | |
| tree | 6dbc56239d2c6cf916c660327525b19773a9907c /src/sat | |
| parent | 765a21240891735a844dd64d1d73789ae6e55bc6 (diff) | |
| download | abc-369f008e69a4f201cbc7c890a08221086bee4698.tar.gz abc-369f008e69a4f201cbc7c890a08221086bee4698.tar.bz2 abc-369f008e69a4f201cbc7c890a08221086bee4698.zip | |
Version abc71130
Diffstat (limited to 'src/sat')
| -rw-r--r-- | src/sat/bsat/satSolver.h | 18 |
1 files changed, 18 insertions, 0 deletions
diff --git a/src/sat/bsat/satSolver.h b/src/sat/bsat/satSolver.h index 542b9895..ca2954d2 100644 --- a/src/sat/bsat/satSolver.h +++ b/src/sat/bsat/satSolver.h @@ -188,4 +188,22 @@ struct sat_solver_t int nRoots; }; +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); +} +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 ); +} +static void sat_solver_act_var_clear(sat_solver* s) +{ + int i; + for (i = 0; i < s->size; i++) + s->activity[i] = 0.0; + s->var_inc = 1.0; +} + #endif |