From 71f30149572f6ad0c0f4173163564dcd580f22b3 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Fri, 3 Jul 2026 23:58:13 -0700 Subject: [PATCH] na Signed-off-by: Nikolaj Bjorner --- src/ast/rewriter/seq_split.cpp | 2 - src/smt/seq_regex.cpp | 83 +++++++++++++++++++++++++--------- src/smt/seq_regex.h | 21 +++------ 3 files changed, 69 insertions(+), 37 deletions(-) diff --git a/src/ast/rewriter/seq_split.cpp b/src/ast/rewriter/seq_split.cpp index eba15111c9..be320cb74d 100644 --- a/src/ast/rewriter/seq_split.cpp +++ b/src/ast/rewriter/seq_split.cpp @@ -210,9 +210,7 @@ struct split_set::iterator::imp { } void consume() override { - TRACE(seq, tout << "concat-start: " << mk_pp(a, parent().i.m) << " " << mk_pp(b, parent().i.m) << "\n"); while (!parent().has_split() && !at_end() && !a_it.failed() && !b_it.failed()) { - TRACE(seq, tout << "concat: " << mk_pp(a, parent().i.m) << " " << mk_pp(b, parent().i.m) << "\n"); if (a_it == a_end) { auto [p, q] = *b_it; parent().push_split(parent().i.rw.mk_re_append(a, p), q); diff --git a/src/smt/seq_regex.cpp b/src/smt/seq_regex.cpp index e466e56178..289ca5e0f8 100644 --- a/src/smt/seq_regex.cpp +++ b/src/smt/seq_regex.cpp @@ -172,39 +172,22 @@ namespace smt { VERIFY(str().is_in_re(e, s, r)); TRACE(seq_regex, tout << "propagate in RE: " << lit.sign() << " " << mk_pp(e, m) << std::endl;); - STRACE(seq_regex_brief, tout << "PIR(" << mk_pp(s, m) << "," - << state_str(r) << ") ";); - // convert negative negative membership literals to positive - // ~(s in R) => s in C(R) - if (lit.sign()) { - expr_ref fml(re().mk_in_re(s, re().mk_complement(r)), m); - rewrite(fml); - literal nlit = th.mk_literal(fml); - if (lit == nlit) { - // is-nullable doesn't simplify for regexes with uninterpreted subterms - th.add_unhandled_expr(fml); - } - th.propagate_lit(nullptr, 1, &lit, nlit); + if (unfold_complement(lit, s, r)) return; - } if (unfold_prefix(lit, s, r)) { - TRACE(seq_regex, tout << "unfolded prefix" << std::endl;); - STRACE(seq_regex_brief, tout << "unfold_prefix ";); + TRACE(seq_regex, tout << "unfolded prefix\n"); return; } if (is_string_equality(lit, s, r)) { - TRACE(seq_regex, tout - << "simplified regex using string equality" << std::endl;); - STRACE(seq_regex_brief, tout << "string_eq ";); + TRACE(seq_regex, tout << "simplified regex using string equality\n"); return; } if (factor_ite(lit, s, r)) { - TRACE(seq_regex, tout << "factored ite in regex" << std::endl;); - STRACE(seq_regex_brief, tout << "factor_ite ";); + TRACE(seq_regex, tout << "factored ite in regex\n"); return; } @@ -502,6 +485,64 @@ namespace smt { return false; } + bool seq_regex::final_check() { + + return true; + + // sketch: + // + // check registered seq_cont if more case splits are needed. + // check registered atomic regex membership for membership + // fallback to initialize_accept? + + expr *x = nullptr, *r = nullptr; + bool done = true; + for (auto s : m_split_conts) { + if (s->failed()) + ; + else if (s->next_split()) + done = false; + else if (s->failed()) { + done = false; + + expr *e = ctx.bool_var2expr(s->lit().var()); + VERIFY(str().is_in_re(e, x, r)); + initialize_accept(s->lit(), x, r); + } + else + ; // some split literal is true + } + obj_map> var2regex; + for (auto lit : m_atomic_memberships) { + expr *e = ctx.bool_var2expr(lit.var()); + VERIFY(str().is_in_re(e, x, r)); + var2regex.insert_if_not_there(x, ptr_vector()).push_back(r); + } + for (auto const &[x, regexes] : var2regex) { + // synthesize a solution within intersection of regexes. + // if intersection is empty, report conflict. + // add guardrails for solution satisfying current length assignment to x + // if solution does not satisfy length constraints initialize_accept instead of retaining atomic + + } + return done; + } + + bool seq_regex::unfold_complement(literal lit, expr *s, expr *r) { + if (!lit.sign()) + return false; + // convert negative negative membership literals to positive + // ~(s in R) => s in C(R) + expr_ref fml(re().mk_in_re(s, re().mk_complement(r)), m); + rewrite(fml); + literal nlit = th.mk_literal(fml); + if (lit == nlit) { + // is-nullable doesn't simplify for regexes with uninterpreted subterms + th.add_unhandled_expr(fml); + } + th.propagate_lit(nullptr, 1, &lit, nlit); + return true; + } bool seq_regex::factor_ite(literal lit, expr* s, expr* r) { bool_rewriter br(m); diff --git a/src/smt/seq_regex.h b/src/smt/seq_regex.h index 914a21d0a3..43320fab7c 100644 --- a/src/smt/seq_regex.h +++ b/src/smt/seq_regex.h @@ -95,17 +95,8 @@ namespace smt { class seq_regex; class seq_regex { - // Data about a constraint of the form (str.in_re s R) - struct s_in_re { - literal m_lit; - expr* m_s; - expr* m_re; - bool m_active; - s_in_re(literal l, expr* s, expr* r): - m_lit(l), m_s(s), m_re(r), m_active(true) {} - }; - // a split continuation is a closure that contains a split set + // 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() @@ -129,13 +120,15 @@ namespace smt { split_cont(seq_regex &sr, split_set&& ss, literal lit, expr* u, expr* v, expr* r); bool failed() const; bool next_split(); + literal lit() const { return m_lit; } }; theory_seq& th; context& ctx; ast_manager& m; - vector m_s_in_re; + ptr_vector m_split_conts; // split continuations + literal_vector m_atomic_memberships; // str.in_re X r, where X is a variable /* state_graph for dead state detection, and associated methods */ @@ -179,6 +172,8 @@ namespace smt { bool unfold_prefix(literal lit, expr* s, expr* r); + bool unfold_complement(literal lit, expr *s, expr *r); + bool factor_membership(literal lit, expr* s, expr* r); bool factor_ite(literal lit, expr* s, expr* r); @@ -227,9 +222,7 @@ namespace smt { seq_regex(theory_seq& th); - bool final_check() { - return true; - } + bool final_check(); void propagate_in_re(literal lit);