fix #5014

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

src/ast/arith_decl_plugin.h

@@ -432,6 +432,7 @@ public:
     app * mk_add(unsigned num_args, expr * const * args) const { return num_args == 1 && is_app(args[0]) ? to_app(args[0]) : m_manager.mk_app(m_afid, OP_ADD, num_args, args); }
     app * mk_add(expr * arg1, expr * arg2) const { return m_manager.mk_app(m_afid, OP_ADD, arg1, arg2); }
     app * mk_add(expr * arg1, expr * arg2, expr* arg3) const { return m_manager.mk_app(m_afid, OP_ADD, arg1, arg2, arg3); }
+    app * mk_add(expr_ref_vector const& args) const { return mk_add(args.size(), args.c_ptr()); }
 
     app * mk_sub(expr * arg1, expr * arg2) const { return m_manager.mk_app(m_afid, OP_SUB, arg1, arg2); }
     app * mk_sub(unsigned num_args, expr * const * args) const { return m_manager.mk_app(m_afid, OP_SUB, num_args, args); }

src/ast/char_decl_plugin.cpp

@@ -17,6 +17,7 @@ Author:
 --*/
 #include "util/gparams.h"
 #include "ast/char_decl_plugin.h"
+#include "ast/arith_decl_plugin.h"
 #include "ast/ast_pp.h"
 
 char_decl_plugin::char_decl_plugin(): 
@@ -46,7 +47,7 @@ func_decl* char_decl_plugin::mk_func_decl(decl_kind k, unsigned num_parameters,
 
     case OP_CHAR_CONST:
         if (num_parameters != 1)
-            msg << "incorrect number of parameters passed. Expected 1, recieved " << num_parameters;
+            msg << "incorrect number of parameters passed. Expected 1, received " << num_parameters;
         else if (arity != 0)
             msg << "incorrect number of arguments passed. Expected 1, received " << arity;
         else if (!parameters[0].is_int())
@@ -58,6 +59,16 @@ func_decl* char_decl_plugin::mk_func_decl(decl_kind k, unsigned num_parameters,
         else
             return m.mk_const_decl(m_charc_sym, m_char, func_decl_info(m_family_id, OP_CHAR_CONST, num_parameters, parameters));
         m.raise_exception(msg.str());
+    case OP_CHAR_TO_INT:
+        if (num_parameters != 0)
+            msg << "incorrect number of parameters passed. Expected 0, received " << num_parameters;
+        else if (arity != 1)
+            msg << "incorrect number of arguments passed. Expected one character, received " << arity;
+        else {
+            arith_util a(m);
+            return m.mk_func_decl(symbol("char.to_int"), arity, domain, a.mk_int(), func_decl_info(m_family_id, k, 0, nullptr));
+        }
+        m.raise_exception(msg.str());
     default:
         UNREACHABLE();
     }    
@@ -73,6 +84,7 @@ void char_decl_plugin::set_manager(ast_manager * m, family_id id) {
 void char_decl_plugin::get_op_names(svector<builtin_name>& op_names, symbol const& logic) {
     op_names.push_back(builtin_name("char.<=", OP_CHAR_LE));
     op_names.push_back(builtin_name("Char", OP_CHAR_CONST));
+    op_names.push_back(builtin_name("char.to_int", OP_CHAR_TO_INT));
 }
 
 void char_decl_plugin::get_sort_names(svector<builtin_name>& sort_names, symbol const& logic) {

src/ast/char_decl_plugin.h

@@ -32,7 +32,8 @@ enum char_sort_kind {
 
 enum char_op_kind {
     OP_CHAR_CONST,
-    OP_CHAR_LE
+    OP_CHAR_LE,
+    OP_CHAR_TO_INT
 };
 
 class char_decl_plugin : public decl_plugin {
@@ -76,12 +77,16 @@ public:
 
     app* mk_le(expr* a, expr* b);
 
+    app* mk_to_int(expr* a) { return m_manager->mk_app(m_family_id, OP_CHAR_TO_INT, 1, &a); }
+
     bool is_le(expr const* e) const { return is_app_of(e, m_family_id, OP_CHAR_LE); }
 
     bool is_const_char(expr const* e, unsigned& c) const { 
         return is_app_of(e, m_family_id, OP_CHAR_CONST) && (c = to_app(e)->get_parameter(0).get_int(), true);
     }
 
+    bool is_to_int(expr const* e) const { return is_app_of(e, m_family_id, OP_CHAR_TO_INT); }
+
     bool unicode() const { return m_unicode; }
     unsigned max_char() const { return m_unicode ? zstring::unicode_max_char() : zstring::ascii_max_char(); }
     unsigned num_bits() const { return m_unicode ? zstring::unicode_num_bits() : zstring::ascii_num_bits(); }

src/ast/seq_decl_plugin.cpp

@@ -767,6 +767,10 @@ bool seq_util::is_char_le(expr const* e) const {
     return ch.is_le(e);
 }
 
+bool seq_util::is_char2int(expr const* e) const {
+    return ch.is_to_int(e);
+}
+
 app* seq_util::mk_char(unsigned ch) const {
     return seq.mk_char(ch);
 }

src/ast/seq_decl_plugin.h

@@ -234,10 +234,12 @@ public:
     bool is_const_char(expr* e, unsigned& c) const;
     bool is_const_char(expr* e) const { unsigned c; return is_const_char(e, c); }
     bool is_char_le(expr const* e) const;
+    bool is_char2int(expr const* e) const;
     app* mk_char_bit(expr* e, unsigned i);
     app* mk_char(unsigned ch) const;
     app* mk_le(expr* ch1, expr* ch2) const;
     app* mk_lt(expr* ch1, expr* ch2) const;    
+    app* mk_char2int(expr* e) { return ch.mk_to_int(e); }
     unsigned max_char() const { return seq.max_char(); }
     unsigned num_bits() const { return seq.num_bits(); }
 
@@ -245,6 +247,7 @@ public:
     bool is_skolem(expr const* e) const { return is_app_of(e, m_fid, _OP_SEQ_SKOLEM); }
 
     MATCH_BINARY(is_char_le);
+    MATCH_UNARY(is_char2int);
 
     bool has_re() const { return seq.has_re(); }
     bool has_seq() const { return seq.has_seq(); }

src/sat/smt/ba_solver.cpp

@@ -1437,10 +1437,6 @@ namespace sat {
 
 
     bool ba_solver::init_watch(constraint& c) {
-        if (c.is_xr()) {
-            std::cout << c.is_xr() << "\n";
-        }
-
         return !inconsistent() && c.init_watch(*this);
     }
 

src/smt/seq_axioms.cpp

@@ -813,6 +813,7 @@ void seq_axioms::add_str_to_code_axiom(expr* n) {
     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.max_char()));
+    add_axiom(~len_is1, mk_eq(n, seq.mk_char2int(mk_nth(e, 0))));
     if (!seq.str.is_from_code(e))
         add_axiom(~len_is1, mk_eq(e, seq.str.mk_from_code(n)));
     add_axiom(len_is1, mk_eq(n, a.mk_int(-1)));

src/smt/theory_char.cpp

@@ -79,6 +79,9 @@ namespace smt {
         unsigned c = 0;
         if (seq.is_const_char(term, c))
             new_const_char(v, c);
+        expr* n = nullptr;
+        if (seq.is_char2int(term, n)) 
+            new_char2int(v, n);
         return true;
     }
 
@@ -216,6 +219,27 @@ namespace smt {
         }
     }
 
+    void theory_char::new_char2int(theory_var v, expr* c) {
+        theory_var w = ctx.get_enode(c)->get_th_var(get_id());
+        init_bits(w);
+        auto const& bits = get_ebits(w);
+        expr_ref_vector sum(m);
+        unsigned p = 0;
+        arith_util a(m);
+        for (auto b : bits) {
+            sum.push_back(m.mk_ite(b, a.mk_int(1 << p), a.mk_int(0)));
+            p++;
+        }
+        expr_ref sum_bits(a.mk_add(sum), m);
+        enode* n1 = get_enode(v);
+        enode* n2 = ensure_enode(sum_bits);
+        justification* j = 
+            ctx.mk_justification(
+                ext_theory_eq_propagation_justification(get_id(), ctx.get_region(), n1, n2));
+        ctx.assign_eq(n1, n2, eq_justification(j));
+    }
+
+
     /**
      * 1. Check that values of classes are unique.
      *    Check that values within each class is the same. 

src/smt/theory_char.h

@@ -57,6 +57,7 @@ namespace smt {
 
         bool final_check();
         void new_const_char(theory_var v, unsigned c);
+        void new_char2int(theory_var v, expr* c);
         unsigned get_char_value(theory_var v);
         void internalize_le(literal lit, app* term);