additional str/re operators, remove encoding option from zstring

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

src/api/api_seq.cpp

@@ -48,7 +48,7 @@ extern "C" {
         Z3_TRY;
         LOG_Z3_mk_string(c, str);
         RESET_ERROR_CODE();
-        zstring s(str, zstring::ascii);
+        zstring s(str);
         app* a = mk_c(c)->sutil().str.mk_string(s);
         mk_c(c)->save_ast_trail(a);
         RETURN_Z3(of_ast(a));
@@ -62,7 +62,7 @@ extern "C" {
         RESET_ERROR_CODE();
         unsigned_vector chs;
         for (unsigned i = 0; i < sz; ++i) chs.push_back(str[i]);
-        zstring s(sz, chs.c_ptr(), zstring::ascii);
+        zstring s(sz, chs.c_ptr());
         app* a = mk_c(c)->sutil().str.mk_string(s);
         mk_c(c)->save_ast_trail(a);
         RETURN_Z3(of_ast(a));

src/ast/rewriter/seq_rewriter.cpp

@@ -473,6 +473,9 @@ br_status seq_rewriter::mk_app_core(func_decl * f, unsigned num_args, expr * con
     case OP_RE_LOOP:
         st = mk_re_loop(f, num_args, args, result);
         break;
+    case OP_RE_POWER:
+        st = mk_re_power(f, args[0], result);
+        break;
     case OP_RE_EMPTY_SET:
         return BR_FAILED;    
     case OP_RE_FULL_SEQ_SET:
@@ -558,6 +561,18 @@ br_status seq_rewriter::mk_app_core(func_decl * f, unsigned num_args, expr * con
         SASSERT(num_args == 2);
         st = mk_str_lt(args[0], args[1], result);
         break;
+    case OP_STRING_FROM_CODE:
+        SASSERT(num_args == 1);
+        st = mk_str_from_code(args[0], result);
+        break;
+    case OP_STRING_TO_CODE:
+        SASSERT(num_args == 1);
+        st = mk_str_to_code(args[0], result);
+        break;
+    case OP_STRING_IS_DIGIT:
+        SASSERT(num_args == 1);
+        st = mk_str_is_digit(args[0], result);
+        break;
     case OP_STRING_CONST:
         st = BR_FAILED;
         if (!m_coalesce_chars) {
@@ -1493,6 +1508,19 @@ br_status seq_rewriter::mk_seq_replace(expr* a, expr* b, expr* c, expr_ref& resu
     return BR_FAILED;
 }
 
+br_status seq_rewriter::mk_seq_replace_all(expr* a, expr* b, expr* c, expr_ref& result) {
+    return BR_FAILED;
+}
+
+br_status seq_rewriter::mk_seq_replace_re_all(expr* a, expr* b, expr* c, expr_ref& result) {
+    return BR_FAILED;
+}
+
+br_status seq_rewriter::mk_seq_replace_re(expr* a, expr* b, expr* c, expr_ref& result) {
+    return BR_FAILED;
+}
+
+
 br_status seq_rewriter::mk_seq_prefix(expr* a, expr* b, expr_ref& result) {
     TRACE("seq", tout << mk_pp(a, m()) << " " << mk_pp(b, m()) << "\n";);
     zstring s1, s2;
@@ -1708,6 +1736,54 @@ br_status seq_rewriter::mk_str_lt(expr* a, expr* b, expr_ref& result) {
     return BR_FAILED;
 }
 
+br_status seq_rewriter::mk_str_from_code(expr* a, expr_ref& result) {
+    rational r;
+    if (m_autil.is_numeral(a, r)) {
+        if (r.is_neg() || r > m_util.str.max_char_value()) {
+            result = m_util.str.mk_string(symbol(""));
+        }
+        else {
+            unsigned num = r.get_unsigned();
+            zstring s(1, &num);
+            result = m_util.str.mk_string(s);
+        }
+        return BR_DONE;
+    }
+    return BR_FAILED;
+}
+
+br_status seq_rewriter::mk_str_to_code(expr* a, expr_ref& result) {
+    zstring str;
+    if (m_util.str.is_string(a, str)) {
+        if (str.length() == 1) 
+            result = m_autil.mk_int(str[0]);
+        else
+            result = m_autil.mk_int(-1);
+        return BR_DONE;
+    }    
+    return BR_FAILED;
+}
+
+br_status seq_rewriter::mk_str_is_digit(expr* a, expr_ref& result) {
+    zstring str;
+    if (m_util.str.is_string(a, str)) {
+        if (str.length() == 1 && '0' <= str[0] && str[0] <= '9')
+            result = m().mk_true();
+        else
+            result = m().mk_false();
+        return BR_DONE;
+    }
+    if (m_util.str.is_empty(a)) {
+        result = m().mk_false();
+        return BR_DONE;
+    }
+    // when a has length > 1 -> false
+    // when a is a unit character -> evaluate
+   
+    return BR_FAILED;
+}
+
+
 br_status seq_rewriter::mk_str_itos(expr* a, expr_ref& result) {
     rational r;
     if (m_autil.is_numeral(a, r)) {
@@ -2216,6 +2292,13 @@ br_status seq_rewriter::mk_re_loop(func_decl* f, unsigned num_args, expr* const*
     return BR_FAILED;
 }
 
+br_status seq_rewriter::mk_re_power(func_decl* f, expr* a, expr_ref& result) {
+    unsigned p = f->get_parameter(0).get_int();
+    result = m_util.re.mk_loop(a, p, p);
+    return BR_REWRITE1;
+}
+
+
 /*
   a** = a*
   (a* + b)* = (a + b)*

src/ast/rewriter/seq_rewriter.h

@@ -143,6 +143,9 @@ class seq_rewriter {
     br_status mk_seq_index(expr* a, expr* b, expr* c, expr_ref& result);
     br_status mk_seq_last_index(expr* a, expr* b, expr_ref& result);
     br_status mk_seq_replace(expr* a, expr* b, expr* c, expr_ref& result);
+    br_status mk_seq_replace_all(expr* a, expr* b, expr* c, expr_ref& result);
+    br_status mk_seq_replace_re_all(expr* a, expr* b, expr* c, expr_ref& result);
+    br_status mk_seq_replace_re(expr* a, expr* b, expr* c, expr_ref& result);
     br_status mk_seq_prefix(expr* a, expr* b, expr_ref& result);
     br_status mk_seq_suffix(expr* a, expr* b, expr_ref& result);
     br_status mk_str_units(func_decl* f, expr_ref& result);
@@ -152,6 +155,9 @@ class seq_rewriter {
     br_status mk_str_to_regexp(expr* a, expr_ref& result);
     br_status mk_str_le(expr* a, expr* b, expr_ref& result);
     br_status mk_str_lt(expr* a, expr* b, expr_ref& result);
+    br_status mk_str_from_code(expr* a, expr_ref& result);
+    br_status mk_str_to_code(expr* a, expr_ref& result);
+    br_status mk_str_is_digit(expr* a, expr_ref& result);
     br_status mk_re_concat(expr* a, expr* b, expr_ref& result);
     br_status mk_re_union(expr* a, expr* b, expr_ref& result);
     br_status mk_re_inter(expr* a, expr* b, expr_ref& result);
@@ -160,6 +166,7 @@ class seq_rewriter {
     br_status mk_re_diff(expr* a, expr* b, expr_ref& result);
     br_status mk_re_plus(expr* a, expr_ref& result);
     br_status mk_re_opt(expr* a, expr_ref& result);
+    br_status mk_re_power(func_decl* f, expr* a, expr_ref& result);
     br_status mk_re_loop(func_decl* f, unsigned num_args, expr* const* args, expr_ref& result);
     br_status mk_re_range(expr* lo, expr* hi, expr_ref& result);
     br_status lift_ite(func_decl* f, unsigned n, expr* const* args, expr_ref& result);

src/ast/seq_decl_plugin.cpp

@@ -158,10 +158,10 @@ static bool is_escape_char(char const *& s, unsigned& result) {
     return false;
 }
 
-zstring::zstring(encoding enc): m_encoding(enc) {}
+zstring::zstring() {}
 
-zstring::zstring(char const* s, encoding enc): m_encoding(enc) {
+zstring::zstring(char const* s) {
-    unsigned mask = 0xFF; // TBD for UTF
+    unsigned mask = 0xFF; // TBD for Unicode
     while (*s) {
         unsigned ch;
         if (is_escape_char(s, ch)) {
@@ -176,17 +176,14 @@ zstring::zstring(char const* s, encoding enc): m_encoding(enc) {
 
 zstring::zstring(zstring const& other) {
     m_buffer = other.m_buffer;
-    m_encoding = other.m_encoding;
 }
 
-zstring::zstring(unsigned sz, unsigned const* s, encoding enc) {
+zstring::zstring(unsigned sz, unsigned const* s) {
     m_buffer.append(sz, s);
-    m_encoding = enc;
 }
 
 zstring::zstring(unsigned num_bits, bool const* ch) {
-    SASSERT(num_bits == 8 || num_bits == 16);
+    SASSERT(num_bits == 8); // TBD for unicode
-    m_encoding = (num_bits == 8)?ascii:unicode;
     unsigned n = 0;
     for (unsigned i = 0; i < num_bits; ++i) {
         n |= (((unsigned)ch[i]) << i);
@@ -194,20 +191,19 @@ zstring::zstring(unsigned num_bits, bool const* ch) {
     m_buffer.push_back(n);
 }
 
-zstring::zstring(unsigned ch, encoding enc) {
+zstring::zstring(unsigned ch) {
-    m_encoding = enc;
+    SASSERT(ch <= 196607);
-    m_buffer.push_back(ch & ((enc == ascii)?0x000000FF:0x0000FFFF));
+    m_buffer.push_back(ch);
 }
 
 zstring& zstring::operator=(zstring const& other) {
-    m_encoding = other.m_encoding;
     m_buffer.reset();
     m_buffer.append(other.m_buffer);
     return *this;
 }
 
 zstring zstring::replace(zstring const& src, zstring const& dst) const {
-    zstring result(m_encoding);
+    zstring result;
     if (length() < src.length()) {
         return zstring(*this);
     }
@@ -272,7 +268,6 @@ std::string zstring::encode() const {
 }
 
 std::string zstring::as_string() const {
-    SASSERT(m_encoding == ascii); 
     std::ostringstream strm;
     char buffer[100];
     unsigned offset = 0;
@@ -351,7 +346,7 @@ int zstring::last_indexof(zstring const& other) const {
 }
 
 zstring zstring::extract(unsigned offset, unsigned len) const {
-    zstring result(m_encoding);
+    zstring result;
     if (offset + len < offset) return result;
     int last = std::min(offset+len, length());
     for (int i = offset; i < last; ++i) {
@@ -361,7 +356,6 @@ zstring zstring::extract(unsigned offset, unsigned len) const {
 }
 
 zstring zstring::operator+(zstring const& other) const {
-    SASSERT(m_encoding == other.m_encoding);
     zstring result(*this);
     result.m_buffer.append(other.m_buffer);
     return result;
@@ -578,6 +572,8 @@ void seq_decl_plugin::init() {
     sort* boolT = m.mk_bool_sort();
     sort* intT  = arith_util(m).mk_int();
     sort* predA = array_util(m).mk_array_sort(A, boolT);
+    sort* seqAseqAseqA[3] = { seqA, seqA, seqA };
+    sort* seqAreAseqA[3] = { seqA, reA, seqA };
     sort* seqAseqA[2] = { seqA, seqA };
     sort* seqAreA[2] = { seqA, reA };
     sort* reAreA[2] = { reA, reA };
@@ -615,6 +611,7 @@ void seq_decl_plugin::init() {
     m_sigs[OP_RE_UNION]      = alloc(psig, m, "re.union",     1, 2, reAreA, reA);
     m_sigs[OP_RE_INTERSECT]  = alloc(psig, m, "re.inter",     1, 2, reAreA, reA);
     m_sigs[OP_RE_LOOP]           = alloc(psig, m, "re.loop",    1, 1, &reA, reA);
+    m_sigs[OP_RE_POWER]          = alloc(psig, m, "re.^", 1, 1, &reA, reA);
     m_sigs[OP_RE_COMPLEMENT]     = alloc(psig, m, "re.comp", 1, 1, &reA, reA);
     m_sigs[OP_RE_EMPTY_SET]      = alloc(psig, m, "re.empty", 1, 0, nullptr, reA);
     m_sigs[OP_RE_FULL_SEQ_SET]   = alloc(psig, m, "re.all", 1, 0, nullptr, reA);
@@ -622,6 +619,9 @@ void seq_decl_plugin::init() {
     m_sigs[OP_RE_OF_PRED]        = alloc(psig, m, "re.of.pred", 1, 1, &predA, reA);
     m_sigs[OP_SEQ_TO_RE]         = alloc(psig, m, "seq.to.re",  1, 1, &seqA, reA);
     m_sigs[OP_SEQ_IN_RE]         = alloc(psig, m, "seq.in.re", 1, 2, seqAreA, boolT);
+    m_sigs[OP_SEQ_REPLACE_RE_ALL] = alloc(psig, m, "str.replace_re_all", 1, 3, seqAreAseqA, seqA);
+    m_sigs[OP_SEQ_REPLACE_RE]    = alloc(psig, m, "str.replace_re", 1, 3, seqAreAseqA, seqA);
+    m_sigs[OP_SEQ_REPLACE_ALL]   = alloc(psig, m, "str.replace_all", 1, 3, seqAseqAseqA, seqA);
     m_sigs[OP_STRING_CONST]      = nullptr;
     m_sigs[_OP_STRING_STRIDOF]   = alloc(psig, m, "str.indexof", 0, 3, str2TintT, intT);
     m_sigs[_OP_STRING_STRREPL]   = alloc(psig, m, "str.replace", 0, 3, str3T, strT);
@@ -629,6 +629,9 @@ void seq_decl_plugin::init() {
     m_sigs[OP_STRING_STOI]       = alloc(psig, m, "str.to_int", 0, 1, &strT, intT);
     m_sigs[OP_STRING_LT]         = alloc(psig, m, "str.<", 0, 2, str2T, boolT);
     m_sigs[OP_STRING_LE]         = alloc(psig, m, "str.<=", 0, 2, str2T, boolT);
+    m_sigs[OP_STRING_IS_DIGIT]   = alloc(psig, m, "str.is_digit", 0, 1, &strT, boolT);
+    m_sigs[OP_STRING_TO_CODE]    = alloc(psig, m, "str.to_code", 0, 1, &strT, intT);
+    m_sigs[OP_STRING_FROM_CODE]  = alloc(psig, m, "str.from_code", 0, 1, &intT, strT);
     m_sigs[_OP_STRING_CONCAT]    = alloc(psig, m, "str.++", 1, 2, str2T, strT);
     m_sigs[_OP_STRING_LENGTH]    = alloc(psig, m, "str.len", 0, 1, &strT, intT);
     m_sigs[_OP_STRING_STRCTN]    = alloc(psig, m, "str.contains", 0, 2, str2T, boolT);
@@ -752,6 +755,9 @@ func_decl * seq_decl_plugin::mk_func_decl(decl_kind k, unsigned num_parameters,
     case OP_STRING_STOI:
     case OP_STRING_LT:
     case OP_STRING_LE:
+    case OP_STRING_IS_DIGIT:
+    case OP_STRING_TO_CODE:
+    case OP_STRING_FROM_CODE:
         match(*m_sigs[k], arity, domain, range, rng);
         return m.mk_func_decl(m_sigs[k]->m_name, arity, domain, rng, func_decl_info(m_family_id, k));
         
@@ -812,6 +818,13 @@ func_decl * seq_decl_plugin::mk_func_decl(decl_kind k, unsigned num_parameters,
         default:
             m.raise_exception("Incorrect number of arguments passed to loop. Expected 1 regular expression and two integer parameters");
         }
+    case OP_RE_POWER:
+        m_has_re = true;
+        if (num_parameters == 1 && parameters[0].is_int() && arity == 1 && parameters[0].get_int() >= 0) {
+            rng = domain[0];
+            return m.mk_func_decl(m_sigs[k]->m_name, arity, domain, rng, func_decl_info(m_family_id, k, num_parameters, parameters));
+        }
+        m.raise_exception("Incorrect arguments used for re.^. Expected one non-negative integer parameter");
 
     case OP_STRING_CONST:
         if (!(num_parameters == 1 && arity == 0 && parameters[0].is_symbol())) {
@@ -823,6 +836,7 @@ func_decl * seq_decl_plugin::mk_func_decl(decl_kind k, unsigned num_parameters,
     case OP_RE_UNION:
     case OP_RE_CONCAT:
     case OP_RE_INTERSECT:
+    case OP_RE_DIFF:
         m_has_re = true;
         return mk_assoc_fun(k, arity, domain, range, k, k);
 
@@ -1066,11 +1080,13 @@ app* seq_util::str::mk_string(zstring const& s) const {
 }
 
 app*  seq_util::str::mk_char(zstring const& s, unsigned idx) const {
-    return u.bv().mk_numeral(s[idx], s.num_bits());
+    // TBD: change to unicode
+    return u.bv().mk_numeral(s[idx], 8);
 }
 
 app*  seq_util::str::mk_char(char ch) const {
-    zstring s(ch, zstring::ascii);
+    // TBD: change to unicode
+    zstring s(ch);
     return mk_char(s, 0);
 }
 

src/ast/seq_decl_plugin.h

@@ -17,15 +17,6 @@ Revision History:
 
     Updated to string sequences 2015-12-5
 
-TBD: 
--  ((_ re.^ n) RegLan RegLan)
--  (str.replace_re_all String RegLan String String) 
--  (str.replace_re String RegLan String String)
--  (str.replace_all String String String String)
--  (str.is_digit String Bool)                     would replace smt/seq_skolem is_digit.
--  (str.to_code String Int)
--  (str.from_code Int String) 
-
 --*/
 #ifndef SEQ_DECL_PLUGIN_H_
 #define SEQ_DECL_PLUGIN_H_
@@ -60,6 +51,9 @@ enum seq_op_kind {
     OP_SEQ_LAST_INDEX,
     OP_SEQ_TO_RE,
     OP_SEQ_IN_RE,
+    OP_SEQ_REPLACE_RE_ALL, // Seq -> RegEx -> Seq -> Seq
+    OP_SEQ_REPLACE_RE,     // Seq -> RegEx -> Seq -> Seq
+    OP_SEQ_REPLACE_ALL,    // Seq -> Seq -> Seq -> Seq
 
     OP_RE_PLUS,
     OP_RE_STAR,
@@ -70,6 +64,7 @@ enum seq_op_kind {
     OP_RE_DIFF,
     OP_RE_INTERSECT,
     OP_RE_LOOP,
+    OP_RE_POWER,
     OP_RE_COMPLEMENT,
     OP_RE_EMPTY_SET,
     OP_RE_FULL_SEQ_SET,
@@ -83,6 +78,9 @@ enum seq_op_kind {
     OP_STRING_STOI,
     OP_STRING_LT,
     OP_STRING_LE,
+    OP_STRING_IS_DIGIT,
+    OP_STRING_TO_CODE,
+    OP_STRING_FROM_CODE,
     // internal only operators. Converted to SEQ variants.
     _OP_STRING_STRREPL,
     _OP_STRING_CONCAT,
@@ -103,25 +101,17 @@ enum seq_op_kind {
 
 
 class zstring {
-public:
-    enum encoding {
-        ascii,
-        unicode
-    };
 private:
     buffer<unsigned> m_buffer;
-    encoding         m_encoding;
 public:
-    zstring(encoding enc = ascii);
+    zstring();
-    zstring(char const* s, encoding enc = ascii);
+    zstring(char const* s);
-    zstring(unsigned sz, unsigned const* s, encoding enc = ascii);
+    zstring(unsigned sz, unsigned const* s);
     zstring(zstring const& other);
     zstring(unsigned num_bits, bool const* ch);
-    zstring(unsigned ch, encoding enc = ascii);
+    zstring(unsigned ch);
     zstring& operator=(zstring const& other);
     zstring replace(zstring const& src, zstring const& dst) const;
-    unsigned num_bits() const { return (m_encoding==ascii)?8:16; }
-    encoding get_encoding() const { return m_encoding; }
     std::string encode() const;
     std::string as_string() const;
     unsigned length() const { return m_buffer.size(); }
@@ -267,6 +257,9 @@ public:
     public:
         str(seq_util& u): u(u), m(u.m), m_fid(u.m_fid) {}
 
+        unsigned min_char_value() const { return 0; }
+        unsigned max_char_value() const { return 196607; }
+
         sort* mk_seq(sort* s) const { parameter param(s); return m.mk_sort(m_fid, SEQ_SORT, 1, &param); }
         sort* mk_string_sort() const { return m.mk_sort(m_fid, _STRING_SORT, 0, nullptr); }
         app* mk_empty(sort* s) const { return m.mk_const(m.mk_func_decl(m_fid, OP_SEQ_EMPTY, 0, nullptr, 0, (expr*const*)nullptr, s)); }
@@ -300,6 +293,9 @@ public:
         app* mk_is_empty(expr* s) const;
         app* mk_lex_lt(expr* a, expr* b) const { expr* es[2] = { a, b }; return m.mk_app(m_fid, OP_STRING_LT, 2, es); }
         app* mk_lex_le(expr* a, expr* b) const { expr* es[2] = { a, b }; return m.mk_app(m_fid, OP_STRING_LE, 2, es); }
+        app* mk_to_code(expr* e) const { return m.mk_app(m_fid, OP_STRING_TO_CODE, 1, &e); }
+        app* mk_from_code(expr* e) const { return m.mk_app(m_fid, OP_STRING_FROM_CODE, 1, &e); }
+        app* mk_is_digit(expr* e) const { return m.mk_app(m_fid, OP_STRING_IS_DIGIT, 1, &e); }
 
 
         bool is_nth_i(func_decl const* f)       const { return is_decl_of(f, m_fid, OP_SEQ_NTH_I); }
@@ -335,6 +331,9 @@ public:
         bool is_unit(expr const* n)     const { return is_app_of(n, m_fid, OP_SEQ_UNIT); }
         bool is_lt(expr const* n)       const { return is_app_of(n, m_fid, OP_STRING_LT); }
         bool is_le(expr const* n)       const { return is_app_of(n, m_fid, OP_STRING_LE); }
+        bool is_is_digit(expr const* n) const { return is_app_of(n, m_fid, OP_STRING_IS_DIGIT); }
+        bool is_from_code(expr const* n) const { return is_app_of(n, m_fid, OP_STRING_TO_CODE); }
+        bool is_to_code(expr const* n) const { return is_app_of(n, m_fid, OP_STRING_FROM_CODE); }
 
         bool is_string_term(expr const * n) const {
             sort * s = get_sort(n);
@@ -363,6 +362,9 @@ public:
         MATCH_BINARY(is_le);
         MATCH_UNARY(is_itos);
         MATCH_UNARY(is_stoi);
+        MATCH_UNARY(is_is_digit);
+        MATCH_UNARY(is_from_code);
+        MATCH_UNARY(is_to_code);
         MATCH_BINARY(is_in_re);
         MATCH_UNARY(is_unit);
 

src/math/lp/nla_monotone_lemmas.cpp

@@ -50,10 +50,11 @@ void monotone::monotonicity_lemma(monic const& m) {
     Example:
 
     0 >= x >= -2 & 0 <= y <= 3 => x*y >= -6
-
+    0 >= x >= -2 & 0 <= y <= 3 => x*x*y <= 12
+    
 */
 void monotone::monotonicity_lemma_gt(const monic& m) {
-    new_lemma lemma(c(), __FUNCTION__);
+    new_lemma lemma(c(), "monotonicity > ");
     rational product(1);
     for (lpvar j : m.vars()) {
         auto v = c().val(j);
@@ -75,7 +76,7 @@ void monotone::monotonicity_lemma_gt(const monic& m) {
     x <= -2 & y >= 3 => x*y <= -6
 */
 void monotone::monotonicity_lemma_lt(const monic& m) {
-    new_lemma lemma(c(), __FUNCTION__);
+    new_lemma lemma(c(), "monotonicity <");
     rational product(1);
     for (lpvar j : m.vars()) {
         auto v = c().val(j);

src/math/lp/nla_order_lemmas.cpp

@@ -289,6 +289,7 @@ void order::generate_ol(const monic& ac,
     lemma |= ineq(c.var(), val(c.var()).is_neg() ? llc::GE : llc::LE, 0);
     _().negate_var_relation_strictly(lemma, ac.var(), bc.var());
     _().negate_var_relation_strictly(lemma, a.var(),  b.var());
+
     lemma &= ac;
     lemma &= a;
     lemma &= bc;

src/smt/seq_axioms.cpp

@@ -771,6 +771,59 @@ void seq_axioms::add_le_axiom(expr* n) {
     add_axiom(~lt, le);
 }
 
+/**
+   is_digit(e) <=> e = '0' or ... or e = '9'
+ */
+void seq_axioms::add_is_digit_axiom(expr* n) {
+    expr* e = nullptr;
+    VERIFY(seq.str.is_is_digit(n, e)); 
+    literal is_digit = mk_literal(n);
+    literal_vector digits;
+    digits.push_back(~is_digit);
+    for (unsigned i = 0; i < 10; ++i) {
+        unsigned d = '0' + i;
+        zstring str(1, &d);
+        expr_ref s(seq.str.mk_string(str), m);
+        m_rewrite(s); // if the solver depends on unit normal form
+        literal digit_i = mk_eq(e, s); 
+        digits.push_back(digit_i);
+        add_axiom(~digit_i, is_digit);        
+    }
+    // literals are marked relevant by add_axiom of binary clauses
+    ctx().mk_th_axiom(th.get_id(), digits);
+}
+
+/**
+   len(e) = 1 => 0 <= to_code(e) <= max_code
+   len(e) != 1 => to_code(e) = -1
+ */
+void seq_axioms::add_str_to_code_axiom(expr* n) {
+    expr* e = nullptr;
+    VERIFY(seq.str.is_to_code(n, e)); 
+    literal len_is1 = mk_eq(mk_len(e), a.mk_int(1));
+    add_axiom(~len_is1, mk_ge(n, 0)); 
+    add_axiom(~len_is1, mk_le(n, seq.str.max_char_value())); 
+    add_axiom(len_is1, mk_eq(n, a.mk_int(-1)));
+}
+
+/**
+   0 <= e <= max_char => len(from_code(e)) = 1
+   0 <= e <= max_char => to_code(from_code(e)) = e
+   e < 0 or e > max_char => len(from_code(e)) = ""
+ */
+void seq_axioms::add_str_from_code_axiom(expr* n) {
+    expr* e = nullptr;
+    VERIFY(seq.str.is_from_code(n, e)); 
+    literal ge = mk_ge(e, 0);
+    literal le = mk_le(e, seq.str.max_char_value());
+    literal emp = mk_literal(seq.str.mk_is_empty(n));
+    add_axiom(~ge, ~le, mk_eq(mk_len(n), a.mk_int(1)));
+    add_axiom(~ge, ~le, mk_eq(seq.str.mk_to_code(n), e));
+    add_axiom(ge, emp);
+    add_axiom(le, emp);
+}
+
+
 /**
 Unit is injective:
 

src/smt/seq_axioms.h

@@ -84,6 +84,9 @@ namespace smt {
         void add_itos_axiom(expr* s, unsigned k);
         void add_lt_axiom(expr* n);
         void add_le_axiom(expr* n);
+        void add_is_digit_axiom(expr* n);
+        void add_str_to_code_axiom(expr* n);
+        void add_str_from_code_axiom(expr* n);
         void add_unit_axiom(expr* n);
         void add_length_axiom(expr* n);
         void unroll_not_contains(expr* n);