From cea52f493a21b289c9dc479589f03f571489a5ab Mon Sep 17 00:00:00 2001
From: Ilana Shapiro <ishapiro00@gmail.com>
Date: Wed, 29 Oct 2025 16:06:26 -0700
Subject: [PATCH] adding the learned clauses from the internalizer

---
 src/smt/smt_context.cpp      |  3 ++-
 src/smt/smt_context.h        |  3 +++
 src/smt/smt_internalizer.cpp | 15 +++++++++++++++
 3 files changed, 20 insertions(+), 1 deletion(-)

diff --git a/src/smt/smt_context.cpp b/src/smt/smt_context.cpp
index c0a2f3a4d..46b630231 100644
--- a/src/smt/smt_context.cpp
+++ b/src/smt/smt_context.cpp
@@ -82,7 +82,8 @@ namespace smt {
         m_mk_bool_var_trail(*this),
         m_mk_enode_trail(*this),
         m_mk_lambda_trail(*this),
-        m_lemma_visitor(m) {
+        m_lemma_visitor(m),
+        m_recorded_clauses(m) {
 
         SASSERT(m_scope_lvl == 0);
         SASSERT(m_base_lvl == 0);
diff --git a/src/smt/smt_context.h b/src/smt/smt_context.h
index 7d68dc808..328e7dc25 100644
--- a/src/smt/smt_context.h
+++ b/src/smt/smt_context.h
@@ -137,6 +137,7 @@ namespace smt {
         scoped_ptr<base_dependent_expr_state> m_fmls;
 
         svector<double> m_lit_scores[2];
+        expr_ref_vector m_recorded_clauses;
 
 
         // -----------------------------------
@@ -1301,6 +1302,8 @@ namespace smt {
 
         void add_scores(unsigned n, literal const *lits);
 
+        void record_clause(clause const* cls);
+
 
         // -----------------------------------
         //
diff --git a/src/smt/smt_internalizer.cpp b/src/smt/smt_internalizer.cpp
index 7f0fe1e9e..90b49dcfa 100644
--- a/src/smt/smt_internalizer.cpp
+++ b/src/smt/smt_internalizer.cpp
@@ -936,6 +936,7 @@ namespace smt {
         m_lit_scores[0].reserve(v + 1);
         m_lit_scores[1].reserve(v + 1);
         m_lit_scores[0][v] = m_lit_scores[1][v] = 0.0;
+        m_recorded_clauses.reserve(v + 1);
 
         literal l(v, false);
         literal not_l(v, true);
@@ -965,6 +966,19 @@ namespace smt {
         return v;
     }
 
+    // following the pattern of solver::persist_clause in src/sat/smt/user_solver.cpp
+    void context::record_clause(clause const* cls) {
+        expr_ref_vector clause(m);
+        for (unsigned i = 0; i < cls->get_num_literals(); ++i) {
+            literal lit = cls->get_literal(i);
+            clause.push_back(literal2expr(~lit));
+        }
+        if (!clause.empty() && m.is_false(clause.back()))
+            clause.pop_back();
+        expr_ref disj(m.mk_or(clause.size(), clause.data()), m);
+        m_recorded_clauses.push_back(disj);
+    }
+
     void context::add_scores(unsigned n, literal const *lits) {
         for (unsigned i = 0; i < n; ++i) {
             auto lit = lits[i];
@@ -1492,6 +1506,7 @@ namespace smt {
                 if (k == CLS_LEARNED) {
                     int w2_idx  = select_learned_watch_lit(cls);
                     cls->swap_lits(1, w2_idx);
+                    record_clause(cls);
                 }
                 else {
                     SASSERT(k == CLS_TH_LEMMA);