From ce615ee116aefdd08e12c5dc7e63ba7c69b2315e Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Thu, 23 Jan 2025 10:51:12 -0800
Subject: [PATCH] avoid repeated clauses during scoring function

---
 src/ast/sls/sls_arith_clausal.cpp | 11 +++++++++--
 src/ast/sls/sls_arith_clausal.h   |  4 ++++
 2 files changed, 13 insertions(+), 2 deletions(-)

diff --git a/src/ast/sls/sls_arith_clausal.cpp b/src/ast/sls/sls_arith_clausal.cpp
index 877b3f71b..1337baa34 100644
--- a/src/ast/sls/sls_arith_clausal.cpp
+++ b/src/ast/sls/sls_arith_clausal.cpp
@@ -222,7 +222,7 @@ namespace sls {
         for (auto const& u : a.m_updates)
             lookahead(u.m_var, u.m_delta);
 
-//        verbose_stream() << a.m_updates.size() << " " << m_num_lookaheads << " lookaheads\n";
+        // verbose_stream() << a.m_updates.size() << " " << m_num_lookaheads << " lookaheads\n";
         ctx.rlimit().inc(1 + m_num_lookaheads);
         critical_move(m_best_var, m_best_delta, mt);        
         return m_best_var;
@@ -300,9 +300,16 @@ namespace sls {
         if (!a.update_num(v, delta))
             return -1;
         double score = 0;
+        m_tmp_nat_set.reset();
+        m_tmp_nat_set.assure_domain(ctx.clauses().size() + 1);
         for (auto bv : vi.m_bool_vars_of) {
             for (auto lit : { sat::literal(bv, false), sat::literal(bv, true) }) {
-                for (auto ci : ctx.get_use_list(lit)) {
+                for (auto ci : ctx.get_use_list(lit)) {                    
+                    if (m_tmp_nat_set.contains(ci)) {
+                        continue;
+                    }
+                    m_tmp_nat_set.insert(ci);
+
                     auto const& c = ctx.get_clause(ci);
                     unsigned num_true = 0;
                     for (auto lit : c) {
diff --git a/src/ast/sls/sls_arith_clausal.h b/src/ast/sls/sls_arith_clausal.h
index b0c2b3015..78897ba27 100644
--- a/src/ast/sls/sls_arith_clausal.h
+++ b/src/ast/sls/sls_arith_clausal.h
@@ -19,10 +19,12 @@ Author:
 
 #include "util/checked_int64.h"
 #include "util/optional.h"
+#include "util/nat_set.h"
 #include "ast/ast_trail.h"
 #include "ast/arith_decl_plugin.h"
 #include "ast/sls/sls_context.h"
 
+
 namespace sls {
     
     template<typename num_t>
@@ -78,6 +80,8 @@ namespace sls {
         unsigned m_best_last_step = 0;
         unsigned m_num_lookaheads = 0;
 
+        nat_set  m_tmp_nat_set;
+
         // avoid checking the same updates twice
         var_t m_last_var = UINT_MAX;
         num_t m_last_delta;