From 004139b320aaaaf9458d5a0c844583b2cd085966 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Sat, 2 Jul 2022 11:37:21 -0700
Subject: [PATCH] rewrites for characters

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/ast/rewriter/char_rewriter.cpp | 36 ++++++++++++++++++++++++++++++
 src/ast/rewriter/char_rewriter.h   |  6 +++++
 src/ast/seq_decl_plugin.cpp        |  7 +++++-
 3 files changed, 48 insertions(+), 1 deletion(-)

diff --git a/src/ast/rewriter/char_rewriter.cpp b/src/ast/rewriter/char_rewriter.cpp
index 14b86773a87..01f605816b9 100644
--- a/src/ast/rewriter/char_rewriter.cpp
+++ b/src/ast/rewriter/char_rewriter.cpp
@@ -37,21 +37,57 @@ br_status char_rewriter::mk_app_core(func_decl * f, unsigned num_args, expr * co
     case OP_CHAR_CONST:
         break;
     case OP_CHAR_LE:
+        st = mk_char_le(args[0], args[1], result);
         break;
     case OP_CHAR_TO_INT:
         st = mk_char_to_int(args[0], result);        
         break;
     case OP_CHAR_TO_BV:
+        st = mk_char_to_bv(args[0], result);
         break;
     case OP_CHAR_FROM_BV:
         st = mk_char_from_bv(args[0], result);
         break;
     case OP_CHAR_IS_DIGIT:
+        st = mk_char_is_digit(args[0], result);
         break;
     }
     return st;
 }
 
+br_status char_rewriter::mk_char_is_digit(expr* a, expr_ref& result) {
+    unsigned n;
+    if (!m_char->is_const_char(a, n))
+        return BR_FAILED;
+    result = m.mk_bool_val('0' <= n && n <= '9');
+    return BR_DONE;
+}
+
+br_status char_rewriter::mk_char_to_bv(expr* a, expr_ref& result) {
+    return BR_FAILED;
+}
+
+br_status char_rewriter::mk_char_le(expr* a, expr* b, expr_ref& result) {
+    unsigned na = 0, nb = 0;
+    if (m_char->is_const_char(a, na)) {
+        if (na == 0) {
+            result = m.mk_true();
+            return BR_DONE;
+        }
+    }
+    if (m_char->is_const_char(b, nb)) {
+        if (na != 0) {
+            result = m.mk_bool_val(na <= nb);
+            return BR_DONE;
+        }
+        if (nb == m_char->max_char()) {
+            result = m.mk_true();
+            return BR_DONE;
+        }
+    }
+    return BR_FAILED;
+}
+
 br_status char_rewriter::mk_char_from_bv(expr* e, expr_ref& result) {
     bv_util bv(m);
     rational n;
diff --git a/src/ast/rewriter/char_rewriter.h b/src/ast/rewriter/char_rewriter.h
index f67695bd80f..0ff8338496e 100644
--- a/src/ast/rewriter/char_rewriter.h
+++ b/src/ast/rewriter/char_rewriter.h
@@ -35,6 +35,12 @@ class char_rewriter {
 
     br_status mk_char_to_int(expr* e, expr_ref& result);
 
+    br_status mk_char_le(expr* a, expr* b, expr_ref& result);
+
+    br_status mk_char_is_digit(expr* a, expr_ref& result);
+
+    br_status mk_char_to_bv(expr* a, expr_ref& result);
+
 public:
 
     char_rewriter(ast_manager& m);
diff --git a/src/ast/seq_decl_plugin.cpp b/src/ast/seq_decl_plugin.cpp
index 95b9b8579f7..bb9df68a274 100644
--- a/src/ast/seq_decl_plugin.cpp
+++ b/src/ast/seq_decl_plugin.cpp
@@ -532,7 +532,12 @@ func_decl* seq_decl_plugin::mk_func_decl(decl_kind k, unsigned num_parameters, p
     case _OP_STRING_FROM_CHAR: {
         if (!(num_parameters == 1 && parameters[0].is_int())) 
             m.raise_exception("character literal expects integer parameter");
-        zstring zs(parameters[0].get_int());        
+        int i = parameters[0].get_int();
+        if (i < 0)
+            m.raise_exception("character literal expects a non-negative integer parameter");
+        if (i > (int)m_char_plugin->max_char())
+            m.raise_exception("character literal is out of bounds");
+        zstring zs(i);        
         parameter p(zs);
         return m.mk_const_decl(m_stringc_sym, m_string,func_decl_info(m_family_id, OP_STRING_CONST, 1, &p));
     }