From aab96dbd29a673c390031ac58666e5ccc798ddfa Mon Sep 17 00:00:00 2001 From: CEisenhofer Date: Tue, 24 Mar 2026 14:58:10 +0100 Subject: [PATCH] Rule for unwinding powers in membership constraints --- src/smt/seq/seq_nielsen.cpp | 87 +++++++++++++++++++++++++++++++++---- src/smt/seq/seq_nielsen.h | 9 +++- 2 files changed, 85 insertions(+), 11 deletions(-) diff --git a/src/smt/seq/seq_nielsen.cpp b/src/smt/seq/seq_nielsen.cpp index 98806c37d..104e98a2f 100644 --- a/src/smt/seq/seq_nielsen.cpp +++ b/src/smt/seq/seq_nielsen.cpp @@ -2437,9 +2437,13 @@ namespace seq { if (apply_var_nielsen(node)) return ++m_stats.m_mod_var_nielsen, true; - // Priority 13: VarNumUnwinding - variable power unwinding - if (apply_var_num_unwinding(node)) - return ++m_stats.m_mod_var_num_unwinding, true; + // Priority 13: VarNumUnwinding - variable power unwinding for equality constraints + if (apply_var_num_unwinding_eq(node)) + return ++m_stats.m_mod_var_num_unwinding_eq, true; + + // Priority 14: variable power unwinding for membership constraints + if (apply_var_num_unwinding_mem(node)) + return ++m_stats.m_mod_var_num_unwinding_mem, true; return false; } @@ -2523,10 +2527,8 @@ namespace seq { str_eq const*& eq_out, bool& fwd) const { for (str_eq const& eq : node->str_eqs()) { - if (eq.is_trivial()) - continue; - if (!eq.m_lhs || !eq.m_rhs) - continue; + SASSERT(eq.m_lhs && eq.m_rhs && !eq.is_trivial()); + for (unsigned od = 0; od < 2; ++od) { bool local_fwd = (od == 0); euf::snode* lhead = dir_token(eq.m_lhs, local_fwd); @@ -2550,6 +2552,27 @@ namespace seq { return false; } + bool nielsen_graph::find_power_vs_var(nielsen_node* node, + euf::snode*& power, + str_mem const*& mem_out, + bool& fwd) const { + for (str_mem const& mem : node->str_mems()) { + SASSERT(mem.m_str && mem.m_regex && !mem.is_trivial()); + + for (unsigned od = 0; od < 2; ++od) { + bool local_fwd = (od == 0); + euf::snode* lhead = dir_token(mem.m_str, local_fwd); + if (lhead && lhead->is_power()) { + power = lhead; + mem_out = &mem; + fwd = local_fwd; + return true; + } + } + } + return false; + } + // ----------------------------------------------------------------------- // Modifier: apply_power_epsilon // Fires only when one side of an equation is empty and the other side @@ -3493,7 +3516,7 @@ namespace seq { // mirrors ZIPT's VarNumUnwindingModifier // ----------------------------------------------------------------------- - bool nielsen_graph::apply_var_num_unwinding(nielsen_node* node) { + bool nielsen_graph::apply_var_num_unwinding_eq(nielsen_node* node) { ast_manager& m = m_sg.get_manager(); arith_util arith(m); @@ -3539,6 +3562,51 @@ namespace seq { return true; } + bool nielsen_graph::apply_var_num_unwinding_mem(nielsen_node* node) { + ast_manager& m = m_sg.get_manager(); + arith_util arith(m); + + euf::snode* power = nullptr; + str_mem const* mem = nullptr; + bool fwd = true; + if (!find_power_vs_var(node, power, mem, fwd)) + return false; + + SASSERT(power->is_power() && power->num_args() >= 1); + euf::snode* base = power->arg(0); + expr* exp_n = get_power_exponent(power); + expr* zero = arith.mk_int(0); + expr* one = arith.mk_int(1); + + // Branch 1: n = 0 → replace u^n with ε (progress) + // Side constraint: n = 0 + { + nielsen_node* child = mk_child(node); + nielsen_edge* e = mk_edge(node, child, true); + nielsen_subst s(power, m_sg.mk_empty_seq(power->get_sort()), mem->m_dep); + e->add_subst(s); + child->apply_subst(m_sg, s); + if (exp_n) + e->add_side_int(mk_int_constraint(exp_n, zero, int_constraint_kind::eq, mem->m_dep)); + } + + // Branch 2: n >= 1 → peel one u: u^n → u · u^(n-1) + // Side constraint: n >= 1 + { + euf::snode* fresh = mk_fresh_var(power->get_sort()); + euf::snode* replacement = dir_concat(m_sg, base, fresh, fwd); + nielsen_node* child = mk_child(node); + nielsen_edge* e = mk_edge(node, child, false); + nielsen_subst s(power, replacement, mem->m_dep); + e->add_subst(s); + child->apply_subst(m_sg, s); + if (exp_n) + e->add_side_int(mk_int_constraint(exp_n, one, int_constraint_kind::ge, mem->m_dep)); + } + + return true; + } + void nielsen_graph::collect_conflict_deps(dep_tracker& deps) const { for (nielsen_node const* n : m_nodes) { if (n->eval_idx() != m_run_idx) @@ -4198,7 +4266,8 @@ namespace seq { st.update("nseq mod regex var", m_stats.m_mod_regex_var_split); st.update("nseq mod power split", m_stats.m_mod_power_split); st.update("nseq mod var nielsen", m_stats.m_mod_var_nielsen); - st.update("nseq mod var num unwind", m_stats.m_mod_var_num_unwinding); + st.update("nseq mod var num unwind (eq)", m_stats.m_mod_var_num_unwinding_eq); + st.update("nseq mod var num unwind (mem)", m_stats.m_mod_var_num_unwinding_mem); } } diff --git a/src/smt/seq/seq_nielsen.h b/src/smt/seq/seq_nielsen.h index 1b3d90acd..cf00fcd2f 100644 --- a/src/smt/seq/seq_nielsen.h +++ b/src/smt/seq/seq_nielsen.h @@ -742,7 +742,8 @@ namespace seq { unsigned m_mod_signature_split = 0; unsigned m_mod_power_split = 0; unsigned m_mod_var_nielsen = 0; - unsigned m_mod_var_num_unwinding = 0; + unsigned m_mod_var_num_unwinding_eq = 0; + unsigned m_mod_var_num_unwinding_mem = 0; void reset() { memset(this, 0, sizeof(nielsen_stats)); } }; @@ -1085,7 +1086,9 @@ namespace seq { // variable numeric unwinding: for a power token u^n vs a variable, // branch: (1) n = 0 (u^n = ε), (2) n >= 1 (peel one u). // mirrors ZIPT's VarNumUnwindingModifier - bool apply_var_num_unwinding(nielsen_node* node); + bool apply_var_num_unwinding_eq(nielsen_node* node); + + bool apply_var_num_unwinding_mem(nielsen_node* node); // find the first power token in any str_eq at this node euf::snode* find_power_token(nielsen_node* node) const; @@ -1098,6 +1101,8 @@ namespace seq { // equation; returns orientation via `fwd` (true=head, false=tail). bool find_power_vs_var(nielsen_node* node, euf::snode*& power, euf::snode*& var_head, str_eq const*& eq_out, bool& fwd) const; + bool find_power_vs_var(nielsen_node* node, euf::snode*& power, str_mem const*& mem_out, bool& fwd) const; + // ----------------------------------------------- // Integer feasibility subsolver methods // -----------------------------------------------