From f5cdff407fb9a5aefb5d207efef896b2c60a1c16 Mon Sep 17 00:00:00 2001
From: Copilot <198982749+Copilot@users.noreply.github.com>
Date: Fri, 23 Jan 2026 13:32:18 -0800
Subject: [PATCH] Refactor theory_char::get_char_value to use std::optional
 (#8302)

* Initial plan

* Refactor theory_char::get_char_value to use std::optional

- Updated function signature to return std::optional<unsigned>
- Added const qualifier to function
- Updated both call sites to use modern C++17 patterns
- Used std::as_const to disambiguate overload resolution

Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>

---------

Co-authored-by: copilot-swe-agent[bot] <198982749+Copilot@users.noreply.github.com>
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
---
 src/smt/theory_char.cpp | 22 +++++++++++-----------
 src/smt/theory_char.h   |  3 ++-
 2 files changed, 13 insertions(+), 12 deletions(-)

diff --git a/src/smt/theory_char.cpp b/src/smt/theory_char.cpp
index a5a52b4b2..bcefa12e6 100644
--- a/src/smt/theory_char.cpp
+++ b/src/smt/theory_char.cpp
@@ -314,11 +314,11 @@ namespace smt {
 
         // extract the initial set of constants.
         uint_set values;
-        unsigned c = 0, d = 0;
         for (unsigned v = get_num_vars(); v-- > 0; ) {
             expr* e = get_expr(v);
-            if (seq.is_char(e) && m_var2value[v] == UINT_MAX && get_char_value(v, c)) {
-                CTRACE(seq_verbose, seq.is_char(e), tout << mk_pp(e, m) << " root: " << get_enode(v)->is_root() << " is_value: " << get_char_value(v, c) << "\n";);
+            if (auto c_opt = std::as_const(*this).get_char_value(v); seq.is_char(e) && m_var2value[v] == UINT_MAX && c_opt) {
+                unsigned c = *c_opt;
+                CTRACE(seq_verbose, seq.is_char(e), tout << mk_pp(e, m) << " root: " << get_enode(v)->is_root() << " is_value: " << c << "\n";);
                 enode* r = get_enode(v)->get_root();
                 m_value2var.reserve(c + 1, null_theory_var);
                 theory_var u = m_value2var[c];
@@ -334,7 +334,7 @@ namespace smt {
                     u = n->get_th_var(get_id());
                     if (u == null_theory_var)
                         continue;
-                    if (get_char_value(u, d) && d != c) {
+                    if (auto d_opt = std::as_const(*this).get_char_value(u); d_opt && *d_opt != c) {
                         enforce_ackerman(u, v);
                         return false;
                     }
@@ -346,11 +346,11 @@ namespace smt {
         }
         
         // assign values to other unassigned nodes
-        c = 'A';
+        unsigned c = 'A';
         for (unsigned v = get_num_vars(); v-- > 0; ) {
             expr* e = get_expr(v);
             if (seq.is_char(e) && m_var2value[v] == UINT_MAX) {
-                d = c;
+                unsigned d = c;
                 while (values.contains(c)) {
                     c = (c + 1) % seq.max_char();
                     if (d == c) {
@@ -420,18 +420,18 @@ namespace smt {
         return m_var2value[v];
     }
 
-    bool theory_char::get_char_value(theory_var v, unsigned& c) {
+    std::optional<unsigned> theory_char::get_char_value(theory_var v) const {
         if (!has_bits(v))
-            return false;
-        auto const & b = get_bits(v);
-        c = 0;
+            return std::nullopt;
+        auto const & b = m_bits[v];
+        unsigned c = 0;
         unsigned p = 1;
         for (literal lit : b) {
             if (ctx.get_assignment(lit) == l_true)
                 c += p;
             p *= 2;
         }
-        return true;
+        return c;
     }
 
     // a stand-alone theory.
diff --git a/src/smt/theory_char.h b/src/smt/theory_char.h
index a4078a74e..b94de7c2e 100644
--- a/src/smt/theory_char.h
+++ b/src/smt/theory_char.h
@@ -20,6 +20,7 @@ Author:
 #include "ast/rewriter/bit_blaster/bit_blaster.h"
 #include "model/char_factory.h"
 #include "smt/smt_theory.h"
+#include <optional>
 
 namespace smt {
 
@@ -49,7 +50,7 @@ namespace smt {
         expr_ref_vector const& get_ebits(theory_var v);
         bool has_bits(theory_var v) const;
         void init_bits(theory_var v);
-        bool get_char_value(theory_var v, unsigned& c);        
+        std::optional<unsigned> get_char_value(theory_var v) const;        
         void enforce_ackerman(theory_var v, theory_var w);
         void enforce_value_bound(theory_var v);
         void enforce_bits();