From 475101e932b9f055421417186c6a0156ea361b42 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Mon, 27 Feb 2017 20:49:37 -0800
Subject: [PATCH] updates

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/sat/sat_local_search.cpp | 22 +++++++++++-----------
 src/sat/sat_local_search.h   |  8 +++++---
 2 files changed, 16 insertions(+), 14 deletions(-)

diff --git a/src/sat/sat_local_search.cpp b/src/sat/sat_local_search.cpp
index f204cdec2..46657f2f4 100644
--- a/src/sat/sat_local_search.cpp
+++ b/src/sat/sat_local_search.cpp
@@ -74,7 +74,7 @@ namespace sat {
             constraint & cn = m_constraints[c];
             for (unsigned i = 0; i < cn.size(); ++i) {
                 bool_var v = cn[i].var();
-                if (cur_solution[v] == is_pos(cn[i])) 
+                if (is_true(cn[i]))
                     --cn.m_slack;
             }
             // constraint_slack[c] = constraint_k[c] - true_terms_count[c];
@@ -340,9 +340,9 @@ namespace sat {
         int org_flipvar_score = score(flipvar);
         int org_flipvar_slack_score = slack_score(flipvar);
 
-        bool is_true = cur_solution[flipvar];
-        int_vector& truep = m_vars[flipvar].m_watch[is_true];
-        int_vector& falsep = m_vars[flipvar].m_watch[!is_true];
+        bool flip_is_true = cur_solution[flipvar];
+        int_vector& truep = m_vars[flipvar].m_watch[flip_is_true];
+        int_vector& falsep = m_vars[flipvar].m_watch[!flip_is_true];
 
         // update related clauses and neighbor vars
         for (unsigned i = 0; i < truep.size(); ++i) {
@@ -354,7 +354,7 @@ namespace sat {
                 for (unsigned j = 0; j < c.size(); ++j) {
                     v = c[j].var();
                     // flipping the slack increasing var will no long sat this constraint
-                    if (cur_solution[v] == is_pos(c[j])) {
+                    if (is_true(c[j])) {
                         //score[v] -= constraint_weight[c];
                         dec_score(v);
                     }
@@ -367,7 +367,7 @@ namespace sat {
                     //score[v] += constraint_weight[c];
                     inc_score(v);
                     // slack increasing var
-                    if (cur_solution[v] == is_pos(c[j]))
+                    if (is_true(c[j]))
                         inc_slack_score(v);
                 }
                 unsat(truep[i]);
@@ -376,7 +376,7 @@ namespace sat {
                 for (unsigned j = 0; j < c.size(); ++j) {
                     v = c[j].var();
                     // flip the slack decreasing var will falsify this constraint
-                    if (cur_solution[v] != is_pos(c[j])) {
+                    if (is_false(c[j])) {
                         //score[v] -= constraint_weight[c];
                         dec_score(v);
                         dec_slack_score(v);
@@ -396,7 +396,7 @@ namespace sat {
                 for (unsigned j = 0; j < c.size(); ++j) {
                     v = c[j].var();
                     // flip the slack decreasing var will no long falsify this constraint
-                    if (cur_solution[v] != is_pos(c[j])) {
+                    if (is_false(c[j])) {
                         //score[v] += constraint_weight[c];
                         inc_score(v);
                         inc_slack_score(v);
@@ -410,7 +410,7 @@ namespace sat {
                     //score[v] -= constraint_weight[c];
                     dec_score(v);
                     // slack increasing var no longer sat this var
-                    if (cur_solution[v] == is_pos(c[j]))
+                    if (is_true(c[j]))
                         dec_slack_score(v);
                 }
                 sat(falsep[i]);
@@ -419,7 +419,7 @@ namespace sat {
                 for (unsigned j = 0; j < c.size(); ++j) {
                     v = c[j].var();
                     // flip the slack increasing var will satisfy this constraint
-                    if (cur_solution[v] == is_pos(c[j])) {
+                    if (is_true(c[j])) {
                         //score[v] += constraint_weight[c];
                         inc_score(v);
                     }
@@ -526,7 +526,7 @@ namespace sat {
         unsigned c_size = c.size();
         for (unsigned i = 0; i < c_size; ++i) {
             v = c[i].var();
-            if (cur_solution[v] == is_pos(c[i]) && time_stamp(v) < time_stamp(best_var))
+            if (is_true(c[i]) && time_stamp(v) < time_stamp(best_var))
                 best_var = v;
         }
         return best_var;
diff --git a/src/sat/sat_local_search.h b/src/sat/sat_local_search.h
index 7e366c83a..30ee3ce38 100644
--- a/src/sat/sat_local_search.h
+++ b/src/sat/sat_local_search.h
@@ -113,9 +113,9 @@ namespace sat {
         /* TBD: other scores */
         
         struct constraint {
-            unsigned       m_k;
-            int            m_slack;
-            svector<literal>  m_literals;
+            unsigned        m_k;
+            int             m_slack;
+            literal_vector  m_literals;
             constraint(unsigned k) : m_k(k), m_slack(0) {}
             unsigned size() const { return m_literals.size(); }
             literal const& operator[](unsigned idx) const { return m_literals[idx]; }
@@ -127,6 +127,8 @@ namespace sat {
         // vector<svector<term> > constraint_term;  // constraint_term[i][j] means the j'th term of constraint i
 
         inline bool is_pos(literal t) const { return !t.sign(); }
+        inline bool is_true(literal l) const { return cur_solution[l.var()] != l.sign(); }
+        inline bool is_false(literal l) const { return cur_solution[l.var()] == l.sign(); }
 
         // parameters of the instance
         unsigned num_constraints() const { return m_constraints.size(); } // constraint index from 1 to num_constraint