New function to retrieve polarity value of a variable.

2 files changed, 6 insertions, 1 deletions

diff --git a/src/sat/satoko/solver.c b/src/sat/satoko/solver.c
index 6554f653..3e5fc8ee 100644
--- a/src/sat/satoko/solver.c
+++ b/src/sat/satoko/solver.c
@@ -195,7 +195,7 @@ static inline unsigned solver_decide(solver_t *s)
         if (solver_has_marks(s) && !var_mark(s, next_var))
             next_var = UNDEF;
     }
-    return var2lit(next_var, vec_char_at(s->polarity, next_var));
+    return var2lit(next_var, var_polarity(s, next_var));
 }
 
 static inline void solver_new_decision(solver_t *s, unsigned lit)
diff --git a/src/sat/satoko/solver.h b/src/sat/satoko/solver.h
index 68cc97dc..dcae8f6e 100644
--- a/src/sat/satoko/solver.h
+++ b/src/sat/satoko/solver.h
@@ -132,6 +132,11 @@ static inline char var_value(solver_t *s, unsigned var)
     return vec_char_at(s->assigns, var);
 }
 
+static inline char var_polarity(solver_t *s, unsigned var)
+{
+    return vec_char_at(s->polarity, var);
+}
+
 static inline unsigned var_dlevel(solver_t *s, unsigned var)
 {
     return vec_uint_at(s->levels, var);