mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-04-26 13:53:33 +00:00
Code Activity

Merge branch 'c3' into copilot/add-arith-util-to-nielsen-graph

Browse source
This commit is contained in:
Nikolaj Bjorner 2026-04-01 07:18:09 -07:00 • committed by GitHub
commit 76ea0d2fbf
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
1 changed files with 16 additions and 17 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -526,12 +526,8 @@ namespace seq {
// Power equated to empty → exponent must be 0. // Power equated to empty → exponent must be 0.
expr* e = t->get_expr(); expr* e = t->get_expr();
expr* pow_base = nullptr, *pow_exp = nullptr; expr* pow_base = nullptr, *pow_exp = nullptr;
if (e) seq.str.is_power(e, pow_base, pow_exp); if (seq.str.is_power(e, pow_base, pow_exp) && pow_exp)
if (pow_exp) { add_constraint(constraint(m.mk_eq(pow_exp, a.mk_int(0)), dep, m));
expr* zero = m_graph.a.mk_int(0);
add_constraint(
constraint(m.mk_eq(pow_exp, zero), dep, m));
}
nielsen_subst s(t, sg.mk_empty_seq(t->get_sort()), dep); nielsen_subst s(t, sg.mk_empty_seq(t->get_sort()), dep);
apply_subst(sg, s); apply_subst(sg, s);
changed = true; changed = true;
@ -597,7 +593,8 @@ namespace seq {
euf::snode_vector tokens; euf::snode_vector tokens;
side->collect_tokens(tokens); side->collect_tokens(tokens);
if (tokens.size() < 2) return nullptr; if (tokens.size() < 2)
return nullptr;
ast_manager& m = sg.get_manager(); ast_manager& m = sg.get_manager();
arith_util arith(m); arith_util arith(m);
@ -685,7 +682,8 @@ namespace seq {
++i; ++i;
} }
if (!merged) return nullptr; if (!merged)
return nullptr;
euf::snode* rebuilt = nullptr; euf::snode* rebuilt = nullptr;
for (unsigned k = 0; k < result.size(); ++k) for (unsigned k = 0; k < result.size(); ++k)
@ -2471,7 +2469,7 @@ namespace seq {
if (lhead->num_args() < 1 || rhead->num_args() < 1) if (lhead->num_args() < 1 || rhead->num_args() < 1)
continue; continue;
// same base: compare the two powers // same base: compare the two powers
if (lhead->arg(0)->id() != rhead->arg(0)->id()) if (lhead->arg(0) != rhead->arg(0))
continue; continue;
// Skip if the exponents differ by a constant — simplify_and_init's // Skip if the exponents differ by a constant — simplify_and_init's
@ -2485,15 +2483,13 @@ namespace seq {
// Branch 1 (explored first): n < m (add constraint c ≥ p + 1) // Branch 1 (explored first): n < m (add constraint c ≥ p + 1)
{ {
nielsen_node* child = mk_child(node); nielsen_edge *e = mk_edge(node, mk_child(node), true);
nielsen_edge* e = mk_edge(node, child, true);
expr_ref n_plus_1(a.mk_add(exp_n, a.mk_int(1)), m); expr_ref n_plus_1(a.mk_add(exp_n, a.mk_int(1)), m);
e->add_side_constraint(mk_constraint(a.mk_ge(exp_m, n_plus_1), eq.m_dep)); e->add_side_constraint(mk_constraint(a.mk_ge(exp_m, n_plus_1), eq.m_dep));
} }
// Branch 2 (explored second): m <= n (add constraint p ≥ c) // Branch 2 (explored second): m <= n (add constraint p ≥ c)
{ {
nielsen_node* child = mk_child(node); nielsen_edge *e = mk_edge(node, mk_child(node), true);
nielsen_edge* e = mk_edge(node, child, true);
e->add_side_constraint(mk_constraint(a.mk_ge(exp_n, exp_m), eq.m_dep)); e->add_side_constraint(mk_constraint(a.mk_ge(exp_n, exp_m), eq.m_dep));
} }
return true; return true;
@ -2520,12 +2516,15 @@ namespace seq {
for (str_eq const& eq : node->str_eqs()) { for (str_eq const& eq : node->str_eqs()) {
if (eq.is_trivial()) if (eq.is_trivial())
continue; continue;
// NB: Shuvendu - this test is always false based on how str_eqs are constructed
// it can be an assertion to force the invariant that str_eqs always have both sides non-null.
if (!eq.m_lhs || !eq.m_rhs) if (!eq.m_lhs || !eq.m_rhs)
continue; continue;
for (int side = 0; side < 2; ++side) { for (int side = 0; side < 2; ++side) {
euf::snode* pow_side = (side == 0) ? eq.m_lhs : eq.m_rhs; euf::snode* pow_side = (side == 0) ? eq.m_lhs : eq.m_rhs;
euf::snode* other_side = (side == 0) ? eq.m_rhs : eq.m_lhs; euf::snode* other_side = (side == 0) ? eq.m_rhs : eq.m_lhs;
// NB: Shuvendu - this test is always false
if (!pow_side || !other_side) if (!pow_side || !other_side)
continue; continue;
@ -2536,6 +2535,7 @@ namespace seq {
continue; continue;
euf::snode* base_sn = end_tok->arg(0); euf::snode* base_sn = end_tok->arg(0);
expr* pow_exp = get_power_exp_expr(end_tok, seq); expr* pow_exp = get_power_exp_expr(end_tok, seq);
// NB: Shuvendu - this test is also redundant
if (!base_sn || !pow_exp) if (!base_sn || !pow_exp)
continue; continue;
@ -2553,15 +2553,13 @@ namespace seq {
// Branch 1: pow_exp < count (i.e., count >= pow_exp + 1) // Branch 1: pow_exp < count (i.e., count >= pow_exp + 1)
{ {
nielsen_node* child = mk_child(node); nielsen_edge *e = mk_edge(node, mk_child(node), true);
nielsen_edge* e = mk_edge(node, child, true);
expr_ref pow_plus1(a.mk_add(pow_exp, a.mk_int(1)), m); expr_ref pow_plus1(a.mk_add(pow_exp, a.mk_int(1)), m);
e->add_side_constraint(mk_constraint(a.mk_ge(norm_count, pow_plus1), eq.m_dep)); e->add_side_constraint(mk_constraint(a.mk_ge(norm_count, pow_plus1), eq.m_dep));
} }
// Branch 2: count <= pow_exp (i.e., pow_exp >= count) // Branch 2: count <= pow_exp (i.e., pow_exp >= count)
{ {
nielsen_node* child = mk_child(node); nielsen_edge *e = mk_edge(node, mk_child(node), true);
nielsen_edge* e = mk_edge(node, child, true);
e->add_side_constraint(mk_constraint(a.mk_ge(pow_exp, norm_count), eq.m_dep)); e->add_side_constraint(mk_constraint(a.mk_ge(pow_exp, norm_count), eq.m_dep));
} }
return true; return true;
@ -3956,6 +3954,7 @@ namespace seq {
} }
m_solver.assert_expr(m.mk_distinct(dist.size(), dist.data())); m_solver.assert_expr(m.mk_distinct(dist.size(), dist.data()));
} }
// NSB code review: there is a seprate sort for characters
bv_util arith(m); bv_util arith(m);
for (auto const& kvp : m_sat_node->char_ranges()) { for (auto const& kvp : m_sat_node->char_ranges()) {
expr_ref_vector cases(m); expr_ref_vector cases(m);