fix #5674

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

src/api/api_ast.cpp

@@ -1232,6 +1232,7 @@ extern "C" {
 
         if (mk_c(c)->get_char_fid() == _d->get_family_id()) {
             switch (_d->get_decl_kind()) {
+            case OP_CHAR_CONST: return Z3_OP_CHAR_CONST;
             case OP_CHAR_LE: return Z3_OP_CHAR_LE;
             case OP_CHAR_TO_INT: return Z3_OP_CHAR_TO_INT;
             case OP_CHAR_TO_BV: return Z3_OP_CHAR_TO_BV;

src/api/python/z3/z3printer.py

@@ -770,6 +770,8 @@ class Formatter:
             return self.pp_set("Empty", a)
         elif k == Z3_OP_RE_FULL_SET:
             return self.pp_set("Full", a)
+        elif k == Z3_OP_CHAR_CONST:
+            return self.pp_char(a)
         return self.pp_name(a)
 
     def pp_int(self, a):
@@ -1060,6 +1062,10 @@ class Formatter:
     def pp_set(self, id, a):
         return seq1(id, [self.pp_sort(a.sort())])
 
+    def pp_char(self, a):
+        n = a.params()[0]
+        return to_format(str(n))
+
     def pp_pattern(self, a, d, xs):
         if a.num_args() == 1:
             return self.pp_expr(a.arg(0), d, xs)
@@ -1151,6 +1157,9 @@ class Formatter:
                 return self.pp_pbcmp(a, d, f, xs)
             elif k == Z3_OP_PB_EQ:
                 return self.pp_pbcmp(a, d, f, xs)
+            elif k == Z3_OP_SEQ_UNIT and z3.is_app(a.arg(0)) and a.arg(0).decl().kind() == Z3_OP_CHAR_CONST:
+                n = a.arg(0).params()[0]
+                return to_format(f"\"{chr(n)}\"")
             elif z3.is_pattern(a):
                 return self.pp_pattern(a, d, xs)
             elif self.is_infix(k):

src/api/z3_api.h

@@ -1222,6 +1222,7 @@ typedef enum {
     Z3_OP_RE_COMPLEMENT,
 
     // char
+    Z3_OP_CHAR_CONST,
     Z3_OP_CHAR_LE,
     Z3_OP_CHAR_TO_INT,
     Z3_OP_CHAR_TO_BV,

src/ast/ast.h

@@ -1050,6 +1050,12 @@ public:
     */
     virtual bool is_value(app * a) const { return false; }
 
+
+    /**
+       \brief return true if the expression can be used as a model value.
+     */
+    virtual bool is_model_value(app* a) const { return is_value(a); }
+
     /**
        \brief Return true if \c a is a unique plugin value.
        The following property should hold for unique theory values:

src/ast/seq_decl_plugin.cpp

@@ -705,6 +705,17 @@ bool seq_decl_plugin::is_value(app* e) const {
     }
 }
 
+bool seq_decl_plugin::is_model_value(app* e) const {
+    if (is_app_of(e, m_family_id, OP_SEQ_EMPTY)) 
+        return true;
+    if (is_app_of(e, m_family_id, OP_STRING_CONST)) 
+        return true;
+    if (is_app_of(e, m_family_id, OP_SEQ_UNIT) &&
+        m_manager->is_value(e->get_arg(0))) 
+        return true;
+    return false;
+}
+
 bool seq_decl_plugin::are_equal(app* a, app* b) const {
     if (a == b) return true;
     // handle concatenations

src/ast/seq_decl_plugin.h

@@ -179,6 +179,8 @@ public:
 
     bool is_value(app * e) const override;
 
+    bool is_model_value(app* e) const override;
+
     bool is_unique_value(app * e) const override;
 
     bool are_equal(app* a, app* b) const override;

src/smt/smt_model_generator.cpp

@@ -105,7 +105,7 @@ namespace smt {
                     else
                         proc = alloc(expr_wrapper_proc, m.mk_false());
                 }
-                else if (m.is_value(r->get_expr()))
+                else if (m.is_model_value(r->get_expr()))
                     proc = alloc(expr_wrapper_proc, r->get_expr());                    
                 else {
                     family_id fid = s->get_family_id();