From aab50ff3f53da7315548e9fb59dbb913573442c1 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Tue, 21 Jul 2020 15:50:19 -0700 Subject: [PATCH] fixing bugs reported in #4518 Signed-off-by: Nikolaj Bjorner --- src/smt/seq_axioms.cpp | 17 +++++++++++++++++ src/smt/seq_eq_solver.cpp | 16 ++++++---------- src/smt/seq_skolem.h | 9 +++++++++ src/smt/theory_seq.cpp | 39 ++++++++++++++++++++++++++++++++++++++- src/smt/theory_seq.h | 1 - 5 files changed, 70 insertions(+), 12 deletions(-) diff --git a/src/smt/seq_axioms.cpp b/src/smt/seq_axioms.cpp index 3a5c57f3cbe..48203105e17 100644 --- a/src/smt/seq_axioms.cpp +++ b/src/smt/seq_axioms.cpp @@ -846,6 +846,13 @@ void seq_axioms::add_suffix_axiom(expr* e) { m_rewrite(t); literal lit = mk_literal(e); literal s_gt_t = mk_ge(mk_sub(mk_len(s), mk_len(t)), 1); +#if 0 + expr_ref x = m_sk.mk_pre(t, mk_sub(mk_len(t), mk_len(s))); + expr_ref y = m_sk.mk_tail(t, mk_sub(mk_len(s), a.mk_int(1))); + add_axiom(lit, s_gt_t, mk_seq_eq(t, mk_concat(x, y))); + add_axiom(lit, s_gt_t, mk_eq(mk_len(y), mk_len(s))); + add_axiom(lit, s_gt_t, ~mk_eq(y, s)); +#else sort* char_sort = nullptr; VERIFY(seq.is_seq(m.get_sort(s), char_sort)); expr_ref x = m_sk.mk("seq.suffix.x", s, t); @@ -856,6 +863,7 @@ void seq_axioms::add_suffix_axiom(expr* e) { add_axiom(lit, s_gt_t, mk_seq_eq(s, mk_concat(y, seq.str.mk_unit(c), x))); add_axiom(lit, s_gt_t, mk_seq_eq(t, mk_concat(z, seq.str.mk_unit(d), x))); add_axiom(lit, s_gt_t, ~mk_eq(c, d)); +#endif } void seq_axioms::add_prefix_axiom(expr* e) { @@ -866,6 +874,14 @@ void seq_axioms::add_prefix_axiom(expr* e) { m_rewrite(t); literal lit = mk_literal(e); literal s_gt_t = mk_ge(mk_sub(mk_len(s), mk_len(t)), 1); +#if 0 + expr_ref x = m_sk.mk_pre(t, mk_len(s)); + expr_ref y = m_sk.mk_tail(t, mk_sub(mk_sub(mk_len(t), mk_len(s)), a.mk_int(1))); + add_axiom(lit, s_gt_t, mk_seq_eq(t, mk_concat(x, y))); + add_axiom(lit, s_gt_t, mk_eq(mk_len(x), mk_len(s))); + add_axiom(lit, s_gt_t, ~mk_eq(x, s)); + +#else sort* char_sort = nullptr; VERIFY(seq.is_seq(m.get_sort(s), char_sort)); expr_ref x = m_sk.mk("seq.prefix.x", s, t); @@ -876,6 +892,7 @@ void seq_axioms::add_prefix_axiom(expr* e) { add_axiom(lit, s_gt_t, mk_seq_eq(s, mk_concat(x, seq.str.mk_unit(c), y))); add_axiom(lit, s_gt_t, mk_seq_eq(t, mk_concat(x, seq.str.mk_unit(d), z)), mk_seq_eq(t, x)); add_axiom(lit, s_gt_t, ~mk_eq(c, d)); +#endif } /*** diff --git a/src/smt/seq_eq_solver.cpp b/src/smt/seq_eq_solver.cpp index ab83768c672..5a0028567ab 100644 --- a/src/smt/seq_eq_solver.cpp +++ b/src/smt/seq_eq_solver.cpp @@ -758,10 +758,6 @@ bool theory_seq::branch_ternary_variable() { } -bool theory_seq::eq_unit(expr* l, expr* r) const { - return l == r || is_unit_nth(l) || is_unit_nth(r); -} - // exists x, y, rs' != empty s.t. (ls = x ++ rs ++ y) || (ls = rs' ++ y && rs = x ++ rs') bool theory_seq::can_align_from_lhs(expr_ref_vector const& ls, expr_ref_vector const& rs) { SASSERT(!ls.empty() && !rs.empty()); @@ -773,7 +769,7 @@ bool theory_seq::can_align_from_lhs(expr_ref_vector const& ls, expr_ref_vector c return result; } for (unsigned i = 0; i < ls.size(); ++i) { - if (eq_unit(ls[i], rs.back())) { + if (!m.are_distinct(ls[i], rs.back())) { bool same = true; if (i == 0) { m_overlap_lhs.insert(pair, true); @@ -783,7 +779,7 @@ bool theory_seq::can_align_from_lhs(expr_ref_vector const& ls, expr_ref_vector c if (rs.size() > i) { unsigned diff = rs.size() - (i + 1); for (unsigned j = 0; same && j < i; ++j) { - same = eq_unit(ls[j], rs[diff + j]); + same = !m.are_distinct(ls[j], rs[diff + j]); } if (same) { m_overlap_lhs.insert(pair, true); @@ -794,7 +790,7 @@ bool theory_seq::can_align_from_lhs(expr_ref_vector const& ls, expr_ref_vector c else { unsigned diff = (i + 1) - rs.size(); for (unsigned j = 0; same && j < rs.size()-1; ++j) { - same = eq_unit(ls[diff + j], rs[j]); + same = !m.are_distinct(ls[diff + j], rs[j]); } if (same) { m_overlap_lhs.insert(pair, true); @@ -819,7 +815,7 @@ bool theory_seq::can_align_from_rhs(expr_ref_vector const& ls, expr_ref_vector c } for (unsigned i = 0; i < ls.size(); ++i) { unsigned diff = ls.size()-1-i; - if (eq_unit(ls[diff], rs[0])) { + if (!m.are_distinct(ls[diff], rs[0])) { bool same = true; if (i == 0) { m_overlap_rhs.insert(pair, true); @@ -828,7 +824,7 @@ bool theory_seq::can_align_from_rhs(expr_ref_vector const& ls, expr_ref_vector c // ls = x ++ rs' && rs = rs' ++ y, diff = |x| if (rs.size() > i) { for (unsigned j = 1; same && j <= i; ++j) { - same = eq_unit(ls[diff+j], rs[j]); + same = !m.are_distinct(ls[diff+j], rs[j]); } if (same) { m_overlap_rhs.insert(pair, true); @@ -838,7 +834,7 @@ bool theory_seq::can_align_from_rhs(expr_ref_vector const& ls, expr_ref_vector c // ls = x ++ rs ++ y, diff = |x| else { for (unsigned j = 1; same && j < rs.size(); ++j) { - same = eq_unit(ls[diff + j], rs[j]); + same = !m.are_distinct(ls[diff + j], rs[j]); } if (same) { m_overlap_rhs.insert(pair, true); diff --git a/src/smt/seq_skolem.h b/src/smt/seq_skolem.h index 18ad8e63da7..59809878389 100644 --- a/src/smt/seq_skolem.h +++ b/src/smt/seq_skolem.h @@ -102,12 +102,21 @@ namespace smt { bool is_skolem(symbol const& s, expr const* e) const; bool is_skolem(expr const* e) const { return seq.is_skolem(e); } + bool is_first(expr* e, expr*& u) { return is_skolem(m_seq_first, e) && (u = to_app(e)->get_arg(0), true); } + bool is_last(expr* e, expr*& u) { return is_skolem(m_seq_last, e) && (u = to_app(e)->get_arg(0), true); } bool is_unit_inv(expr* e) const { return is_skolem(symbol("seq.unit-inv"), e); } bool is_unit_inv(expr* e, expr*& u) const { return is_unit_inv(e) && (u = to_app(e)->get_arg(0), true); } bool is_tail(expr* e) const { return is_skolem(m_tail, e); } bool is_seq_first(expr* e) const { return is_skolem(m_seq_first, e); } bool is_indexof_left(expr* e) const { return is_skolem(m_indexof_left, e); } bool is_indexof_right(expr* e) const { return is_skolem(m_indexof_right, e); } + bool is_indexof_left(expr* e, expr*& x, expr*& y) const { + return is_indexof_left(e) && (x = to_app(e)->get_arg(0), y = to_app(e)->get_arg(1), true); + } + bool is_indexof_right(expr* e, expr*& x, expr*& y) const { + return is_indexof_right(e) && (x = to_app(e)->get_arg(0), y = to_app(e)->get_arg(1), true); + } + bool is_step(expr* e) const { return is_skolem(m_aut_step, e); } bool is_step(expr* e, expr*& s, expr*& idx, expr*& re, expr*& i, expr*& j, expr*& t) const; bool is_accept(expr* acc) const { return is_skolem(m_accept, acc); } diff --git a/src/smt/theory_seq.cpp b/src/smt/theory_seq.cpp index 1202f77c0a0..d7be9f5b0bb 100644 --- a/src/smt/theory_seq.cpp +++ b/src/smt/theory_seq.cpp @@ -2213,6 +2213,41 @@ expr_ref theory_seq::elim_skolem(expr* e) { todo.pop_back(); continue; } + if (m_sk.is_first(a, x) && cache.contains(x)) { + x = cache[x]; + result = m_util.str.mk_substr(x, m_autil.mk_int(0), m_autil.mk_sub(m_util.str.mk_length(x), m_autil.mk_int(1))); + trail.push_back(result); + cache.insert(a, result); + todo.pop_back(); + continue; + } + if (m_sk.is_last(a, x) && cache.contains(x)) { + x = cache[x]; + result = m_util.str.mk_nth(x, m_autil.mk_sub(m_util.str.mk_length(x), m_autil.mk_int(1))); + trail.push_back(result); + cache.insert(a, result); + todo.pop_back(); + continue; + } + if (m_sk.is_indexof_left(a, x, y) && cache.contains(x) && cache.contains(y)) { + x = cache[x]; + y = cache[y]; + result = m_util.str.mk_substr(x, m_autil.mk_int(0), m_util.str.mk_index(x, y, m_autil.mk_int(0))); + trail.push_back(result); + cache.insert(a, result); + todo.pop_back(); + continue; + } + if (m_sk.is_indexof_right(a, x, y) && cache.contains(x) && cache.contains(y)) { + x = cache[x]; + y = cache[y]; + expr_ref offset(m_autil.mk_add(m_util.str.mk_length(y), m_util.str.mk_index(x, y, m_autil.mk_int(0))), m); + result = m_util.str.mk_substr(x, offset, m_util.str.mk_length(x)); + trail.push_back(result); + cache.insert(a, result); + todo.pop_back(); + continue; + } args.reset(); for (expr* arg : *to_app(a)) { @@ -2282,6 +2317,7 @@ void theory_seq::validate_assign_eq(enode* a, enode* b, enode_pair_vector const& void theory_seq::validate_fmls(enode_pair_vector const& eqs, literal_vector const& lits, expr_ref_vector& fmls) { smt_params fp; fp.m_seq_validate = false; + fp.m_max_conflicts = 100; expr_ref fml(m); kernel k(m, fp); for (literal lit : lits) { @@ -2292,6 +2328,7 @@ void theory_seq::validate_fmls(enode_pair_vector const& eqs, literal_vector cons fmls.push_back(m.mk_eq(p.first->get_owner(), p.second->get_owner())); } TRACE("seq", tout << fmls << "\n";); + for (unsigned i = 0; i < fmls.size(); ++i) { fml = elim_skolem(fmls.get(i)); fmls[i] = fml; @@ -2301,7 +2338,7 @@ void theory_seq::validate_fmls(enode_pair_vector const& eqs, literal_vector cons k.assert_expr(f); } lbool r = k.check(); - if (r != l_false && !m.limit().is_canceled()) { + if (r == l_true) { model_ref mdl; k.get_model(mdl); IF_VERBOSE(0, diff --git a/src/smt/theory_seq.h b/src/smt/theory_seq.h index 48220959688..ac5f52ac19a 100644 --- a/src/smt/theory_seq.h +++ b/src/smt/theory_seq.h @@ -451,7 +451,6 @@ namespace smt { void branch_unit_variable(dependency* dep, expr* X, expr_ref_vector const& units); bool branch_variable_eq(eq const& e); bool branch_binary_variable(eq const& e); - bool eq_unit(expr* l, expr* r) const; bool can_align_from_lhs(expr_ref_vector const& ls, expr_ref_vector const& rs); bool can_align_from_rhs(expr_ref_vector const& ls, expr_ref_vector const& rs); bool branch_ternary_variable_rhs(eq const& e);