From 7956cf120147b4b8cdfb74851196d1026c8c57ca Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Sun, 12 Feb 2023 20:55:44 -0800
Subject: [PATCH] annotate arith_sls

---
 src/sat/sat_ddfw.h               |  1 +
 src/sat/smt/arith_sls.cpp        | 13 +++++++++++++
 src/sat/smt/euf_local_search.cpp |  7 ++-----
 3 files changed, 16 insertions(+), 5 deletions(-)

diff --git a/src/sat/sat_ddfw.h b/src/sat/sat_ddfw.h
index 9971033e3f6..ee1c73b6e96 100644
--- a/src/sat/sat_ddfw.h
+++ b/src/sat/sat_ddfw.h
@@ -52,6 +52,7 @@ namespace sat {
                 p(p), i(lit.index()) {}
             unsigned const* begin() { return p.m_flat_use_list.data() + p.m_use_list_index[i]; }
             unsigned const* end() { return p.m_flat_use_list.data() + p.m_use_list_index[i + 1]; }
+            unsigned size() const { return p.m_use_list_index[i + 1] - p.m_use_list_index[i]; }
         };
 
     protected:
diff --git a/src/sat/smt/arith_sls.cpp b/src/sat/smt/arith_sls.cpp
index 7afabe2474e..809295cca34 100644
--- a/src/sat/smt/arith_sls.cpp
+++ b/src/sat/smt/arith_sls.cpp
@@ -90,6 +90,7 @@ namespace arith {
                 rational new_value_(new_value, rational::i64());
                 lp::impq val(new_value_, rational::zero());
                 s.lp().set_value_for_nbasic_column(vj.index(), val);
+                // TODO - figure out why this leads to unsound (unsat).
             }
         }
     }
@@ -147,6 +148,11 @@ namespace arith {
         }
     }
 
+    //
+    // dtt is high overhead. It walks ineq.m_args
+    // m_vars[w].m_value can be computed outside and shared among calls
+    // different data-structures for storing coefficients
+    // 
     int64_t sls::dtt(ineq const& ineq, var_t v, int64_t new_value) const {
         auto new_args_value = ineq.m_args_value;
         for (auto const& [coeff, w] : ineq.m_args) {
@@ -302,6 +308,12 @@ namespace arith {
         return score;
     }
 
+    //
+    // cm_score is costly. It involves several cache misses.
+    // Note that
+    // - m_bool_search->get_use_list(lit).size() is "often" 1 or 2
+    // - dtt_old can be saved
+    //
     int sls::cm_score(var_t v, int64_t new_value) {
         int score = 0;
         auto& vi = m_vars[v];
@@ -309,6 +321,7 @@ namespace arith {
             auto const& ineq = *atom(lit);            
             int64_t dtt_old = dtt(ineq);
             int64_t dtt_new = dtt(ineq, v, new_value);
+            
             for (auto cl : m_bool_search->get_use_list(lit)) {
                 auto const& clause = get_clause_info(cl);
                 if (!clause.is_true()) {
diff --git a/src/sat/smt/euf_local_search.cpp b/src/sat/smt/euf_local_search.cpp
index fab3b7815b4..5357c083723 100644
--- a/src/sat/smt/euf_local_search.cpp
+++ b/src/sat/smt/euf_local_search.cpp
@@ -81,11 +81,8 @@ namespace euf {
                 return;
             }
             euf::enode* n = m_egraph.find(m_bool_var2expr.get(l.var(), nullptr));
-            for (auto const& thv : enode_th_vars(n)) {
-                auto* th = m_id2solver.get(thv.get_id(), nullptr);
-                if (th)
-                    th->set_bounds(n);
-            }
+            for (auto* s : m_solvers)
+                s->set_bounds(n);
         };
 
         for (auto cl : bool_search.unsat_set()) {