handle model generation from issue #748. Deal with warnings from #836

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

src/ast/rewriter/seq_rewriter.cpp

@@ -1721,7 +1721,7 @@ bool seq_rewriter::solve_itos(unsigned szl, expr* const* ls, unsigned szr, expr*
         }
     }
 
-    if (szr == 1 && m_util.str.is_itos(rs[0], r)) {
+    if (szr == 1 && m_util.str.is_itos(rs[0], r) && !m_util.str.is_itos(ls[0])) {
         return solve_itos(szr, rs, szl, ls, rhs, lhs, is_sat);
     }
 

src/muz/rel/dl_product_relation.cpp

@@ -255,7 +255,7 @@ namespace datalog {
             table_plugin & tplugin = rmgr.get_appropriate_plugin(tsig);
             relation_plugin & inner_plugin = rmgr.get_table_relation_plugin(tplugin);
 
-            return sieve_relation_plugin::get_plugin(rmgr).mk_full(p, sig, inner_plugin);
+            return sieve_relation_plugin::get_plugin(rmgr).full(p, sig, inner_plugin);
         }
 
         void init(relation_signature const& r1_sig, unsigned num_rels1, relation_base const* const* r1, 
@@ -294,7 +294,7 @@ namespace datalog {
                         rel2 = r1_plugin.mk_full(p, r2_sig, r1_kind);
                     }
                     else {
-                        rel2 = sieve_relation_plugin::get_plugin(rmgr).mk_full(p, r2_sig, r1_plugin);
+                        rel2 = sieve_relation_plugin::get_plugin(rmgr).full(p, r2_sig, r1_plugin);
                     }
                     m_offset1.push_back(i);
                     m_kind1.push_back(T_INPUT);
@@ -318,7 +318,7 @@ namespace datalog {
                         rel1 = r2_plugin.mk_full(p, r1_sig, r2_kind);
                     }
                     else {
-                        rel1 = sieve_relation_plugin::get_plugin(rmgr).mk_full(p, r1_sig, r2_plugin);
+                        rel1 = sieve_relation_plugin::get_plugin(rmgr).full(p, r1_sig, r2_plugin);
                     }
                     m_offset1.push_back(m_full.size());
                     m_kind1.push_back(T_FULL);

src/muz/rel/dl_sieve_relation.cpp

@@ -253,7 +253,7 @@ namespace datalog {
         return mk_from_inner(s, inner_cols, inner);
     }
 
-    sieve_relation * sieve_relation_plugin::mk_full(func_decl* p, const relation_signature & s, relation_plugin & inner_plugin) {
+    sieve_relation * sieve_relation_plugin::full(func_decl* p, const relation_signature & s, relation_plugin & inner_plugin) {
         SASSERT(!inner_plugin.is_sieve_relation()); //it does not make sense to make a sieve of a sieve
         svector<bool> inner_cols(s.size());
         extract_inner_columns(s, inner_plugin, inner_cols);

src/muz/rel/dl_sieve_relation.h

@@ -104,8 +104,7 @@ namespace datalog {
         sieve_relation * mk_empty(const relation_signature & s, relation_plugin & inner_plugin);
 
         virtual relation_base * mk_full(func_decl* p, const relation_signature & s);
-        sieve_relation * mk_full(func_decl* p, const relation_signature & s, relation_plugin & inner_plugin);
+        sieve_relation * full(func_decl* p, const relation_signature & s, relation_plugin & inner_plugin);
-
 
         sieve_relation * mk_from_inner(const relation_signature & s, const bool * inner_columns, 
             relation_base * inner_rel);

src/smt/proto_model/numeral_factory.cpp

@@ -47,6 +47,6 @@ app * bv_factory::mk_value_core(rational const & val, sort * s) {
     return m_util.mk_numeral(val, s);
 }
 
-app * bv_factory::mk_value(rational const & val, unsigned bv_size) {
+app * bv_factory::mk_num_value(rational const & val, unsigned bv_size) {
     return numeral_factory::mk_value(val, m_util.mk_sort(bv_size));
 }

src/smt/proto_model/numeral_factory.h

@@ -50,7 +50,7 @@ public:
     bv_factory(ast_manager & m);
     virtual ~bv_factory();
 
-    app * mk_value(rational const & val, unsigned bv_size);
+    app * mk_num_value(rational const & val, unsigned bv_size);
 };
 
 #endif /* NUMERAL_FACTORY_H_ */

src/smt/theory_bv.cpp

@@ -1583,7 +1583,7 @@ namespace smt {
 #endif
         get_fixed_value(v, val);
         SASSERT(r);
-        return alloc(expr_wrapper_proc, m_factory->mk_value(val, get_bv_size(v)));
+        return alloc(expr_wrapper_proc, m_factory->mk_num_value(val, get_bv_size(v)));
     }
 
     void theory_bv::display_var(std::ostream & out, theory_var v) const {

src/smt/theory_seq.cpp

@@ -2235,6 +2235,7 @@ bool theory_seq::add_stoi_axiom(expr* e) {
     context& ctx = get_context();
     expr* n;
     rational val;
+    TRACE("seq", tout << mk_pp(e, m) << "\n";);
     VERIFY(m_util.str.is_stoi(e, n));    
     if (get_num_value(e, val) && !m_stoi_axioms.contains(val)) {
         m_stoi_axioms.insert(val);
@@ -2252,13 +2253,70 @@ bool theory_seq::add_stoi_axiom(expr* e) {
             return true;
         }
     }
+    if (upper_bound(n, val) && get_length(n, val) && val.is_pos() && !m_stoi_axioms.contains(val)) {
+        zstring s;
+        SASSERT(val.is_unsigned());
+        unsigned sz = val.get_unsigned();
+        expr_ref len1(m), len2(m), ith_char(m), num(m), coeff(m);
+        expr_ref_vector nums(m);
+        len1 = m_util.str.mk_length(n);
+        len2 = m_autil.mk_int(sz);
+        literal lit = mk_eq(len1, len2, false);
+        literal_vector lits;
+        lits.push_back(~lit);
+        for (unsigned i = 0; i < sz; ++i) {
+            ith_char = mk_nth(n, m_autil.mk_int(i));
+            lits.push_back(~is_digit(ith_char));
+            nums.push_back(digit2int(ith_char));
+        }        
+        for (unsigned i = sz-1, c = 1; i > 0; c *= 10) {
+            --i;
+            coeff = m_autil.mk_int(c);
+            nums[i] = m_autil.mk_mul(coeff, nums[i].get());
+        }
+        num = m_autil.mk_add(nums.size(), nums.c_ptr());
+        lits.push_back(mk_eq(e, num, false));
+        ++m_stats.m_add_axiom;
+        m_new_propagation = true;
+        for (unsigned i = 0; i < lits.size(); ++i) {
+            ctx.mark_as_relevant(lits[i]);
+        }
+        ctx.mk_th_axiom(get_id(), lits.size(), lits.c_ptr());
+        m_stoi_axioms.insert(val);
+        m_trail_stack.push(insert_map<theory_seq, rational_set, rational>(m_stoi_axioms, val));
+        m_trail_stack.push(push_replay(alloc(replay_axiom, m, e)));
+        return true;
+    }
+    
     return false;
 }
 
+literal theory_seq::is_digit(expr* ch) {
+    bv_util bv(m);
+    literal isd = mk_literal(mk_skolem(symbol("seq.is_digit"), ch, 0, 0, m.mk_bool_sort()));
+    expr_ref d2i = digit2int(ch);
+    expr_ref _lo(bv.mk_ule(bv.mk_numeral(rational('0'), bv.mk_sort(8)), ch), m);
+    expr_ref _hi(bv.mk_ule(ch, bv.mk_numeral(rational('9'), bv.mk_sort(8))), m);
+    literal lo = mk_literal(_lo);
+    literal hi = mk_literal(_hi);
+    add_axiom(~lo, ~hi, isd);
+    add_axiom(~isd, lo);
+    add_axiom(~isd, hi);
+    for (unsigned i = 0; i < 10; ++i) {
+        add_axiom(~mk_eq(ch, bv.mk_numeral(rational('0'+i), bv.mk_sort(8)), false), mk_eq(d2i, m_autil.mk_int(i), false));
+    }
+    return isd;
+}
+
+expr_ref theory_seq::digit2int(expr* ch) {
+    return expr_ref(mk_skolem(symbol("seq.digit2int"), ch, 0, 0, m_autil.mk_int()), m);
+}
+
 bool theory_seq::add_itos_axiom(expr* e) {
     context& ctx = get_context();
     rational val;
     expr* n;
+    TRACE("seq", tout << mk_pp(e, m) << "\n";);
     VERIFY(m_util.str.is_itos(e, n));
     if (get_num_value(n, val)) {
         if (!m_itos_axioms.contains(val)) {
@@ -2282,6 +2340,9 @@ bool theory_seq::add_itos_axiom(expr* e) {
     else {
         // stoi(itos(n)) = n
         app_ref e2(m_util.str.mk_stoi(e), m);
+        if (ctx.e_internalized(e2) && ctx.get_enode(e2)->get_root() == ctx.get_enode(n)->get_root()) {
+            return false;
+        }
         add_axiom(mk_eq(e2, n, false));
         m_trail_stack.push(push_replay(alloc(replay_axiom, m, e)));
         return true;
@@ -2464,22 +2525,27 @@ void theory_seq::init_model(model_generator & mg) {
 
 
 class theory_seq::seq_value_proc : public model_value_proc {
+    enum source_t { unit_source, int_source, string_source };
     theory_seq&                     th;
     sort*                           m_sort;
     svector<model_value_dependency> m_dependencies;
     ptr_vector<expr>                m_strings;
-    svector<bool>                   m_source;
+    svector<source_t>               m_source;
 public:
     seq_value_proc(theory_seq& th, sort* s): th(th), m_sort(s) {
     }
     virtual ~seq_value_proc() {}
-    void add_dependency(enode* n) { 
+    void add_unit(enode* n) { 
         m_dependencies.push_back(model_value_dependency(n)); 
-        m_source.push_back(true);
+        m_source.push_back(unit_source);
+    }
+    void add_int(enode* n) { 
+        m_dependencies.push_back(model_value_dependency(n)); 
+        m_source.push_back(int_source);
     }
     void add_string(expr* n) {
         m_strings.push_back(n);
-        m_source.push_back(false);
+        m_source.push_back(string_source);
     }
     virtual void get_dependencies(buffer<model_value_dependency> & result) {
         result.append(m_dependencies.size(), m_dependencies.c_ptr());
@@ -2504,11 +2570,13 @@ public:
             unsigned sz;
 
             for (unsigned i = 0; i < m_source.size(); ++i) {
-                if (m_source[i]) {
+                switch (m_source[i]) {
+                case unit_source: {
                     VERIFY(bv.is_numeral(values[j++], val, sz));
                     sbuffer.push_back(val.get_unsigned());
+                    break;
                 }
-                else {
+                case string_source: {
                     dependency* deps = 0;
                     expr_ref tmp = th.canonize(m_strings[k], deps);
                     zstring zs;
@@ -2519,17 +2587,34 @@ public:
                         TRACE("seq", tout << "Not a string: " << tmp << "\n";);
                     }
                     ++k;
+                    break;
+                }
+                case int_source: {
+                    std::ostringstream strm;
+                    arith_util arith(th.m);
+                    VERIFY(arith.is_numeral(values[j++], val));
+                    if (val.is_neg()) strm << "-";
+                    strm << abs(val);
+                    zstring zs(strm.str().c_str());
+                    add_buffer(sbuffer, zs);
+                    break;
+                }
                 }
             }
             result = th.m_util.str.mk_string(zstring(sbuffer.size(), sbuffer.c_ptr()));
         }
         else {
             for (unsigned i = 0; i < m_source.size(); ++i) {
-                if (m_source[i]) {
+                switch (m_source[i]) {
+                case unit_source:
                     args.push_back(th.m_util.str.mk_unit(values[j++]));
-                }
+                    break;
-                else {
+                case string_source:
                     args.push_back(m_strings[k++]);
+                    break;
+                case int_source:
+                    UNREACHABLE();
+                    break;
                 }
             }
             result = th.mk_concat(args, m_sort);
@@ -2567,7 +2652,12 @@ model_value_proc * theory_seq::mk_value(enode * n, model_generator & mg) {
             TRACE("seq", tout << mk_pp(c, m) << "\n";);
             if (m_util.str.is_unit(c, c1)) {
                 if (ctx.e_internalized(c1)) {
-                    sv->add_dependency(ctx.get_enode(c1));
+                    sv->add_unit(ctx.get_enode(c1));
+                }
+            }
+            else if (m_util.str.is_itos(c, c1)) {
+                if (ctx.e_internalized(c1)) {
+                    sv->add_int(ctx.get_enode(c1));
                 }
             }
             else if (m_util.str.is_string(c)) {
@@ -2741,6 +2831,7 @@ expr_ref theory_seq::expand(expr* e0, dependency*& eqs) {
     }
     else if (m_util.str.is_itos(e, e1)) {
         rational val;
+        TRACE("seq", tout << mk_pp(e, m) << "\n";);
         if (get_num_value(e1, val)) {
             TRACE("seq", tout << mk_pp(e, m) << " -> " << val << "\n";);
             expr_ref num(m), res(m);
@@ -3177,13 +3268,12 @@ bool theory_seq::get_num_value(expr* e, rational& val) const {
     theory_mi_arith* tha = get_th_arith(ctx, m_autil.get_family_id(), e);
     expr_ref _val(m);
     if (!tha) return false;
-    enode* next = ctx.get_enode(e), *n;
+    enode* next = ctx.get_enode(e), *n = next;
     do { 
-        n = next;
+        if (tha->get_value(next, _val) && m_autil.is_numeral(_val, val) && val.is_int()) {
-        if (tha->get_value(n, _val) && m_autil.is_numeral(_val, val) && val.is_int()) {
             return true;
         }
-        next = n->get_next();
+        next = next->get_next();
     }
     while (next != n);
     return false;
@@ -3692,7 +3782,10 @@ void theory_seq::assign_eh(bool_var v, bool is_true) {
     else if (is_skolem(symbol("seq.split"), e)) {
         // propagate equalities
     }
+    else if (is_skolem(symbol("seq.is_digit"), e)) {
+    }
     else {
+        TRACE("seq", tout << mk_pp(e, m) << "\n";);
         UNREACHABLE();
     }
 }

src/smt/theory_seq.h

@@ -499,6 +499,8 @@ namespace smt {
         void add_in_re_axiom(expr* n);
         bool add_stoi_axiom(expr* n);
         bool add_itos_axiom(expr* n);
+        literal is_digit(expr* ch);
+        expr_ref digit2int(expr* ch);
         void add_itos_length_axiom(expr* n);
         literal mk_literal(expr* n);
         literal mk_eq_empty(expr* n, bool phase = true);