From ac857aaf727da71274d744862969502ed151a783 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Wed, 23 Jul 2025 15:32:49 -0700
Subject: [PATCH] add score access and reset

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/smt/smt_context.h        |  8 ++++++++
 src/smt/smt_internalizer.cpp | 11 +++++++++++
 2 files changed, 19 insertions(+)

diff --git a/src/smt/smt_context.h b/src/smt/smt_context.h
index 3dbadc1cb..da6e92569 100644
--- a/src/smt/smt_context.h
+++ b/src/smt/smt_context.h
@@ -189,6 +189,7 @@ namespace smt {
         unsigned_vector             m_lit_occs;    //!< occurrence count of literals
         svector<bool_var_data>      m_bdata;       //!< mapping bool_var -> data
         svector<double>             m_activity;
+        svector<double[2]>          m_scores;
         clause_vector               m_aux_clauses;
         clause_vector               m_lemmas;
         vector<clause_vector>       m_clauses_to_reinit;
@@ -929,6 +930,13 @@ namespace smt {
         ast_pp_util m_lemma_visitor;
         void dump_lemma(unsigned n, literal const* lits);
         void dump_axiom(unsigned n, literal const* lits);
+        void add_scores(unsigned n, literal const* lits);
+        void reset_scores() {
+            for (auto& s : m_scores) s[0] = s[1] = 0.0;
+        }
+        double get_score(literal l) const {
+            return m_scores[l.var()][l.sign()];
+        }
     public:        
 
         void ensure_internalized(expr* e);
diff --git a/src/smt/smt_internalizer.cpp b/src/smt/smt_internalizer.cpp
index c15505ab0..faf7ea24d 100644
--- a/src/smt/smt_internalizer.cpp
+++ b/src/smt/smt_internalizer.cpp
@@ -928,6 +928,8 @@ namespace smt {
         set_bool_var(id, v);
         m_bdata.reserve(v+1);
         m_activity.reserve(v+1);
+        m_scores.reserve(v + 1);
+        m_scores[v][0] = m_scores[v][1] = 0.0;
         m_bool_var2expr.reserve(v+1);
         m_bool_var2expr[v] = n;
         literal l(v, false);
@@ -1416,6 +1418,7 @@ namespace smt {
             break;
         case CLS_LEARNED:
             dump_lemma(num_lits, lits);
+            add_scores(num_lits, lits);
             break;
         default:
             break;
@@ -1524,6 +1527,14 @@ namespace smt {
         }} 
     }
 
+    void context::add_scores(unsigned n, literal const* lits) {
+        for (unsigned i = 0; i < n; ++i) {
+            auto lit = lits[i];
+            unsigned v = lit.var();
+            m_scores[v][lit.sign()] += 1.0 / n;
+        }
+    }
+
     void context::dump_axiom(unsigned n, literal const* lits) {
         if (m_fparams.m_axioms2files) {
             literal_buffer tmp;