From 584eee2cf4350d325992ae35eebcfaaa4606b867 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Fri, 2 Aug 2019 19:31:02 +0800 Subject: [PATCH] fixing #2448 and #2445 and #2443 Signed-off-by: Nikolaj Bjorner --- src/ast/rewriter/seq_rewriter.cpp | 15 ++++++++-- src/ast/rewriter/seq_rewriter.h | 1 + src/ast/seq_decl_plugin.cpp | 12 +++++--- src/ast/seq_decl_plugin.h | 17 +++++++---- src/smt/theory_seq.cpp | 47 ++++++------------------------- src/smt/theory_seq.h | 8 +----- 6 files changed, 43 insertions(+), 57 deletions(-) diff --git a/src/ast/rewriter/seq_rewriter.cpp b/src/ast/rewriter/seq_rewriter.cpp index 298a32c34..04a01d0b3 100644 --- a/src/ast/rewriter/seq_rewriter.cpp +++ b/src/ast/rewriter/seq_rewriter.cpp @@ -478,11 +478,12 @@ br_status seq_rewriter::mk_app_core(func_decl * f, unsigned num_args, expr * con SASSERT(num_args == 2); st = mk_seq_at(args[0], args[1], result); break; -#if 1 case OP_SEQ_NTH: SASSERT(num_args == 2); return mk_seq_nth(args[0], args[1], result); -#endif + case OP_SEQ_NTH_I: + SASSERT(num_args == 2); + return mk_seq_nth_i(args[0], args[1], result); case OP_SEQ_PREFIX: SASSERT(num_args == 2); st = mk_seq_prefix(args[0], args[1], result); @@ -991,6 +992,16 @@ br_status seq_rewriter::mk_seq_at(expr* a, expr* b, expr_ref& result) { } br_status seq_rewriter::mk_seq_nth(expr* a, expr* b, expr_ref& result) { + expr* es[2] = { a, b}; + expr* la = m_util.str.mk_length(a); + result = m().mk_ite(m().mk_and(m_autil.mk_le(m_autil.mk_int(0), b), m_autil.mk_lt(b, la)), + m().mk_app(m_util.get_family_id(), OP_SEQ_NTH_I, 2, es), + m().mk_app(m_util.get_family_id(), OP_SEQ_NTH_U, 2, es)); + return BR_REWRITE_FULL; +} + + +br_status seq_rewriter::mk_seq_nth_i(expr* a, expr* b, expr_ref& result) { zstring c; rational r; if (!m_autil.is_numeral(b, r) || !r.is_unsigned()) { diff --git a/src/ast/rewriter/seq_rewriter.h b/src/ast/rewriter/seq_rewriter.h index 13c93b3ca..8ff9c2c27 100644 --- a/src/ast/rewriter/seq_rewriter.h +++ b/src/ast/rewriter/seq_rewriter.h @@ -115,6 +115,7 @@ class seq_rewriter { br_status mk_seq_contains(expr* a, expr* b, expr_ref& result); br_status mk_seq_at(expr* a, expr* b, expr_ref& result); br_status mk_seq_nth(expr* a, expr* b, expr_ref& result); + br_status mk_seq_nth_i(expr* a, expr* b, expr_ref& result); 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); diff --git a/src/ast/seq_decl_plugin.cpp b/src/ast/seq_decl_plugin.cpp index 3ebb8280e..6a0cb3ff8 100644 --- a/src/ast/seq_decl_plugin.cpp +++ b/src/ast/seq_decl_plugin.cpp @@ -559,6 +559,8 @@ void seq_decl_plugin::init() { m_sigs[OP_SEQ_LAST_INDEX] = alloc(psig, m, "seq.last_indexof", 1, 2, seqAseqA, intT); m_sigs[OP_SEQ_AT] = alloc(psig, m, "seq.at", 1, 2, seqAintT, seqA); m_sigs[OP_SEQ_NTH] = alloc(psig, m, "seq.nth", 1, 2, seqAintT, A); + m_sigs[OP_SEQ_NTH_I] = alloc(psig, m, "seq.nth_i", 1, 2, seqAintT, A); + m_sigs[OP_SEQ_NTH_U] = alloc(psig, m, "seq.nth_u", 1, 2, seqAintT, A); m_sigs[OP_SEQ_LENGTH] = alloc(psig, m, "seq.len", 1, 1, &seqA, intT); m_sigs[OP_RE_PLUS] = alloc(psig, m, "re.+", 1, 1, &reA, reA); m_sigs[OP_RE_STAR] = alloc(psig, m, "re.*", 1, 1, &reA, reA); @@ -852,6 +854,8 @@ func_decl * seq_decl_plugin::mk_func_decl(decl_kind k, unsigned num_parameters, return mk_str_fun(k, arity, domain, range, OP_SEQ_AT); case OP_SEQ_NTH: + case OP_SEQ_NTH_I: + case OP_SEQ_NTH_U: 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)); @@ -1035,14 +1039,14 @@ bool seq_util::str::is_string(expr const* n, zstring& s) const { } } -bool seq_util::str::is_nth(expr const* n, expr*& s, unsigned& idx) const { +bool seq_util::str::is_nth_i(expr const* n, expr*& s, unsigned& idx) const { expr* i = nullptr; - if (!is_nth(n, s, i)) return false; + if (!is_nth_i(n, s, i)) return false; return arith_util(m).is_unsigned(i, idx); } -app* seq_util::str::mk_nth(expr* s, unsigned i) const { - return mk_nth(s, arith_util(m).mk_int(i)); +app* seq_util::str::mk_nth_i(expr* s, unsigned i) const { + return mk_nth_i(s, arith_util(m).mk_int(i)); } void seq_util::str::get_concat(expr* e, expr_ref_vector& es) const { diff --git a/src/ast/seq_decl_plugin.h b/src/ast/seq_decl_plugin.h index 3d71d80cf..38db9c078 100644 --- a/src/ast/seq_decl_plugin.h +++ b/src/ast/seq_decl_plugin.h @@ -41,6 +41,8 @@ enum seq_op_kind { OP_SEQ_REPLACE, OP_SEQ_AT, OP_SEQ_NTH, + OP_SEQ_NTH_I, + OP_SEQ_NTH_U, OP_SEQ_LENGTH, OP_SEQ_INDEX, OP_SEQ_LAST_INDEX, @@ -259,8 +261,8 @@ public: expr* mk_concat(expr_ref_vector const& es) const { return mk_concat(es.size(), es.c_ptr()); } app* mk_length(expr* a) const { return m.mk_app(m_fid, OP_SEQ_LENGTH, 1, &a); } app* mk_at(expr* s, expr* i) const { expr* es[2] = { s, i }; return m.mk_app(m_fid, OP_SEQ_AT, 2, es); } - app* mk_nth(expr* s, expr* i) const { expr* es[2] = { s, i }; return m.mk_app(m_fid, OP_SEQ_NTH, 2, es); } - app* mk_nth(expr* s, unsigned i) const; + app* mk_nth_i(expr* s, expr* i) const { expr* es[2] = { s, i }; return m.mk_app(m_fid, OP_SEQ_NTH_I, 2, es); } + app* mk_nth_i(expr* s, unsigned i) const; app* mk_substr(expr* a, expr* b, expr* c) const { expr* es[3] = { a, b, c }; return m.mk_app(m_fid, OP_SEQ_EXTRACT, 3, es); } app* mk_contains(expr* a, expr* b) const { expr* es[2] = { a, b }; return m.mk_app(m_fid, OP_SEQ_CONTAINS, 2, es); } @@ -277,7 +279,8 @@ public: 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); } - bool is_nth(func_decl* f) const { return is_decl_of(f, m_fid, OP_SEQ_NTH); } + bool is_nth_i(func_decl* f) const { return is_decl_of(f, m_fid, OP_SEQ_NTH_I); } + bool is_nth_u(func_decl* f) const { return is_decl_of(f, m_fid, OP_SEQ_NTH_U); } bool is_string(expr const * n) const { return is_app_of(n, m_fid, OP_STRING_CONST); } bool is_string(expr const* n, symbol& s) const { @@ -292,8 +295,9 @@ public: bool is_extract(expr const* n) const { return is_app_of(n, m_fid, OP_SEQ_EXTRACT); } bool is_contains(expr const* n) const { return is_app_of(n, m_fid, OP_SEQ_CONTAINS); } bool is_at(expr const* n) const { return is_app_of(n, m_fid, OP_SEQ_AT); } - bool is_nth(expr const* n) const { return is_app_of(n, m_fid, OP_SEQ_NTH); } - bool is_nth(expr const* n, expr*& s, unsigned& idx) const; + bool is_nth_i(expr const* n) const { return is_app_of(n, m_fid, OP_SEQ_NTH_I); } + bool is_nth_u(expr const* n) const { return is_app_of(n, m_fid, OP_SEQ_NTH_U); } + bool is_nth_i(expr const* n, expr*& s, unsigned& idx) const; bool is_index(expr const* n) const { return is_app_of(n, m_fid, OP_SEQ_INDEX); } bool is_last_index(expr const* n) const { return is_app_of(n, m_fid, OP_SEQ_LAST_INDEX); } bool is_replace(expr const* n) const { return is_app_of(n, m_fid, OP_SEQ_REPLACE); } @@ -321,7 +325,8 @@ public: MATCH_TERNARY(is_extract); MATCH_BINARY(is_contains); MATCH_BINARY(is_at); - MATCH_BINARY(is_nth); + MATCH_BINARY(is_nth_i); + MATCH_BINARY(is_nth_u); MATCH_BINARY(is_index); MATCH_TERNARY(is_index); MATCH_BINARY(is_last_index); diff --git a/src/smt/theory_seq.cpp b/src/smt/theory_seq.cpp index d9d68e721..cf4fd9ebf 100644 --- a/src/smt/theory_seq.cpp +++ b/src/smt/theory_seq.cpp @@ -274,7 +274,6 @@ theory_seq::theory_seq(ast_manager& m, theory_seq_params const & params): m_overlap(m), m_overlap2(m), m_len_prop_lvl(-1), - m_internal_nth_es(m), m_factory(nullptr), m_exclude(m), m_axioms(m), @@ -1985,16 +1984,9 @@ bool theory_seq::propagate_is_conc(expr* e, expr* conc) { bool theory_seq::is_unit_nth(expr* e) const { expr *s = nullptr; - return m_util.str.is_unit(e, s) && is_nth(s); + return m_util.str.is_unit(e, s) && m_util.str.is_nth_i(s); } -bool theory_seq::is_nth(expr* e) const { - return m_util.str.is_nth(e); -} - -bool theory_seq::is_nth(expr* e, expr*& e1, expr*& e2) const { - return m_util.str.is_nth(e, e1, e2); -} bool theory_seq::is_tail(expr* e, expr*& s, unsigned& idx) const { rational r; @@ -2017,14 +2009,8 @@ bool theory_seq::is_post(expr* e, expr*& s, expr*& i) { return is_skolem(m_post, e) && (s = to_app(e)->get_arg(0), i = to_app(e)->get_arg(1), true); } - - expr_ref theory_seq::mk_nth(expr* s, expr* idx) { - expr_ref result(m_util.str.mk_nth(s, idx), m); - if (!m_internal_nth_table.contains(result)) { - m_internal_nth_table.insert(result); - m_internal_nth_es.push_back(result); - } + expr_ref result(m_util.str.mk_nth_i(s, idx), m); return result; } @@ -2445,7 +2431,7 @@ bool theory_seq::solve_nth_eq(expr_ref_vector const& ls, expr_ref_vector const& for (unsigned i = 0; i < rs.size(); ++i) { unsigned k = 0; expr* ru = nullptr, *r = nullptr; - if (m_util.str.is_unit(rs.get(i), ru) && m_util.str.is_nth(ru, r, k) && k == i && r == l) { + if (m_util.str.is_unit(rs.get(i), ru) && m_util.str.is_nth_i(ru, r, k) && k == i && r == l) { continue; } return false; @@ -2461,10 +2447,6 @@ bool theory_seq::solve_unit_eq(expr_ref_vector const& l, expr_ref_vector const& if (r.size() == 1 && is_var(r[0]) && !occurs(r[0], l) && add_solution(r[0], mk_concat(l, m.get_sort(r[0])), deps)) { return true; } -// if (l.size() == 1 && r.size() == 1 && l[0] != r[0] && is_nth(l[0]) && add_solution(l[0], r[0], deps)) -// return true; -// if (l.size() == 1 && r.size() == 1 && l[0] != r[0] && is_nth(r[0]) && add_solution(r[0], l[0], deps)) -// return true; return false; } @@ -2493,10 +2475,6 @@ bool theory_seq::solve_unit_eq(expr* l, expr* r, dependency* deps) { if (is_var(r) && !occurs(r, l) && add_solution(r, l, deps)) { return true; } -// if (is_nth(l) && !occurs(l, r) && add_solution(l, r, deps)) -// return true; -// if (is_nth(r) && !occurs(r, l) && add_solution(r, l, deps)) -// return true; return false; } @@ -2529,7 +2507,7 @@ bool theory_seq::occurs(expr* a, expr* b) { else if (m_util.str.is_unit(b, e1)) { m_todo.push_back(e1); } - else if (m_util.str.is_nth(b, e1, e2)) { + else if (m_util.str.is_nth_i(b, e1, e2)) { m_todo.push_back(e1); } } @@ -4440,7 +4418,7 @@ void theory_seq::deque_axiom(expr* n) { else if (m_util.str.is_at(n)) { add_at_axiom(n); } - else if (m_util.str.is_nth(n)) { + else if (m_util.str.is_nth_i(n)) { add_nth_axiom(n); } else if (m_util.str.is_string(n)) { @@ -5207,12 +5185,12 @@ void theory_seq::add_nth_axiom(expr* e) { expr* s = nullptr, *i = nullptr; rational n; zstring str; - VERIFY(m_util.str.is_nth(e, s, i)); + VERIFY(m_util.str.is_nth_i(e, s, i)); if (m_util.str.is_string(s, str) && m_autil.is_numeral(i, n) && n.is_unsigned() && n.get_unsigned() < str.length()) { app_ref ch(m_util.str.mk_char(str[n.get_unsigned()]), m); add_axiom(mk_eq(ch, e, false)); } - else if (!m_internal_nth_table.contains(e)) { + else { expr_ref zero(m_autil.mk_int(0), m); literal i_ge_0 = mk_simplified_literal(m_autil.mk_ge(i, zero)); literal i_ge_len_s = mk_simplified_literal(m_autil.mk_ge(mk_sub(i, mk_len(s)), zero)); @@ -5563,7 +5541,7 @@ void theory_seq::assign_eh(bool_var v, bool is_true) { else if (m_util.str.is_lt(e) || m_util.str.is_le(e)) { m_lts.push_back(e); } - else if (is_nth(e)) { + else if (m_util.str.is_nth_i(e)) { // no-op } else { @@ -5693,7 +5671,6 @@ void theory_seq::push_scope_eh() { m_nqs.push_scope(); m_ncs.push_scope(); m_lts.push_scope(); - m_internal_nth_lim.push_back(m_internal_nth_es.size()); } void theory_seq::pop_scope_eh(unsigned num_scopes) { @@ -5715,12 +5692,6 @@ void theory_seq::pop_scope_eh(unsigned num_scopes) { m_len_prop_lvl = ctx.get_scope_level(); m_len_offset.reset(); } - unsigned old_sz = m_internal_nth_lim[m_internal_nth_lim.size() - num_scopes]; - for (unsigned i = m_internal_nth_es.size(); i-- > old_sz; ) { - m_internal_nth_table.erase(m_internal_nth_es.get(i)); - } - m_internal_nth_es.shrink(old_sz); - m_internal_nth_lim.shrink(m_internal_nth_lim.size() - num_scopes); } void theory_seq::restart_eh() { @@ -5731,7 +5702,7 @@ void theory_seq::relevant_eh(app* n) { m_util.str.is_replace(n) || m_util.str.is_extract(n) || m_util.str.is_at(n) || - m_util.str.is_nth(n) || + m_util.str.is_nth_i(n) || m_util.str.is_empty(n) || m_util.str.is_string(n) || m_util.str.is_itos(n) || diff --git a/src/smt/theory_seq.h b/src/smt/theory_seq.h index bb81e9c16..f09d06d74 100644 --- a/src/smt/theory_seq.h +++ b/src/smt/theory_seq.h @@ -338,10 +338,6 @@ namespace smt { obj_map> m_len_offset; int m_len_prop_lvl; - obj_hashtable m_internal_nth_table; - expr_ref_vector m_internal_nth_es; - unsigned_vector m_internal_nth_lim; - seq_factory* m_factory; // value factory exclusion_table m_exclude; // set of asserted disequalities. expr_ref_vector m_axioms; // list of axioms to add. @@ -399,7 +395,7 @@ namespace smt { void add_theory_assumptions(expr_ref_vector & assumptions) override; theory* mk_fresh(context* new_ctx) override { return alloc(theory_seq, new_ctx->get_manager(), m_params); } char const * get_name() const override { return "seq"; } - bool include_func_interp(func_decl* f) override { return false; } // m_util.str.is_nth(f); } + bool include_func_interp(func_decl* f) override { return m_util.str.is_nth_u(f); } theory_var mk_var(enode* n) override; void apply_sort_cnstr(enode* n, sort* s) override; void display(std::ostream & out) const override; @@ -532,8 +528,6 @@ namespace smt { bool is_var(expr* b) const; bool add_solution(expr* l, expr* r, dependency* dep); bool is_unit_nth(expr* a) const; - bool is_nth(expr* a) const; - bool is_nth(expr* a, expr*& e1, expr*& e2) const; bool is_tail(expr* a, expr*& s, unsigned& idx) const; bool is_eq(expr* e, expr*& a, expr*& b) const; bool is_pre(expr* e, expr*& s, expr*& i);