From 52032b9ef8a60b352027a05947c77d713bafb2d2 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Tue, 12 Oct 2021 10:16:15 -0700 Subject: [PATCH] #5467 --- src/ast/rewriter/seq_axioms.cpp | 6 +++--- src/ast/rewriter/seq_eq_solver.cpp | 9 ++++++--- src/ast/rewriter/seq_skolem.cpp | 4 ++-- src/ast/rewriter/seq_skolem.h | 6 ++++-- src/smt/seq_eq_solver.cpp | 5 +++-- src/smt/smt_conflict_resolution.cpp | 4 +++- src/smt/smt_context_pp.cpp | 12 ++++++++++-- src/smt/smt_internalizer.cpp | 2 +- src/smt/theory_seq.cpp | 11 ++++++----- 9 files changed, 38 insertions(+), 21 deletions(-) diff --git a/src/ast/rewriter/seq_axioms.cpp b/src/ast/rewriter/seq_axioms.cpp index 14e6290c6d6..55754102789 100644 --- a/src/ast/rewriter/seq_axioms.cpp +++ b/src/ast/rewriter/seq_axioms.cpp @@ -1142,8 +1142,8 @@ namespace seq { /** ~contains(a, b) => ~prefix(b, a) - ~contains(a, b) => ~contains(tail(a), b) or a = empty - ~contains(a, b) & a = empty => b != empty + ~contains(a, b) => ~contains(tail(a), b) + a = empty => tail(a) = empty ~(a = empty) => a = head + tail */ void axioms::unroll_not_contains(expr* e) { @@ -1165,7 +1165,7 @@ namespace seq { expr_ref bound_tracker = m_sk.mk_length_limit(s, k); expr* s0 = nullptr; if (seq.str.is_stoi(s, s0)) - s = s0; + s = s0; add_clause(~bound_tracker, mk_le(mk_len(s), k)); return bound_tracker; } diff --git a/src/ast/rewriter/seq_eq_solver.cpp b/src/ast/rewriter/seq_eq_solver.cpp index e293743f845..ca96512f007 100644 --- a/src/ast/rewriter/seq_eq_solver.cpp +++ b/src/ast/rewriter/seq_eq_solver.cpp @@ -15,6 +15,7 @@ Module Name: --*/ +#include "ast/ast_pp.h" #include "ast/rewriter/seq_eq_solver.h" #include "ast/bv_decl_plugin.h" @@ -675,7 +676,7 @@ namespace seq { if (rs.size() > i) { unsigned diff = rs.size() - (i + 1); for (unsigned j = 0; same && j < i; ++j) - same = !m.are_distinct(ls[j], rs[diff + j]); + same = !m.are_distinct(ls[j], rs[diff + j]); } // ls = x ++ rs ++ y, diff = |x| else { @@ -704,8 +705,9 @@ namespace seq { bool same = true; // ls = x ++ rs' && rs = rs' ++ y, diff = |x| if (rs.size() > i) { - for (unsigned j = 1; same && j <= i; ++j) - same = !m.are_distinct(ls[diff + j], rs[j]); + for (unsigned j = 1; same && j <= i; ++j) { + same = !m.are_distinct(ls[diff + j], rs[j]); + } } // ls = x ++ rs ++ y, diff = |x| else { @@ -715,6 +717,7 @@ namespace seq { if (same) return true; } + return false; } diff --git a/src/ast/rewriter/seq_skolem.cpp b/src/ast/rewriter/seq_skolem.cpp index ecefe8374be..90b33c24e3c 100644 --- a/src/ast/rewriter/seq_skolem.cpp +++ b/src/ast/rewriter/seq_skolem.cpp @@ -28,8 +28,8 @@ skolem::skolem(ast_manager& m, th_rewriter& rw): m_tail = "seq.tail"; m_seq_first = "seq.first"; m_seq_last = "seq.last"; - m_indexof_left = "seq.idx.left"; - m_indexof_right = "seq.idx.right"; + m_indexof_left = "seq.idx.l"; + m_indexof_right = "seq.idx.r"; m_aut_step = "aut.step"; m_pre = "seq.pre"; // (seq.pre s l): prefix of string s of length l m_post = "seq.post"; // (seq.post s l): suffix of string s of length k, based on extract starting at index i of length l diff --git a/src/ast/rewriter/seq_skolem.h b/src/ast/rewriter/seq_skolem.h index a7d4be91782..1a5928a0b5e 100644 --- a/src/ast/rewriter/seq_skolem.h +++ b/src/ast/rewriter/seq_skolem.h @@ -77,8 +77,10 @@ namespace seq { expr_ref mk_indexof_left(expr* t, expr* s, expr* offset = nullptr) { return mk(m_indexof_left, t, s, offset); } expr_ref mk_indexof_right(expr* t, expr* s, expr* offset = nullptr) { return mk(m_indexof_right, t, s, offset); } - expr_ref mk_last_indexof_left(expr* t, expr* s, expr* offset = nullptr) { return mk("seq.last_indexof_left", t, s, offset); } - expr_ref mk_last_indexof_right(expr* t, expr* s, expr* offset = nullptr) { return mk("seq.last_indexof_right", t, s, offset); } + expr_ref mk_contains_left(expr* t, expr* s, expr* offset = nullptr) { return mk("seq.cnt.l", t, s, offset); } + expr_ref mk_contains_right(expr* t, expr* s, expr* offset = nullptr) { return mk("seq.cnt.r", t, s, offset); } + expr_ref mk_last_indexof_left(expr* t, expr* s, expr* offset = nullptr) { return mk("seq.lidx.l", t, s, offset); } + expr_ref mk_last_indexof_right(expr* t, expr* s, expr* offset = nullptr) { return mk("seq.lidx.r", t, s, offset); } expr_ref mk_tail(expr* s, expr* i) { return mk(m_tail, s, i); } expr_ref mk_post(expr* s, expr* i) { return mk(m_post, s, i); } diff --git a/src/smt/seq_eq_solver.cpp b/src/smt/seq_eq_solver.cpp index a8743d21cb2..d53773f0d71 100644 --- a/src/smt/seq_eq_solver.cpp +++ b/src/smt/seq_eq_solver.cpp @@ -684,11 +684,12 @@ bool theory_seq::branch_quat_variable(depeq const& e) { cond = true; } // xs and ys cannot align - else if (!can_align_from_lhs(xs, ys) && !can_align_from_rhs(xs, ys)) + else if (!can_align_from_lhs(xs, ys) && !can_align_from_rhs(xs, ys) && !can_align_from_lhs(ys, xs) && !can_align_from_rhs(ys, xs)) cond = true; if (!cond) return false; + literal_vector lits; if (xs == ys) { @@ -724,7 +725,7 @@ bool theory_seq::branch_quat_variable(depeq const& e) { } } else { - TRACE("seq", tout << mk_pp(x1, m) << " > " << mk_pp(y1, m) << "\n";); + TRACE("seq", tout << mk_pp(x1, m) << " >\n" << mk_pp(y1, m) << "\n";); if (ctx.get_assignment(lit3) == l_undef) { ctx.mark_as_relevant(lit3); return true; diff --git a/src/smt/smt_conflict_resolution.cpp b/src/smt/smt_conflict_resolution.cpp index 4392b8a1f84..45ff1900d95 100644 --- a/src/smt/smt_conflict_resolution.cpp +++ b/src/smt/smt_conflict_resolution.cpp @@ -474,7 +474,8 @@ namespace smt { TRACE("conflict", tout << "new scope level: " << m_new_scope_lvl << "\n"; - tout << "intern. scope level: " << m_lemma_iscope_lvl << "\n";); + tout << "intern. scope level: " << m_lemma_iscope_lvl << "\n"; + tout << "lemma: " << m_lemma << "\n";); if (m.proofs_enabled()) mk_conflict_proof(conflict, not_l); @@ -761,6 +762,7 @@ namespace smt { m_lemma .shrink(j); m_lemma_atoms.shrink(j); m_ctx.m_stats.m_num_minimized_lits += sz - j; + TRACE("conflict", tout << "lemma: " << m_lemma << "\n";); } /** diff --git a/src/smt/smt_context_pp.cpp b/src/smt/smt_context_pp.cpp index 3f826c2d145..69c77346051 100644 --- a/src/smt/smt_context_pp.cpp +++ b/src/smt/smt_context_pp.cpp @@ -113,9 +113,17 @@ namespace smt { } std::ostream& context::display_literals_smt2(std::ostream& out, unsigned num_lits, literal const* lits) const { - for (unsigned i = 0; i < num_lits; ++i) { + out << literal_vector(num_lits, lits) << ":\n"; +#if 1 + expr_ref_vector fmls(m); + for (unsigned i = 0; i < num_lits; ++i) + fmls.push_back(literal2expr(lits[i])); + expr_ref c = mk_or(fmls); + out << c << "\n"; +#else + for (unsigned i = 0; i < num_lits; ++i) display_literal_smt2(out, lits[i]) << "\n"; - } +#endif return out; } diff --git a/src/smt/smt_internalizer.cpp b/src/smt/smt_internalizer.cpp index 4a4aed0f448..77b3f14d598 100644 --- a/src/smt/smt_internalizer.cpp +++ b/src/smt/smt_internalizer.cpp @@ -1387,7 +1387,7 @@ namespace smt { default: break; } - TRACE("mk_clause", display_literals_verbose(tout << "after simplification:\n", num_lits, lits) << "\n";); + TRACE("mk_clause", display_literals_verbose(tout << "after simplification: " << literal_vector(num_lits, lits) << "\n", num_lits, lits) << "\n";); unsigned activity = 1; bool lemma = is_lemma(k); diff --git a/src/smt/theory_seq.cpp b/src/smt/theory_seq.cpp index b48d0d29fbd..70f7baecd6e 100644 --- a/src/smt/theory_seq.cpp +++ b/src/smt/theory_seq.cpp @@ -726,7 +726,7 @@ void theory_seq::linearize(dependency* dep, enode_pair_vector& eqs, literal_vect svector assumptions; const_cast(m_dm).linearize(dep, assumptions); for (assumption const& a : assumptions) { - if (a.lit != null_literal) { + if (a.lit != null_literal && a.lit != true_literal) { lits.push_back(a.lit); SASSERT(ctx.get_assignment(a.lit) == l_true); } @@ -743,7 +743,7 @@ bool theory_seq::propagate_lit(dependency* dep, unsigned n, literal const* _lits return false; if (ctx.get_assignment(lit) == l_true) return false; - + literal_vector lits(n, _lits); if (lit == false_literal) { @@ -2858,7 +2858,7 @@ void theory_seq::add_axiom(literal l1, literal l2, literal l3, literal l4, liter } void theory_seq::add_axiom(literal_vector & lits) { - TRACE("seq", ctx.display_literals_verbose(tout << "assert:", lits) << "\n";); + TRACE("seq", ctx.display_literals_verbose(tout << "assert " << lits << " :", lits) << "\n";); for (literal lit : lits) ctx.mark_as_relevant(lit); @@ -2898,6 +2898,7 @@ bool theory_seq::propagate_eq(dependency* deps, literal_vector const& _lits, exp if (n1->get_root() == n2->get_root()) { return false; } + ctx.mark_as_relevant(n1); ctx.mark_as_relevant(n2); @@ -2979,8 +2980,8 @@ void theory_seq::assign_eh(bool_var v, bool is_true) { m_rewrite(se1); m_rewrite(se2); if (is_true) { - expr_ref f1 = m_sk.mk_indexof_left(se1, se2); - expr_ref f2 = m_sk.mk_indexof_right(se1, se2); + expr_ref f1 = m_sk.mk_contains_left(se1, se2); + expr_ref f2 = m_sk.mk_contains_right(se1, se2); f = mk_concat(f1, se2, f2); propagate_eq(lit, f, e1, true); propagate_eq(lit, mk_len(f), mk_len(e1), false);