From 661bb130397b8d26fb558f17a1ea0cbb8eec38f6 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Wed, 15 Jul 2026 11:29:20 -0700 Subject: [PATCH 1/6] change relevancy marking to top-level on inconsistent states Signed-off-by: Nikolaj Bjorner --- src/smt/smt_context.h | 9 +++++---- 1 file changed, 5 insertions(+), 4 deletions(-) diff --git a/src/smt/smt_context.h b/src/smt/smt_context.h index 7938c70742..9664dd73ea 100644 --- a/src/smt/smt_context.h +++ b/src/smt/smt_context.h @@ -1779,15 +1779,16 @@ namespace smt { void internalize_proxies(expr_ref_vector const& asms, vector>& asm2proxy); void internalize_instance(expr * body, proof * pr, unsigned generation) { + if (inconsistent()) + return; internalize_assertion(body, pr, generation); if (relevancy()) { // if the instantiation creates a conflict, we backtrack immediately. // to retain the conflict clause being relevant we mark it here. // if the instantiation does not create a conflict, default relevancy propagation applies. - if (inconsistent() && is_app(body)) { - for (auto arg : *to_app(body)) - mark_as_relevant(arg); - } + if (inconsistent()) + mark_as_relevant(body); + m_case_split_queue->internalize_instance_eh(body, generation); } } From 9fb2b491d6f5108494df2e17609409bfa448b775 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Wed, 15 Jul 2026 15:17:14 -0700 Subject: [PATCH 2/6] remove relvancy marking code Signed-off-by: Nikolaj Bjorner --- src/smt/smt_context.h | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/smt/smt_context.h b/src/smt/smt_context.h index 9664dd73ea..0248c75a65 100644 --- a/src/smt/smt_context.h +++ b/src/smt/smt_context.h @@ -1786,8 +1786,8 @@ namespace smt { // if the instantiation creates a conflict, we backtrack immediately. // to retain the conflict clause being relevant we mark it here. // if the instantiation does not create a conflict, default relevancy propagation applies. - if (inconsistent()) - mark_as_relevant(body); + //if (inconsistent() && is_app(body)) + // for (auto arg: *to_app(body)) mark_as_relevant(arg); m_case_split_queue->internalize_instance_eh(body, generation); } From 2db625606d9964e1ffc4c2f7f34ee0e6939d71c1 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Wed, 15 Jul 2026 20:04:48 -0700 Subject: [PATCH 3/6] fold functionality into seq_range_collapse Signed-off-by: Nikolaj Bjorner --- src/ast/rewriter/seq_range_collapse.cpp | 104 +++++++++++++++++++++--- src/ast/seq_decl_plugin.h | 5 +- 2 files changed, 97 insertions(+), 12 deletions(-) diff --git a/src/ast/rewriter/seq_range_collapse.cpp b/src/ast/rewriter/seq_range_collapse.cpp index 8bd725cbeb..5ad71a5a96 100644 --- a/src/ast/rewriter/seq_range_collapse.cpp +++ b/src/ast/rewriter/seq_range_collapse.cpp @@ -21,6 +21,74 @@ Authors: namespace seq { + // Cofactor path condition `pred` (a Boolean over x = (:var 0)) -> the canonical + // range_predicate (union of ranges) of the characters satisfying it. Returns + // false on a construct outside {true,false,and,or,not,=,char.<=} over x. + static bool pred_to_rp(ast_manager &m, seq_util &sq, expr *x, expr *pred, + seq::range_predicate &out) { + unsigned maxc = sq.max_char(); + expr *a = nullptr, *b = nullptr; + unsigned c = 0; + if (m.is_true(pred)) { + out = seq::range_predicate::top(maxc); + return true; + } + if (m.is_false(pred)) { + out = seq::range_predicate::empty(maxc); + return true; + } + if (m.is_eq(pred, a, b)) { + if (a == x && sq.is_const_char(b, c)) { + out = seq::range_predicate::singleton(c, maxc); + return true; + } + if (b == x && sq.is_const_char(a, c)) { + out = seq::range_predicate::singleton(c, maxc); + return true; + } + return false; + } + if (sq.is_char_le(pred, a, b)) { + if (b == x && sq.is_const_char(a, c)) { + out = seq::range_predicate::range(c, maxc, maxc); + return true; + } + if (a == x && sq.is_const_char(b, c)) { + out = seq::range_predicate::range(0, c, maxc); + return true; + } + return false; + } + if (m.is_not(pred, a)) { + seq::range_predicate s(maxc); + if (!pred_to_rp(m, sq, x, a, s)) + return false; + out = ~s; + return true; + } + if (m.is_and(pred)) { + out = seq::range_predicate::top(maxc); + for (expr *arg : *to_app(pred)) { + seq::range_predicate s(maxc); + if (!pred_to_rp(m, sq, x, arg, s)) + return false; + out = out & s; + } + return true; + } + if (m.is_or(pred)) { + out = seq::range_predicate::empty(maxc); + for (expr *arg : *to_app(pred)) { + seq::range_predicate s(maxc); + if (!pred_to_rp(m, sq, x, arg, s)) + return false; + out = out | s; + } + return true; + } + return false; + } + bool regex_to_range_predicate(seq_util& u, expr* r, range_predicate& out) { // The range algebra only models sets of single characters over the // unsigned character domain [0, max_char]. Guard against any regex @@ -35,6 +103,7 @@ namespace seq { unsigned const max_char = u.max_char(); auto& re = u.re; + auto &m = u.get_manager(); if (re.is_empty(r)) { out = range_predicate::empty(max_char); @@ -72,8 +141,10 @@ namespace seq { expr *a = nullptr, *b = nullptr, *c = nullptr; if (re.is_union(r, a, b)) { range_predicate pa(max_char), pb(max_char); - if (!regex_to_range_predicate(u, a, pa)) return false; - if (!regex_to_range_predicate(u, b, pb)) return false; + if (!regex_to_range_predicate(u, a, pa)) + return false; + if (!regex_to_range_predicate(u, b, pb)) + return false; out = pa | pb; return true; } @@ -97,12 +168,22 @@ namespace seq { if (re.is_intersection(r, a, b)) { range_predicate pa(max_char), pb(max_char); - if (!regex_to_range_predicate(u, a, pa)) return false; - if (!regex_to_range_predicate(u, b, pb)) return false; + if (!regex_to_range_predicate(u, a, pa)) + return false; + if (!regex_to_range_predicate(u, b, pb)) + return false; out = pa & pb; return true; } + if (re.is_of_pred(r, a)) { + sort *char_sort = nullptr; + VERIFY(u.is_seq(seq_sort, char_sort)); + expr_ref var(m.mk_var(0, char_sort), m); + if (pred_to_rp(m, u, var, a, out)) + return true; + } + // NOTE: re.complement is intentionally NOT handled here. // re.complement is the SEQUENCE-level complement: its language @@ -130,6 +211,8 @@ namespace seq { expr_ref range_predicate_to_regex(seq_util& u, range_predicate const& p, sort* seq_sort) { ast_manager& m = u.get_manager(); sort* re_sort = u.re.mk_re(seq_sort); + sort *char_sort = nullptr; + VERIFY(u.is_seq(seq_sort, char_sort)); if (p.is_empty()) return expr_ref(u.re.mk_empty(re_sort), m); unsigned const n = p.num_ranges(); @@ -145,16 +228,15 @@ namespace seq { // when it has to combine our materialized output with another // (id-sorted) regex set. expr_ref_vector ranges(m); + expr_ref bound(m.mk_var(0, char_sort), m); + symbol char_sym("ch"); + auto &ch = u.get_char_plugin(); for (unsigned i = 0; i < n; ++i) { auto [lo, hi] = p[i]; - ranges.push_back(mk_single_range_regex(u, lo, hi, re_sort)); + ranges.push_back(m.mk_and(ch.mk_le(ch.mk_char(lo), bound), ch.mk_le(bound, ch.mk_char(hi)))); } - std::sort(ranges.data(), ranges.data() + ranges.size(), - [](expr* a, expr* b) { return a->get_id() < b->get_id(); }); - expr_ref acc(ranges.get(n - 1), m); - for (unsigned i = n - 1; i-- > 0; ) - acc = expr_ref(u.re.mk_union(ranges.get(i), acc), m); - return acc; + expr_ref body(m.mk_or(ranges), m); + return expr_ref(m.mk_lambda(1, &char_sort, &char_sym, body), m); } } diff --git a/src/ast/seq_decl_plugin.h b/src/ast/seq_decl_plugin.h index 9de2c01525..fd5696f493 100644 --- a/src/ast/seq_decl_plugin.h +++ b/src/ast/seq_decl_plugin.h @@ -228,6 +228,9 @@ public: unsigned max_mul(unsigned x, unsigned y) const; ast_manager& get_manager() const { return m; } + char_decl_plugin &get_char_plugin() const { + return ch; + } sort* mk_char_sort() const { return seq.char_sort(); } sort* mk_string_sort() const { return seq.string_sort(); } @@ -239,7 +242,7 @@ public: bool is_re(sort* s) const { return is_sort_of(s, m_fid, RE_SORT); } bool is_re(sort* s, sort*& seq) const { return is_sort_of(s, m_fid, RE_SORT) && (seq = to_sort(s->get_parameter(0).get_ast()), true); } bool is_seq(expr* e) const { return is_seq(e->get_sort()); } - bool is_seq(sort* s, sort*& seq) const { return is_seq(s) && (seq = to_sort(s->get_parameter(0).get_ast()), true); } + bool is_seq(sort* s, sort*& ch) const { return is_seq(s) && (ch = to_sort(s->get_parameter(0).get_ast()), true); } bool is_re(expr* e) const { return is_re(e->get_sort()); } bool is_re(expr* e, sort*& seq) const { return is_re(e->get_sort(), seq); } bool is_const_char(expr* e, unsigned& c) const; From 9945e3dc9a3ad35f76f96caf0db9c6701860f7a8 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Wed, 15 Jul 2026 20:44:46 -0700 Subject: [PATCH 4/6] add Margus' unfold-fold operation and consolidate range-predicate recognizer/constructor. Signed-off-by: Nikolaj Bjorner --- src/ast/rewriter/seq_range_collapse.cpp | 36 ++++++++++++++++++++++--- src/ast/rewriter/seq_range_collapse.h | 15 +++++++++++ 2 files changed, 47 insertions(+), 4 deletions(-) diff --git a/src/ast/rewriter/seq_range_collapse.cpp b/src/ast/rewriter/seq_range_collapse.cpp index 5ad71a5a96..d2af71f6b3 100644 --- a/src/ast/rewriter/seq_range_collapse.cpp +++ b/src/ast/rewriter/seq_range_collapse.cpp @@ -176,11 +176,14 @@ namespace seq { return true; } - if (re.is_of_pred(r, a)) { - sort *char_sort = nullptr; - VERIFY(u.is_seq(seq_sort, char_sort)); + if (re.is_of_pred(r, a) && is_lambda(a)) { + auto q = to_quantifier(a); + if (q->get_num_decls() != 1) + return false; + auto body = q->get_expr(); + sort *char_sort = q->get_decl_sort(0); expr_ref var(m.mk_var(0, char_sort), m); - if (pred_to_rp(m, u, var, a, out)) + if (u.get_char_plugin().get_family_id() == char_sort->get_family_id() && pred_to_rp(m, u, var, body, out)) return true; } @@ -239,4 +242,29 @@ namespace seq { return expr_ref(m.mk_lambda(1, &char_sort, &char_sym, body), m); } + expr_ref unfold_fold(seq_rewriter &rw, expr *r) { + auto &m = rw.m(); + auto& u = rw.u(); + expr_ref_pair_vector cofactors(m); + rw.brz_derivative_cofactors(r, cofactors); + if (cofactors.empty()) + return expr_ref(u.re.mk_empty(r->get_sort()), m); + + sort *seq_sort = nullptr, *char_sort = nullptr; + VERIFY(u.is_re(r, seq_sort)); + VERIFY(u.is_seq(seq_sort, char_sort)); + expr_ref var(m.mk_var(0, char_sort), m); + expr_ref result(m); + symbol ch("ch"); + for (auto const &[c, cof] : cofactors) { + auto prefix = u.re.mk_of_pred(m.mk_lambda(1, &char_sort, &ch, c)); + auto term = u.re.mk_concat(prefix, cof); + if (result) + result = u.re.mk_union(term, result); + else + result = term; + } + return result; + } + } diff --git a/src/ast/rewriter/seq_range_collapse.h b/src/ast/rewriter/seq_range_collapse.h index 16cd5fd67b..f6effc8ee4 100644 --- a/src/ast/rewriter/seq_range_collapse.h +++ b/src/ast/rewriter/seq_range_collapse.h @@ -26,6 +26,7 @@ Authors: #pragma once #include "ast/rewriter/seq_range_predicate.h" +#include "ast/rewriter/seq_rewriter.h" #include "ast/seq_decl_plugin.h" namespace seq { @@ -68,4 +69,18 @@ namespace seq { */ expr_ref range_predicate_to_regex(seq_util& u, range_predicate const& p, sort* seq_sort); + /** + * Unfolds and then folds the given regex expression. + * Unfolding, produces the symbolic derivative which is an expression with a free variable var 0 + * of the character sort. + * Folding produces a regex expression that is equivalent to the original one. + * It is obtained by taking the cofactors of the unfold, and producing a range predicate + * from the conditions with var 0. + * Formally: + * cofactors F_i[var 0], r_i <- unfold(r) + * of_pred(\lambda ch . F_i[ch]) . r_i <- fold(F_i[var 0], r_i) + * union_i of_pred(\ ch. F_i[ch]) . r_i <- fold(unfold(r)) + */ + expr_ref unfold_fold(seq_rewriter &rw, expr *r); + } From 09ffec52e8f7b10e0469d9599c4640bc5e550d11 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Wed, 15 Jul 2026 20:54:23 -0700 Subject: [PATCH 5/6] disable instantiation for inconsistent states Signed-off-by: Nikolaj Bjorner --- src/smt/qi_queue.cpp | 3 +++ 1 file changed, 3 insertions(+) diff --git a/src/smt/qi_queue.cpp b/src/smt/qi_queue.cpp index cb803d7559..d9520f721f 100644 --- a/src/smt/qi_queue.cpp +++ b/src/smt/qi_queue.cpp @@ -197,6 +197,9 @@ namespace smt { } void qi_queue::instantiate(entry & ent) { + if (m_context.inconsistent()) + return; + // set temporary flag to enable quantifier-specific tracing in within smt_internalizer. flet _coming_from_quant(m_context.m_coming_from_quant, true); From ca2ed449515c052c0075529f5d56c6fd0dfa53a1 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Wed, 15 Jul 2026 20:55:11 -0700 Subject: [PATCH 6/6] disable instantiation for inconsistent states Signed-off-by: Nikolaj Bjorner --- src/smt/qi_queue.cpp | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/smt/qi_queue.cpp b/src/smt/qi_queue.cpp index d9520f721f..7b19cf882f 100644 --- a/src/smt/qi_queue.cpp +++ b/src/smt/qi_queue.cpp @@ -268,7 +268,7 @@ namespace smt { } if (m_on_binding && !m_on_binding(q, instance)) { - verbose_stream() << "qi_queue: on_binding returned false, skipping instance.\n"; + IF_VERBOSE(3, verbose_stream() << "qi_queue: on_binding returned false, skipping instance.\n";); return; } expr_ref lemma(m);