From f30650b4b4910eda1333e36ccb160ecdcc6860f6 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Fri, 3 Jul 2026 11:21:38 -0700 Subject: [PATCH] bug fix Signed-off-by: Nikolaj Bjorner --- src/ast/rewriter/seq_split.cpp | 4 +- src/smt/seq_regex.cpp | 82 +++++++++++++++++++++++++++++++++- src/smt/seq_regex.h | 47 ++++++++++--------- 3 files changed, 108 insertions(+), 25 deletions(-) diff --git a/src/ast/rewriter/seq_split.cpp b/src/ast/rewriter/seq_split.cpp index df97e43aa8..d8963ce838 100644 --- a/src/ast/rewriter/seq_split.cpp +++ b/src/ast/rewriter/seq_split.cpp @@ -376,8 +376,8 @@ struct split_set::iterator::imp { } else if (seq.str.is_unit(a, b)) { auto eps = mk_eps(); - push_split(eps, a); - push_split(a, eps); + push_split(eps, r); + push_split(r, eps); } else if (seq.str.is_string(a, str)) { for (unsigned i = 0; i <= str.length(); ++i) { diff --git a/src/smt/seq_regex.cpp b/src/smt/seq_regex.cpp index 497000d461..d9844b31a0 100644 --- a/src/smt/seq_regex.cpp +++ b/src/smt/seq_regex.cpp @@ -26,6 +26,83 @@ Author: namespace smt { + seq_regex::split_cont::split_cont(seq_regex &sr, split_set &&ss, literal lit, expr *u, expr *v, expr *r) + : m_regex(sr), m_u(u), m_v(v), m_split(std::move(ss)), m_it(m_split.begin()), m_end(m_split.end()), + m_in_re2(sr.m), m_lit(lit) {} + + bool seq_regex::split_cont::failed() const { + return m_split.failed(); + } + bool seq_regex::split_cont::next_split() { + if (m_split.failed()) + return false; + auto &ctx = m_regex.ctx; + auto &re = m_regex.re(); + auto &m = m_regex.m; + literal lit_undef = null_literal; + for (auto e : m_in_re2) { + auto lit = m_regex.th.mk_literal(e); + auto rel = ctx.is_relevant(lit); + switch (ctx.get_assignment(lit)) { + case l_undef: + lit_undef = lit; + break; + case l_true: + if (!rel) + ctx.mark_as_relevant(lit); + return rel; + case l_false: + break; + } + if (lit_undef != null_literal) + break; + } + + if (lit_undef == null_literal) { + while (m_it != m_end) { + auto [pre, post] = *m_it; + auto a = re.mk_in_re(m_u, pre); + auto b = re.mk_in_re(m_v, post); + auto e = m.mk_and(a, b); + m_in_re2.push_back(e); + auto lit = m_regex.th.mk_literal(e); + auto rel = ctx.is_relevant(lit); + switch (ctx.get_assignment(lit)) { + case l_undef: lit_undef = lit; break; + case l_true: + if (!rel) + ctx.mark_as_relevant(lit); + return rel; + case l_false: break; + } + ++m_it; + if (lit_undef != null_literal) + break; + } + } + + if (m_split.failed()) + return false; + + if (lit_undef != null_literal) { + ctx.mark_as_relevant(lit_undef); + ctx.force_phase(lit_undef); + return true; + } + // all literals are false: + enode_pair_vector eqs; + literal_vector lits; + lits.push_back(m_lit); + for (auto e : m_in_re2) { + auto lit = m_regex.th.mk_literal(e); + SASSERT(ctx.get_assignment(lit) == l_false); + lits.push_back(~lit); + } + m_regex.th.set_conflict(eqs, lits); + return true; + } + + seq_regex::seq_regex(theory_seq& th): th(th), ctx(th.get_context()), @@ -368,6 +445,8 @@ namespace smt { } bool seq_regex::factor_membership(literal lit) { + if (!th.get_fparams().m_seq_regex_factorization_enabled) + return false; expr *s = nullptr, *r = nullptr; expr *e = ctx.bool_var2expr(lit.var()); VERIFY(str().is_in_re(e, s, r)); @@ -385,8 +464,7 @@ namespace smt { // Final check also unfolds this axiomatization // (we have to add a final check to seq_regex for this). - if (!th.get_fparams().m_seq_regex_factorization_enabled) - return false; + unsigned threshold = th.get_fparams().m_seq_regex_factorization_threshold; expr_ref_vector prefix(m); diff --git a/src/smt/seq_regex.h b/src/smt/seq_regex.h index 376c19a50d..2cb4db4d4c 100644 --- a/src/smt/seq_regex.h +++ b/src/smt/seq_regex.h @@ -94,27 +94,6 @@ namespace smt { class theory_seq; class seq_regex; - // a split continuation is a closure that contains a split set - // and in_re2 literals that were extracted from a partial split. - // there are the following outcomes: - // 1. it was not possible to split:failed() - // 2. one of the in_re2 literals is true: in_re2(u, r1, v, r2) and in_re(u, r1), in_re(v, r2) are true - // 3. one of in_re2(u, r1, v, r2) is true: but in_re(u, r1) or in_re(v, r2) is undef or false. - // 4. all in_re2(u, r1, v, r2) are false: there is a next split from m_split -> add propagation axioms and set phase of in_re2. - // 5. all in_re2(u, r1, v, r2) are false: there is no next split from m_split -> conflict - // split continuations are assigned at scope level and map propagation literal lit to a split continuation. - // they are checked during propagation and during final check. - class split_cont { - split_set m_split; - expr_ref_vector m_in_re2; - public: - split_cont(seq_regex &r, literal lit); - bool failed() const; - bool is_sat(); - bool is_unsat(); - literal next_split(); - }; - class seq_regex { // Data about a constraint of the form (str.in_re s R) struct s_in_re { @@ -126,6 +105,32 @@ namespace smt { m_lit(l), m_s(s), m_re(r), m_active(true) {} }; + // a split continuation is a closure that contains a split set + // and in_re2 literals that were extracted from a partial split. + // there are the following outcomes: + // 1. it was not possible to split:failed() + // 2. one of the in_re2 literals is true: in_re2(u, r1, v, r2) and in_re(u, r1), in_re(v, r2) are true + // 3. one of in_re2(u, r1, v, r2) is true: but in_re(u, r1) or in_re(v, r2) is undef or false. + // 4. all in_re2(u, r1, v, r2) are false: there is a next split from m_split -> add propagation axioms and set + // phase of in_re2. + // 5. all in_re2(u, r1, v, r2) are false: there is no next split from m_split -> conflict + // split continuations are assigned at scope level and map propagation literal lit to a split continuation. + // they are checked during propagation and during final check. + class split_cont { + seq_regex &m_regex; + split_set m_split; + expr *m_u, *m_v, *m_r; + split_set::iterator m_it; + split_set::iterator m_end; + expr_ref_vector m_in_re2; + literal m_lit; + + public: + split_cont(seq_regex &sr, split_set&& ss, literal lit, expr* u, expr* v, expr* r); + bool failed() const; + bool next_split(); + }; + theory_seq& th; context& ctx; ast_manager& m;