From dfe2b27f9aa6d72583014fa301bd79d223fb254f Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Wed, 12 Jan 2022 13:28:15 -0800
Subject: [PATCH] #5773

---
 src/api/api_ast.cpp     |  3 +++
 src/api/api_seq.cpp     |  2 ++
 src/api/python/z3/z3.py | 12 ++++++++++++
 src/api/z3_api.h        | 17 +++++++++++++++++
 4 files changed, 34 insertions(+)

diff --git a/src/api/api_ast.cpp b/src/api/api_ast.cpp
index d11ce313e..87e218d99 100644
--- a/src/api/api_ast.cpp
+++ b/src/api/api_ast.cpp
@@ -1213,6 +1213,9 @@ extern "C" {
 
             case OP_STRING_STOI: return Z3_OP_STR_TO_INT;
             case OP_STRING_ITOS: return Z3_OP_INT_TO_STR;
+            case OP_STRING_TO_CODE: return Z3_OP_STR_TO_CODE;
+            case OP_STRING_FROM_CODE: return Z3_OP_STR_FROM_CODE;
+
             case OP_STRING_UBVTOS: return Z3_OP_UBV_TO_STR;
             case OP_STRING_SBVTOS: return Z3_OP_SBV_TO_STR;
             case OP_STRING_LT: return Z3_OP_STRING_LT;
diff --git a/src/api/api_seq.cpp b/src/api/api_seq.cpp
index a79a63b4d..a7c42df4f 100644
--- a/src/api/api_seq.cpp
+++ b/src/api/api_seq.cpp
@@ -286,6 +286,8 @@ extern "C" {
     MK_BINARY(Z3_mk_seq_contains, mk_c(c)->get_seq_fid(), OP_SEQ_CONTAINS, SKIP);
     MK_BINARY(Z3_mk_str_lt, mk_c(c)->get_seq_fid(), OP_STRING_LT, SKIP);
     MK_BINARY(Z3_mk_str_le, mk_c(c)->get_seq_fid(), OP_STRING_LE, SKIP);
+    MK_UNARY(Z3_mk_string_to_code, mk_c(c)->get_seq_fid(), OP_STRING_TO_CODE, SKIP);
+    MK_UNARY(Z3_mk_string_from_code, mk_c(c)->get_seq_fid(), OP_STRING_FROM_CODE, SKIP);
 
     MK_TERNARY(Z3_mk_seq_extract, mk_c(c)->get_seq_fid(), OP_SEQ_EXTRACT, SKIP);
     MK_TERNARY(Z3_mk_seq_replace, mk_c(c)->get_seq_fid(), OP_SEQ_REPLACE, SKIP);
diff --git a/src/api/python/z3/z3.py b/src/api/python/z3/z3.py
index 150df9f6b..13c922f85 100644
--- a/src/api/python/z3/z3.py
+++ b/src/api/python/z3/z3.py
@@ -10961,6 +10961,18 @@ def IntToStr(s):
     return SeqRef(Z3_mk_int_to_str(s.ctx_ref(), s.as_ast()), s.ctx)
 
 
+def StrToCode(s):
+    """Convert a unit length string to integer code"""
+    if not is_expr(s):
+        s = _py2expr(s)
+    return ArithRef(Z3_mk_string_to_code(s.ctx_ref(), s.as_ast()), s.ctx)
+
+def StrFromCode(c):
+    """Convert code to a string"""
+    if not is_expr(c):
+        c = _py2expr(c)
+    return SeqRef(Z3_mk_string_from_code(c.ctx_ref(), c.as_ast()), c.ctx)
+    
 def Re(s, ctx=None):
     """The regular expression that accepts sequence 's'
     >>> s1 = Re("ab")
diff --git a/src/api/z3_api.h b/src/api/z3_api.h
index d7a21ce20..0b0d286d1 100644
--- a/src/api/z3_api.h
+++ b/src/api/z3_api.h
@@ -1208,6 +1208,8 @@ typedef enum {
     Z3_OP_INT_TO_STR,
     Z3_OP_UBV_TO_STR,
     Z3_OP_SBV_TO_STR,
+    Z3_OP_STR_TO_CODE,
+    Z3_OP_STR_FROM_CODE,
     Z3_OP_STRING_LT,
     Z3_OP_STRING_LE,
 
@@ -3707,6 +3709,21 @@ extern "C" {
      */
     Z3_ast Z3_API Z3_mk_int_to_str(Z3_context c, Z3_ast s);
 
+
+    /**
+       \brief String to code conversion.
+       
+       def_API('Z3_mk_string_to_code', AST, (_in(CONTEXT), _in(AST)))
+    */
+    Z3_ast Z3_API Z3_mk_string_to_code(Z3_context c, Z3_ast a);
+
+    /**
+       \brief Code to string conversion.
+       
+       def_API('Z3_mk_string_from_code', AST, (_in(CONTEXT), _in(AST)))
+    */
+    Z3_ast Z3_API Z3_mk_string_from_code(Z3_context c, Z3_ast a);
+
     /**
        \brief Unsigned bit-vector to string conversion.