annotate arith_sls

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:

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,13 +308,20 @@ 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];
         for (auto const& [coeff, lit] : vi.m_literals) {
             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()) {

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()) {