From 3f0cb6318b14e286cd9054a0f771183d15ef3db6 Mon Sep 17 00:00:00 2001
From: Bruno Schmitt <bruno@oschmitt.com>
Date: Sat, 18 Feb 2017 17:08:54 -0800
Subject: New function to retrieve polarity value of a variable.

---
 src/sat/satoko/solver.c | 2 +-
 src/sat/satoko/solver.h | 5 +++++
 2 files changed, 6 insertions(+), 1 deletion(-)

(limited to 'src')

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);
-- 
cgit v1.2.3