From 5ec28d3bc8aa85a511192b7a0423e63716435d96 Mon Sep 17 00:00:00 2001 From: CEisenhofer Date: Thu, 2 Apr 2026 15:58:15 +0200 Subject: [PATCH] Eliminate length gradients from regexes --- src/ast/arith_decl_plugin.cpp | 10 ++++++ src/ast/arith_decl_plugin.h | 2 +- src/smt/theory_nseq.cpp | 58 +++++++++++++++++++++++++++-------- src/smt/theory_nseq.h | 2 +- 4 files changed, 58 insertions(+), 14 deletions(-) diff --git a/src/ast/arith_decl_plugin.cpp b/src/ast/arith_decl_plugin.cpp index 625a8dc87..5dff4c701 100644 --- a/src/ast/arith_decl_plugin.cpp +++ b/src/ast/arith_decl_plugin.cpp @@ -925,6 +925,16 @@ func_decl* arith_util::mk_mod0() { return m_manager.mk_func_decl(arith_family_id, OP_MOD0, 0, nullptr, 2, rs, mk_int()); } +app *arith_util::mk_divides(expr *arg1, expr *arg2) { + rational val; + bool is_int_num = false; + if (is_numeral(arg1, val, is_int_num) && is_int_num && val.is_int32()) { + parameter p(val.get_int32()); + return m_manager.mk_app(arith_family_id, OP_IDIVIDES, 1, &p, 1, &arg2); + } + return mk_eq(mk_mod(arg2, arg1), mk_int(0)); +} + bool arith_util::is_bounded(expr* n) const { expr* x = nullptr, * y = nullptr; while (true) { diff --git a/src/ast/arith_decl_plugin.h b/src/ast/arith_decl_plugin.h index 5172226ae..30aedf52c 100644 --- a/src/ast/arith_decl_plugin.h +++ b/src/ast/arith_decl_plugin.h @@ -469,7 +469,7 @@ public: app * mk_ge(expr * arg1, expr * arg2) const { return m_manager.mk_app(arith_family_id, OP_GE, arg1, arg2); } app * mk_lt(expr * arg1, expr * arg2) const { return m_manager.mk_app(arith_family_id, OP_LT, arg1, arg2); } app * mk_gt(expr * arg1, expr * arg2) const { return m_manager.mk_app(arith_family_id, OP_GT, arg1, arg2); } - app * mk_divides(expr* arg1, expr* arg2) { return m_manager.mk_app(arith_family_id, OP_IDIVIDES, arg1, arg2); } + app * mk_divides(expr* arg1, expr* arg2); app * mk_add(unsigned num_args, expr * const * args) const { return num_args == 1 && is_app(args[0]) ? to_app(args[0]) : m_manager.mk_app(arith_family_id, OP_ADD, num_args, args); } app * mk_add(expr * arg1, expr * arg2) const { return m_manager.mk_app(arith_family_id, OP_ADD, arg1, arg2); } diff --git a/src/smt/theory_nseq.cpp b/src/smt/theory_nseq.cpp index 017b2eb3a..22ae7aabd 100644 --- a/src/smt/theory_nseq.cpp +++ b/src/smt/theory_nseq.cpp @@ -1203,22 +1203,55 @@ namespace smt { SASSERT(!regexes.empty()); sort* ele_sort; VERIFY(m_seq.is_seq(m_sgraph.get_str_sort(), ele_sort)); + unsigned g = 1; + if (m_gradient_cache.contains(s)) + g = m_gradient_cache[s]; + else + m_gradient_cache.insert(s, 1); + expr_ref allchar(m_seq.re.mk_full_char(m_seq.re.mk_re(m_sgraph.get_str_sort())), m); expr_ref l_expr(m_autil.mk_int(l), m); - expr_ref loop(m_seq.re.mk_loop_proper(allchar.get(), l, l), m); - expr_ref sigmal_expr(loop, m); + expr_ref loop_l(m_seq.re.mk_loop_proper(allchar.get(), l, l), m); - euf::snode* sigmal_node = get_snode(sigmal_expr.get()); + euf::snode* sigmal_node = get_snode(loop_l.get()); regexes.push_back(sigmal_node); SASSERT(regexes.size() > 1); lbool result = m_regex.check_intersection_emptiness(regexes); if (result == l_true) { - expr_ref len_eq_l(m.mk_eq(len_expr, l_expr), m); - if (!ctx.b_internalized(len_eq_l)) - ctx.internalize(len_eq_l, true); - literal lit_len_eq_l = ctx.get_literal(len_eq_l); + // It is empty. Try gradient. + regexes.pop_back(); // Remove loop_l + + expr_ref loop_g(m_seq.re.mk_loop_proper(allchar.get(), g, g), m); + expr_ref star_g(m_seq.re.mk_star(loop_g.get()), m); + expr_ref sigmal_g_expr(m_seq.re.mk_concat(loop_l.get(), star_g.get()), m); + + euf::snode* sigmal_g_node = get_snode(sigmal_g_expr.get()); + regexes.push_back(sigmal_g_node); + + lbool result_g = m_regex.check_intersection_emptiness(regexes); + + expr_ref prop_expr(m); + if (result_g == l_true) { + // Block the whole gradient + expr_ref g_expr(m_autil.mk_int(g), m); + expr_ref len_lt_l(m_autil.mk_lt(len_expr, l_expr), m); + expr_ref len_minus_l(m_autil.mk_sub(len_expr, l_expr), m); + expr_ref not_divides(m.mk_not(m_autil.mk_divides(g_expr, len_minus_l)), m); + prop_expr = m.mk_or(len_lt_l, not_divides); + std::cout << "Propagating " << mk_pp(prop_expr, m) << " for length " << l << " with gradient " << g << std::endl; + + m_gradient_cache[s] = 1; // Reset gradient cache + } + else { + prop_expr = m.mk_not(m.mk_eq(len_expr, l_expr)); + m_gradient_cache[s] = g + 1; // Increment gradient cache + } + + if (!ctx.b_internalized(prop_expr)) + ctx.internalize(prop_expr, true); + literal lit_prop = ctx.get_literal(prop_expr); enode_pair_vector eqs; literal_vector dep_lits; @@ -1227,17 +1260,18 @@ namespace smt { seq::deps_to_lits(mems[idx].m_dep, eqs, dep_lits); } - ctx.mark_as_relevant(lit_len_eq_l); + ctx.mark_as_relevant(lit_prop); justification* js = ctx.mk_justification( ext_theory_propagation_justification( get_id(), ctx, dep_lits.size(), dep_lits.data(), eqs.size(), eqs.data(), - ~lit_len_eq_l)); + lit_prop)); - ctx.assign(~lit_len_eq_l, js); - TRACE(seq, tout << "nseq length coherence check: length " << l << " is incompatible for " << mk_pp(s, m) << ", propagated ~" << mk_pp(len_eq_l, m) << "\n";); - IF_VERBOSE(1, verbose_stream() << "nseq length coherence check: length " << l << " is incompatible for " << mk_pp(s, m) << ", propagated ~" << mk_pp(len_eq_l, m) << "\n";); + ctx.assign(lit_prop, js); + + TRACE(seq, tout << "nseq length coherence check: length " << l << " with gradient " << g << " is incompatible for " << mk_pp(s, m) << ", propagated " << mk_pp(prop_expr, m) << "\n";); + IF_VERBOSE(1, verbose_stream() << "nseq length coherence check: length " << l << " with gradient " << g << " is incompatible for " << mk_pp(s, m) << ", propagated " << mk_pp(prop_expr, m) << "\n";); return false; } } diff --git a/src/smt/theory_nseq.h b/src/smt/theory_nseq.h index 7e0a424fe..84cbeb147 100644 --- a/src/smt/theory_nseq.h +++ b/src/smt/theory_nseq.h @@ -66,7 +66,7 @@ namespace smt { obj_hashtable m_axiom_set; // dedup guard for axiom_item enqueues obj_hashtable m_no_diseq_set; // track expressions that should not trigger new disequality axioms expr_ref_vector m_relevant_lengths; // track variables whose lengths are relevant - + obj_map m_gradient_cache; sat::literal_vector m_nielsen_literals; // literals created by a Nilsen check // statistics