From dbdccbff975b6d314cfbe83ce46e01c6279beb24 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Mon, 23 Mar 2026 13:18:34 -0700 Subject: [PATCH] use recursive function for not-contains Signed-off-by: Nikolaj Bjorner --- src/ast/rewriter/seq_axioms.cpp | 18 ++++++++++------ src/ast/rewriter/seq_rewriter.cpp | 34 +++++++++++++++++++++++-------- src/smt/seq_model.cpp | 3 +-- src/smt/theory_nseq.cpp | 2 +- 4 files changed, 40 insertions(+), 17 deletions(-) diff --git a/src/ast/rewriter/seq_axioms.cpp b/src/ast/rewriter/seq_axioms.cpp index 510282938..40e28c42a 100644 --- a/src/ast/rewriter/seq_axioms.cpp +++ b/src/ast/rewriter/seq_axioms.cpp @@ -268,14 +268,20 @@ namespace seq { m_sk.decompose(s, head, tail); TRACE(seq, tout << "tail " << mk_bounded_pp(e, m, 2) << " " << mk_bounded_pp(s, m, 2) << "\n";); expr_ref emp = mk_eq_empty(s); - add_clause(emp, mk_seq_eq(s, mk_concat(head, e))); + expr_ref con = mk_concat(head, e); + if (m_mark_no_diseq) + m_mark_no_diseq(con); + add_clause(emp, mk_seq_eq(s, con)); add_clause(~emp, mk_eq_empty(e)); } void axioms::drop_last_axiom(expr* e, expr* s) { TRACE(seq, tout << "drop last " << mk_bounded_pp(e, m, 2) << " " << mk_bounded_pp(s, m, 2) << "\n";); expr_ref emp = mk_eq_empty(s); - add_clause(emp, mk_seq_eq(s, mk_concat(e, seq.str.mk_unit(m_sk.mk_last(s))))); + expr_ref con = mk_concat(e, seq.str.mk_unit(m_sk.mk_last(s))); + if (m_mark_no_diseq) + m_mark_no_diseq(con); + add_clause(emp, mk_seq_eq(s, con)); add_clause(~emp, mk_eq_empty(e)); } @@ -1364,12 +1370,12 @@ namespace seq { var_ref vp(m.mk_var(0, srt), m); expr_ref len_s(seq.str.mk_length(vs), m); expr_ref len_p(seq.str.mk_length(vp), m); -// expr_ref tail_s(seq.str.mk_substr(vs, a.mk_int(1), a.mk_sub(len_s, a.mk_int(1))), m); - expr_ref tail_s(m_sk.mk("tail.s", vs), m); - expr* nc_args[2] = { tail_s.get(), vp.get() }; + expr_ref head(m), tail(m); + m_sk.decompose(vs, head, tail); + expr* nc_args[2] = { tail.get(), vp.get() }; expr_ref pref(seq.str.mk_prefix(vp, vs), m); expr_ref hd(seq.str.mk_unit(seq.str.mk_nth_i(vs, a.mk_int(0))), m); - expr_ref decomp(m.mk_eq(vs, seq.str.mk_concat(hd, tail_s)), m); + expr_ref decomp(m.mk_eq(vs, seq.str.mk_concat(hd, tail)), m); expr_ref else_branch(m.mk_and(m.mk_not(pref), m.mk_and(decomp, m.mk_app(m_not_contains.get(), 2, nc_args))), m); expr_ref body(m.mk_ite(a.mk_gt(len_p, len_s), m.mk_true(), diff --git a/src/ast/rewriter/seq_rewriter.cpp b/src/ast/rewriter/seq_rewriter.cpp index e0b86d50c..787c55e6f 100644 --- a/src/ast/rewriter/seq_rewriter.cpp +++ b/src/ast/rewriter/seq_rewriter.cpp @@ -3149,9 +3149,14 @@ expr_ref seq_rewriter::mk_antimirov_deriv_intersection(expr* e, expr* d1, expr* result = mk_antimirov_deriv_intersection(e, b, d2, path); else if (m().is_false(path_and_notc)) result = mk_antimirov_deriv_intersection(e, a, d2, path); - else - result = m().mk_ite(c, mk_antimirov_deriv_intersection(e, a, d2, path_and_c), - mk_antimirov_deriv_intersection(e, b, d2, path_and_notc)); + else { + expr_ref th(mk_antimirov_deriv_intersection(e, a, d2, path_and_c), m()); + expr_ref el(mk_antimirov_deriv_intersection(e, b, d2, path_and_notc), m()); + if (th == el) + result = th; + else + result = m().mk_ite(c, th, el); + } } else if (m().is_ite(d2)) // swap d1 and d2 @@ -3207,8 +3212,14 @@ expr_ref seq_rewriter::mk_antimirov_deriv_negate(expr* elem, expr* d) { result = nothing(); else if (re().is_dot_plus(d)) result = epsilon(); - else if (m().is_ite(d, c, t, e)) - result = m().mk_ite(c, mk_antimirov_deriv_negate(elem, t), mk_antimirov_deriv_negate(elem, e)); + else if (m().is_ite(d, c, t, e)) { + expr_ref th(mk_antimirov_deriv_negate(elem, t), m()); + expr_ref el(mk_antimirov_deriv_negate(elem, e), m()); + if (th == el) + result = th; + else + result = m().mk_ite(c, th, el); + } else if (re().is_union(d, t, e)) result = mk_antimirov_deriv_intersection(elem, mk_antimirov_deriv_negate(elem, t), mk_antimirov_deriv_negate(elem, e), m().mk_true()); else if (re().is_intersection(d, t, e)) @@ -3226,9 +3237,15 @@ expr_ref seq_rewriter::mk_antimirov_deriv_union(expr* d1, expr* d2) { VERIFY(m_util.is_seq(seq_sort, ele_sort)); expr_ref result(m()); expr* c1, * t1, * e1, * c2, * t2, * e2; - if (m().is_ite(d1, c1, t1, e1) && m().is_ite(d2, c2, t2, e2) && c1 == c2) - // eliminate duplicate branching on exactly the same condition - result = m().mk_ite(c1, mk_antimirov_deriv_union(t1, t2), mk_antimirov_deriv_union(e1, e2)); + if (m().is_ite(d1, c1, t1, e1) && m().is_ite(d2, c2, t2, e2) && c1 == c2) { + expr_ref th(mk_antimirov_deriv_union(t1, t2), m()); + expr_ref el(mk_antimirov_deriv_union(e1, e2), m()); + if (th == el) + result = th; + else + // eliminate duplicate branching on exactly the same condition + result = m().mk_ite(c1, th, el); + } else result = mk_regex_union_normalize(d1, d2); return result; @@ -6066,6 +6083,7 @@ lbool seq_rewriter::some_string_in_re(expr_mark& visited, expr* r, unsigned_vect re_eval_pos current = todo.back(); todo.pop_back(); r = current.e; + // IF_VERBOSE(1, verbose_stream() << "derive " << mk_pp(r, m()) << "\n"); str.resize(current.str_len); if (current.needs_derivation) { SASSERT(current.exclude.empty()); diff --git a/src/smt/seq_model.cpp b/src/smt/seq_model.cpp index 20eb2ddbf..724ac360d 100644 --- a/src/smt/seq_model.cpp +++ b/src/smt/seq_model.cpp @@ -308,12 +308,11 @@ namespace smt { // We checked non-emptiness during Nielsen already lbool wr = m_rewriter.some_seq_in_re(re_expr, witness); if (wr == l_true && witness) { - // std::cout << "Witness for " << mk_pp(var->get_expr(), m) << " in " << - // mk_pp(re_expr, m) << ": " << mk_pp(witness, m) << std::endl; m_trail.push_back(witness); m_factory->register_value(witness); return witness; } + IF_VERBOSE(1, verbose_stream() << "witness extraction failed: " << wr << "\n" << mk_pp(re_expr, m) << "\n"); UNREACHABLE(); } diff --git a/src/smt/theory_nseq.cpp b/src/smt/theory_nseq.cpp index c73eec720..d09842ab7 100644 --- a/src/smt/theory_nseq.cpp +++ b/src/smt/theory_nseq.cpp @@ -246,7 +246,7 @@ namespace smt { if (is_true) m_axioms.contains_true_axiom(e); else - m_axioms.unroll_not_contains(e); + m_axioms.not_contains_axiom(e); } else if (m_seq.str.is_lt(e) || m_seq.str.is_le(e)) { // axioms added via relevant_eh → dequeue_axiom