From 8ed1992029a314cc62a02ed46a36e097248ee0b5 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Tue, 26 Jan 2021 11:29:40 -0800
Subject: [PATCH] char value

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/smt/theory_char.cpp | 12 ++++++------
 src/smt/theory_char.h   |  4 ++--
 src/smt/theory_seq.cpp  |  2 +-
 3 files changed, 9 insertions(+), 9 deletions(-)

diff --git a/src/smt/theory_char.cpp b/src/smt/theory_char.cpp
index 26335e892..0a1c4c547 100644
--- a/src/smt/theory_char.cpp
+++ b/src/smt/theory_char.cpp
@@ -224,8 +224,8 @@ namespace smt {
         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_value(v, c)) {
-                CTRACE("seq", seq.is_char(e), tout << mk_pp(e, m) << " root: " << get_enode(v)->is_root() << " is_value: " << get_value(v, c) << "\n";);
+            if (seq.is_char(e) && m_var2value[v] == UINT_MAX && get_char_value(v, c)) {
+                CTRACE("seq", seq.is_char(e), tout << mk_pp(e, m) << " root: " << get_enode(v)->is_root() << " is_value: " << get_char_value(v, c) << "\n";);
                 enode* r = get_enode(v)->get_root();
                 m_value2var.reserve(c + 1, null_theory_var);
                 theory_var u = m_value2var[c];
@@ -241,7 +241,7 @@ namespace smt {
                     u = n->get_th_var(get_id());
                     if (u == null_theory_var)
                         continue;
-                    if (get_value(u, d) && d != c) {
+                    if (get_char_value(u, d) && d != c) {
                         enforce_ackerman(u, v);
                         return false;
                     }
@@ -323,11 +323,11 @@ namespace smt {
         ++m_stats.m_num_ackerman;
     }
     
-    unsigned theory_char::get_value(theory_var v) {
+    unsigned theory_char::get_char_value(theory_var v) {
         return m_var2value[v];
     }
 
-    bool theory_char::get_value(theory_var v, unsigned& c) {
+    bool theory_char::get_char_value(theory_var v, unsigned& c) {
         if (!has_bits(v))
             return false;
         auto const & b = get_bits(v);
@@ -348,7 +348,7 @@ namespace smt {
     }
 
     model_value_proc * theory_char::mk_value(enode * n, model_generator & mg) {
-        unsigned ch = get_value(n->get_th_var(get_id()));
+        unsigned ch = get_char_value(n->get_th_var(get_id()));
         app* val = seq.str.mk_char(ch);
         m_factory->add_trail(val);
         return alloc(expr_wrapper_proc, val);
diff --git a/src/smt/theory_char.h b/src/smt/theory_char.h
index d26e18aec..6a829487a 100644
--- a/src/smt/theory_char.h
+++ b/src/smt/theory_char.h
@@ -56,7 +56,7 @@ namespace smt {
 
         void init_bits(theory_var v);
 
-        bool get_value(theory_var v, unsigned& c);
+        bool get_char_value(theory_var v, unsigned& c);
         
         void enforce_ackerman(theory_var v, theory_var w);
 
@@ -87,7 +87,7 @@ namespace smt {
         void assign_le(theory_var v1, theory_var v2, literal lit);
         void assign_lt(theory_var v1, theory_var v2, literal lit);
         void new_const_char(theory_var v, unsigned c);
-        unsigned get_value(theory_var v);
+        unsigned get_char_value(theory_var v);
 
         void internalize_le(literal lit, app* term);        
     };
diff --git a/src/smt/theory_seq.cpp b/src/smt/theory_seq.cpp
index 108777455..cce9a8bd3 100644
--- a/src/smt/theory_seq.cpp
+++ b/src/smt/theory_seq.cpp
@@ -1992,7 +1992,7 @@ model_value_proc * theory_seq::mk_value(enode * n, model_generator & mg) {
         return sv;
     }
     else if (m_char.enabled() && m_util.is_char(e)) {
-        unsigned ch = m_char.get_value(n->get_th_var(get_id()));
+        unsigned ch = m_char.get_char_value(n->get_th_var(get_id()));
         app* val = m_util.str.mk_char(ch);
         m_factory->add_trail(val);
         return alloc(expr_wrapper_proc, val);