rewrites for characters

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
Z3Prover · Jul 2, 2022 · 004139b · 004139b
1 parent f20db3e
commit 004139b
Show file tree

Hide file tree

Showing 3 changed files with 48 additions and 1 deletion.
diff --git 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
@@ -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
@@ -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));
     }