mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-04-02 18:08:57 +00:00
Code Activity

Rule for unwinding powers in membership constraints

Browse source
This commit is contained in:
CEisenhofer 2026-03-24 14:58:10 +01:00
parent 538fbc1b8d
commit aab96dbd29
2 changed files with 85 additions and 11 deletions
Download patch file Download diff file Expand all files Collapse all files

87
src/smt/seq/seq_nielsen.cpp
View file

@ -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);
}
}

9
src/smt/seq/seq_nielsen.h
View file

@ -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
// -----------------------------------------------