From f16dcef7e2f8a722d59ce6288a9b7e7515410da6 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Fri, 3 Mar 2017 18:09:41 -0800
Subject: [PATCH] updates

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

diff --git a/src/sat/sat_local_search.cpp b/src/sat/sat_local_search.cpp
index 21555cfcb..557a5a9a2 100644
--- a/src/sat/sat_local_search.cpp
+++ b/src/sat/sat_local_search.cpp
@@ -223,8 +223,9 @@ namespace sat {
             m_vars.reserve(c[i].var() + 1);
             literal t(~c[i]);
             m_vars[t.var()].m_watch[is_pos(t)].push_back(id);
-            m_constraints.back().m_literals.push_back(t);
+            m_constraints.back().push(t);
         }
+        m_constraints.back().seal();
         if (sz == 1 && k == 0) {
             m_vars[c[0].var()].m_bias = c[0].sign() ? 0 : 100;
         }
@@ -447,50 +448,55 @@ namespace sat {
         SASSERT(c.m_k < constraint_value(c));
         if (m_rand() % 100 < 98) {
             // take this branch with 98% probability.
-            // display(std::cout, c);
             unsigned best_bsb = 0;
             // find the first one, to fast break the rest    
             unsigned i = 0;
+            literal const* lits = c.m_literals.c_ptr();
+            literal l;
             while (true) {
-                v = c[i].var();
-                if (is_true(c[i])) {
+                l = *lits;
+                if (is_true(l)) {
+                    v = l.var();
                     bool tt = cur_solution(v);
                     int_vector const& falsep = m_vars[v].m_watch[!tt];
-                    for (unsigned j = 0; j < falsep.size(); ++j) {
+                    unsigned sz = falsep.size();
+                    for (unsigned j = 0; j < sz; ++j) {
                         unsigned ci = falsep[j];
                         if (constraint_slack(ci) < 0)
                             ++best_bsb;
                         else if (constraint_slack(ci) == 0)
-                            // >= unsat_stack_fill_pointer is enough
-                            best_bsb += m_constraints.size();
+                            best_bsb += m_unsat_stack.size();
                     }
                     break;
                 }
-                ++i;
+                ++lits;
             }
+            ++lits;
             m_good_vars.push_back(v);
-            for (++i; i < c.size(); ++i) {
-                v = c[i].var();
-                if (is_true(c[i])) {
+            for (; (l = *lits) != null_literal; ++lits) {
+                if (is_true(l)) {
+                    v = l.var();                    
                     bool found = false;
                     unsigned bsb = 0;
                     bool tt = cur_solution(v);
                     int_vector const& falsep = m_vars[v].m_watch[!tt];
-                    for (unsigned j = 0; j < falsep.size() && !found; ++j) {
+                    unsigned sz = falsep.size();
+                    for (unsigned j = 0; j < sz; ++j) {
                         unsigned ci = falsep[j];
                         if (constraint_slack(ci) < 0) {
                             if (bsb == best_bsb) {
                                 found = true;
+                                break;
                             }
                             else {
                                 ++bsb;
                             }
                         }
                         else if (constraint_slack(ci) == 0) {
-                            // >= unsat_stack_fill_pointer is enough
-                            bsb += m_constraints.size();
+                            bsb += m_unsat_stack.size();
                             if (bsb > best_bsb) {
                                 found = true;
+                                break;
                             }
                         }
                     }
diff --git a/src/sat/sat_local_search.h b/src/sat/sat_local_search.h
index f41dfed03..cbd0d9d30 100644
--- a/src/sat/sat_local_search.h
+++ b/src/sat/sat_local_search.h
@@ -94,9 +94,12 @@ namespace sat {
         struct constraint {
             unsigned        m_k;
             int             m_slack;
+            unsigned        m_size;
             literal_vector  m_literals;
-            constraint(unsigned k) : m_k(k), m_slack(0) {}
-            unsigned size() const { return m_literals.size(); }
+            constraint(unsigned k) : m_k(k), m_slack(0), m_size(0) {}
+            void push(literal l) { m_literals.push_back(l); ++m_size; }
+            void seal() { m_literals.push_back(null_literal); }
+            unsigned size() const { return m_size; }
             literal const& operator[](unsigned idx) const { return m_literals[idx]; }
         };