From 804f065215664fd5940e46be9abc8165c46afc95 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sun, 11 Apr 2021 17:42:12 -0700 Subject: [PATCH] fixes for #4688 https://github.com/Z3Prover/z3/issues/4866#issuecomment-778721073 --- src/ast/rewriter/seq_rewriter.cpp | 34 +++++++++++++++++++++++++++++++ src/ast/rewriter/seq_rewriter.h | 1 + src/ast/rewriter/th_rewriter.cpp | 24 +++++++++++++++++----- src/smt/theory_seq.cpp | 6 +++++- 4 files changed, 59 insertions(+), 6 deletions(-) diff --git a/src/ast/rewriter/seq_rewriter.cpp b/src/ast/rewriter/seq_rewriter.cpp index e8d07498f..4d01a0601 100644 --- a/src/ast/rewriter/seq_rewriter.cpp +++ b/src/ast/rewriter/seq_rewriter.cpp @@ -1157,6 +1157,17 @@ br_status seq_rewriter::mk_seq_extract(expr* a, expr* b, expr* c, expr_ref& resu return BR_REWRITE3; } + // (extract (extract a p l) 0 (len a)) -> (extract a p l) + if (str().is_extract(a, a1, b1, c1) && constantPos && pos == 0 && str().is_length(c, b1) && a1 == b1) { + result = a; + return BR_DONE; + } + + // (extract (extract a p l) 0 l) -> (extract a p l) + if (str().is_extract(a, a1, b1, c1) && constantPos && pos == 0 && c == c1) { + result = a; + return BR_DONE; + } // extract(extract(a, 3, 6), 1, len(extract(a, 3, 6)) - 1) -> extract(a, 4, 5) if (str().is_extract(a, a1, b1, c1) && is_suffix(a, b, c) && @@ -4382,6 +4393,29 @@ br_status seq_rewriter::reduce_re_eq(expr* l, expr* r, expr_ref& result) { return BR_FAILED; } +br_status seq_rewriter::mk_le_core(expr * l, expr * r, expr_ref & result) { + + // k <= len(x) -> true if k <= 0 + rational n; + if (str().is_length(r) && m_autil.is_numeral(l, n) && n <= 0) { + result = m().mk_true(); + return BR_DONE; + } + // len(x) <= 0 -> x = "" + // len(x) <= k -> false if k < 0 + expr* e = nullptr; + if (str().is_length(l, e) && m_autil.is_numeral(r, n)) { + if (n == 0) + result = str().mk_is_empty(e); + else if (n < 0) + result = m().mk_false(); + else + return BR_FAILED; + return BR_REWRITE1; + } + return BR_FAILED; +} + br_status seq_rewriter::mk_eq_core(expr * l, expr * r, expr_ref & result) { expr_ref_vector res(m()); expr_ref_pair_vector new_eqs(m()); diff --git a/src/ast/rewriter/seq_rewriter.h b/src/ast/rewriter/seq_rewriter.h index 122e50eb8..4d37482e3 100644 --- a/src/ast/rewriter/seq_rewriter.h +++ b/src/ast/rewriter/seq_rewriter.h @@ -330,6 +330,7 @@ public: br_status mk_app_core(func_decl * f, unsigned num_args, expr * const * args, expr_ref & result); br_status mk_eq_core(expr * lhs, expr * rhs, expr_ref & result); + br_status mk_le_core(expr* lhs, expr* rhs, expr_ref& result); br_status mk_bool_app(func_decl* f, unsigned n, expr* const* args, expr_ref& result); expr_ref mk_app(func_decl* f, expr_ref_vector const& args) { return mk_app(f, args.size(), args.c_ptr()); } diff --git a/src/ast/rewriter/th_rewriter.cpp b/src/ast/rewriter/th_rewriter.cpp index 89800d547..1892d4c9c 100644 --- a/src/ast/rewriter/th_rewriter.cpp +++ b/src/ast/rewriter/th_rewriter.cpp @@ -176,11 +176,8 @@ struct th_rewriter_cfg : public default_rewriter_cfg { // theory dispatch for = SASSERT(num == 2); family_id s_fid = args[0]->get_sort()->get_family_id(); - if (s_fid == m_a_rw.get_fid()) { + if (s_fid == m_a_rw.get_fid()) st = m_a_rw.mk_eq_core(args[0], args[1], result); - if (st == BR_FAILED && is_app(args[0]) && to_app(args[0])->get_family_id() == m_seq_rw.get_fid()) - st = m_seq_rw.mk_eq_core(args[0], args[1], result); - } else if (s_fid == m_bv_rw.get_fid()) st = m_bv_rw.mk_eq_core(args[0], args[1], result); else if (s_fid == m_dt_rw.get_fid()) @@ -208,13 +205,30 @@ struct th_rewriter_cfg : public default_rewriter_cfg { if (st != BR_FAILED) return st; } - if ((k == OP_AND || k == OP_OR /*|| k == OP_EQ*/) && m_seq_rw.u().has_re()) { + if ((k == OP_AND || k == OP_OR) && m_seq_rw.u().has_re()) { st = m_seq_rw.mk_bool_app(f, num, args, result); if (st != BR_FAILED) return st; } + if (k == OP_EQ && m_seq_rw.u().has_seq() && is_app(args[0]) && + to_app(args[0])->get_family_id() == m_seq_rw.get_fid()) { + st = m_seq_rw.mk_eq_core(args[0], args[1], result); + if (st != BR_FAILED) + return st; + } + return m_b_rw.mk_app_core(f, num, args, result); } + if (fid == m_a_rw.get_fid() && OP_LE == f->get_decl_kind() && m_seq_rw.u().has_seq()) { + st = m_seq_rw.mk_le_core(args[0], args[1], result); + if (st != BR_FAILED) + return st; + } + if (fid == m_a_rw.get_fid() && OP_GE == f->get_decl_kind() && m_seq_rw.u().has_seq()) { + st = m_seq_rw.mk_le_core(args[1], args[0], result); + if (st != BR_FAILED) + return st; + } if (fid == m_a_rw.get_fid()) return m_a_rw.mk_app_core(f, num, args, result); if (fid == m_bv_rw.get_fid()) diff --git a/src/smt/theory_seq.cpp b/src/smt/theory_seq.cpp index bb3fb1431..0296d2f46 100644 --- a/src/smt/theory_seq.cpp +++ b/src/smt/theory_seq.cpp @@ -1933,7 +1933,9 @@ model_value_proc * theory_seq::mk_value(enode * n, model_generator & mg) { sv->add_string(c); } else { - sv->add_string(mk_value(to_app(c))); + app_ref val(mk_value(to_app(c)), m); + TRACE("seq", tout << "WARNING: " << val << " is prone to result in incorrect model\n";); + sv->add_string(val); } } m_concat.shrink(start); @@ -2777,6 +2779,7 @@ bool theory_seq::propagate_eq(dependency* deps, literal_vector const& _lits, exp literal_vector lits(_lits); enode_pair_vector eqs; linearize(deps, eqs, lits); + if (add_to_eqs) { deps = mk_join(deps, _lits); new_eq_eh(deps, n1, n2); @@ -3219,6 +3222,7 @@ void theory_seq::get_ite_concat(ptr_vector& concats, ptr_vector& tod todo.pop_back(); e = m_rep.find(e); e = get_ite_value(e); + e = m_rep.find(e); if (m_util.str.is_concat(e, e1, e2)) { todo.push_back(e2, e1); }