mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-07-04 06:16:09 +00:00
Code Activity

Substitutions are extensions

Browse source
This commit is contained in:
CEisenhofer 2026-04-08 19:13:10 +02:00
parent 513f49f39c
commit 857e93fdb2
2 changed files with 42 additions and 30 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -481,8 +481,8 @@ namespace seq {
// nielsen_node: simplify_and_init // nielsen_node: simplify_and_init
// ----------------------------------------------------------------------- // -----------------------------------------------------------------------
bool nielsen_node::handle_empty_side(euf::sgraph& sg, euf::snode* non_empty_side, bool nielsen_node::check_empty_side_conflict(euf::sgraph& sg, euf::snode* non_empty_side,
dep_tracker const& dep, bool& changed) { dep_tracker const& dep) {
euf::snode_vector tokens; euf::snode_vector tokens;
non_empty_side->collect_tokens(tokens); non_empty_side->collect_tokens(tokens);
bool has_char = std::any_of(tokens.begin(), tokens.end(), [](euf::snode* t){ return t->is_char(); }); bool has_char = std::any_of(tokens.begin(), tokens.end(), [](euf::snode* t){ return t->is_char(); });
@ -490,30 +490,10 @@ namespace seq {
return t->is_var() || t->is_power(); return t->is_var() || t->is_power();
}); });
if (has_char || !all_eliminable) { if (has_char || !all_eliminable) {
m_is_general_conflict = true; set_general_conflict(true);
set_conflict(backtrack_reason::symbol_clash, dep); set_conflict(backtrack_reason::symbol_clash, dep);
return true; return true;
} }
ast_manager& m = sg.get_manager();
seq_util& seq = sg.get_seq_util();
arith_util a(m);
for (euf::snode* t : tokens) {
if (t->is_var()) {
nielsen_subst s(t, sg.mk_empty_seq(t->get_sort()), dep);
apply_subst(sg, s);
changed = true;
}
else if (t->is_power()) {
// Power equated to empty → exponent must be 0.
expr* e = t->get_expr();
expr* pow_base = nullptr, *pow_exp = nullptr;
if (seq.str.is_power(e, pow_base, pow_exp) && pow_exp)
add_constraint(constraint(m.mk_eq(pow_exp, a.mk_int(0)), dep, m));
nielsen_subst s(t, sg.mk_empty_seq(t->get_sort()), dep);
apply_subst(sg, s);
changed = true;
}
}
return false; return false;
} }
@ -838,14 +818,15 @@ namespace seq {
if (!eq.m_lhs || !eq.m_rhs) if (!eq.m_lhs || !eq.m_rhs)
continue; continue;
// one side empty, the other not empty => conflict or substitution // one side empty, the other not empty => conflict check
// (the actual substitution is done in apply_det_modifier)
if (eq.m_lhs->is_empty() && !eq.m_rhs->is_empty()) { if (eq.m_lhs->is_empty() && !eq.m_rhs->is_empty()) {
if (handle_empty_side(sg, eq.m_rhs, eq.m_dep, changed)) if (check_empty_side_conflict(sg, eq.m_rhs, eq.m_dep))
return simplify_result::conflict; return simplify_result::conflict;
continue; continue;
} }
if (eq.m_rhs->is_empty() && !eq.m_lhs->is_empty()) { if (eq.m_rhs->is_empty() && !eq.m_lhs->is_empty()) {
if (handle_empty_side(sg, eq.m_lhs, eq.m_dep, changed)) if (check_empty_side_conflict(sg, eq.m_lhs, eq.m_dep))
return simplify_result::conflict; return simplify_result::conflict;
continue; continue;
} }
@ -1512,6 +1493,37 @@ namespace seq {
if (!l || !r) if (!l || !r)
continue; continue;
// 0. empty side propagation
if (l->is_empty() || r->is_empty()) {
euf::snode* non_empty_side = l->is_empty() ? r : l;
nielsen_node* child = mk_child(node);
nielsen_edge* e = mk_edge(node, child, true);
euf::snode_vector tokens;
non_empty_side->collect_tokens(tokens);
auto& eqs = child->str_eqs();
eqs[eq_idx] = eqs.back();
eqs.pop_back();
for (euf::snode* t : tokens) {
if (t->is_var()) {
nielsen_subst s(t, m_sg.mk_empty_seq(t->get_sort()), eq.m_dep);
e->add_subst(s);
child->apply_subst(m_sg, s);
} else if (t->is_power()) {
expr* expr_node = t->get_expr();
expr* pow_base = nullptr, *pow_exp = nullptr;
if (seq().str.is_power(expr_node, pow_base, pow_exp) && pow_exp) {
e->add_side_constraint(mk_constraint(m.mk_eq(pow_exp, a.mk_int(0)), eq.m_dep));
}
nielsen_subst s(t, m_sg.mk_empty_seq(t->get_sort()), eq.m_dep);
e->add_subst(s);
child->apply_subst(m_sg, s);
}
}
return true;
}
// 1. unit equalities produced by unit-unit prefix/suffix splits // 1. unit equalities produced by unit-unit prefix/suffix splits
{ {
euf::snode_vector lhs_toks, rhs_toks; euf::snode_vector lhs_toks, rhs_toks;
@ -4020,6 +4032,7 @@ nielsen_graph::generate_length_constraints(vector<length_constraint>& constraint
} }
bool nielsen_graph::check_lp_le(expr* lhs, expr* rhs) { bool nielsen_graph::check_lp_le(expr* lhs, expr* rhs) {
// TODO: We need the justification!!
rational lhs_lo, rhs_up; rational lhs_lo, rhs_up;
if (m_solver.lower_bound(lhs, lhs_lo) && if (m_solver.lower_bound(lhs, lhs_lo) &&
m_solver.upper_bound(rhs, rhs_up)) { m_solver.upper_bound(rhs, rhs_up)) {

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

@ -688,10 +688,9 @@ namespace seq {
// Helper: handle one empty vs one non-empty side of a string equality. // Helper: handle one empty vs one non-empty side of a string equality.
// Collects tokens from non_empty_side; if any token causes a conflict // Collects tokens from non_empty_side; if any token causes a conflict
// (is a concrete character or an unexpected kind), sets conflict flags // (is a concrete character or an unexpected kind), sets conflict flags
// and returns true. Otherwise substitutes all variables to empty, // and returns true. Otherwise returns false.
// sets changed=true, and returns false. bool check_empty_side_conflict(euf::sgraph& sg, euf::snode* non_empty_side,
bool handle_empty_side(euf::sgraph& sg, euf::snode* non_empty_side, dep_tracker const& dep);
dep_tracker const& dep, bool& changed);
// Length bounds are queried from the arithmetic subsolver when needed. // Length bounds are queried from the arithmetic subsolver when needed.
}; };