From c1480b43894cf191cb67dfcf4283a64e855f7508 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Mon, 12 Dec 2016 00:33:10 +0100 Subject: [PATCH] handle model generation from issue #748. Deal with warnings from #836 Signed-off-by: Nikolaj Bjorner --- src/ast/rewriter/seq_rewriter.cpp | 2 +- src/muz/rel/dl_product_relation.cpp | 6 +- src/muz/rel/dl_sieve_relation.cpp | 2 +- src/muz/rel/dl_sieve_relation.h | 3 +- src/smt/proto_model/numeral_factory.cpp | 2 +- src/smt/proto_model/numeral_factory.h | 2 +- src/smt/theory_bv.cpp | 2 +- src/smt/theory_seq.cpp | 121 +++++++++++++++++++++--- src/smt/theory_seq.h | 2 + 9 files changed, 118 insertions(+), 24 deletions(-) diff --git a/src/ast/rewriter/seq_rewriter.cpp b/src/ast/rewriter/seq_rewriter.cpp index b97d832b1..26c3e23e4 100644 --- a/src/ast/rewriter/seq_rewriter.cpp +++ b/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); } diff --git a/src/muz/rel/dl_product_relation.cpp b/src/muz/rel/dl_product_relation.cpp index 1bc5e3545..817ff194c 100644 --- a/src/muz/rel/dl_product_relation.cpp +++ b/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); diff --git a/src/muz/rel/dl_sieve_relation.cpp b/src/muz/rel/dl_sieve_relation.cpp index 9f9419089..7729ec2eb 100644 --- a/src/muz/rel/dl_sieve_relation.cpp +++ b/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 inner_cols(s.size()); extract_inner_columns(s, inner_plugin, inner_cols); diff --git a/src/muz/rel/dl_sieve_relation.h b/src/muz/rel/dl_sieve_relation.h index da6c9bbff..4d89a66ae 100644 --- a/src/muz/rel/dl_sieve_relation.h +++ b/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); diff --git a/src/smt/proto_model/numeral_factory.cpp b/src/smt/proto_model/numeral_factory.cpp index 413cc1b9e..49ff15167 100644 --- a/src/smt/proto_model/numeral_factory.cpp +++ b/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)); } diff --git a/src/smt/proto_model/numeral_factory.h b/src/smt/proto_model/numeral_factory.h index e0d3cf6b5..9b1ff6a81 100644 --- a/src/smt/proto_model/numeral_factory.h +++ b/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_ */ diff --git a/src/smt/theory_bv.cpp b/src/smt/theory_bv.cpp index a53580b73..a886c8a1e 100644 --- a/src/smt/theory_bv.cpp +++ b/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 { diff --git a/src/smt/theory_seq.cpp b/src/smt/theory_seq.cpp index 4f2683ca9..ed95ef8d7 100644 --- a/src/smt/theory_seq.cpp +++ b/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(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 m_dependencies; ptr_vector m_strings; - svector m_source; + svector 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 & 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++])); - } - else { + break; + 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(n, _val) && m_autil.is_numeral(_val, val) && val.is_int()) { + if (tha->get_value(next, _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(); } } diff --git a/src/smt/theory_seq.h b/src/smt/theory_seq.h index 0e06997ad..aa7ddec1b 100644 --- a/src/smt/theory_seq.h +++ b/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);