mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-10-07 03:35:47 +00:00
Code Activity

Integrated seq.power in seq (#10705)

Browse source 
Co-authored-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Clemens Eisenhofer 2026-08-31 09:42:49 -07:00 • committed by GitHub
parent 6aa9416d4a
commit 71522ca0ac
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
4 changed files with 62 additions and 27 deletions
Download patch file Download diff file Expand all files Collapse all files

28
src/ast/rewriter/seq_axioms.cpp
View file

@ -1192,7 +1192,10 @@ namespace seq {
n <= 0 => e = empty
s = empty => e = empty
n > 0 => len(e) = n * len(s)
n > 0 and s != empty => n <= len(e)
The last axiom is implied by the previous one, but it is linear and
therefore bounds the exponent even when len(s) is not fixed.
The unfolding into a concatenation is only added on demand, see power_unfold_axiom.
*/
void axioms::power_axiom(expr* e) {
@ -1200,21 +1203,33 @@ namespace seq {
VERIFY(seq.str.is_power(e, s, n));
expr_ref emp(seq.str.mk_empty(e->get_sort()), m);
expr_ref n_ge_1 = mk_ge(n, 1);
expr_ref len_e = mk_len(e);
add_clause(n_ge_1, mk_eq(e, emp));
add_clause(~mk_eq(s, emp), mk_eq(e, emp));
add_clause(~n_ge_1, mk_eq(mk_len(e), a.mk_mul(n, mk_len(s))));
add_clause(~n_ge_1, mk_eq(len_e, a.mk_mul(n, mk_len(s))));
add_clause(~n_ge_1, mk_eq(s, emp), mk_ge_e(len_e, n));
}
/**
n = j => s^n = s ++ .. ++ s (j copies), for 1 <= j <= k
The exponent is bounded by k thanks to the length limit of e, so the
cases below are exhaustive for the current unfolding depth.
The length limit of e bounds n by k, so the cases are exhaustive at
the current unfolding depth.
*/
void axioms::power_unfold_axiom(expr* e, unsigned k) {
expr* s = nullptr, *n = nullptr;
VERIFY(seq.str.is_power(e, s, n));
expr_ref pow(s, m);
rational v;
// a known exponent only needs the case it matches
if (a.is_numeral(n, v)) {
if (!v.is_pos() || v > rational(k))
return;
for (unsigned j = 1; j < v.get_unsigned(); ++j)
pow = mk_concat(s, pow);
add_clause(mk_seq_eq(e, pow));
return;
}
for (unsigned j = 1; j <= k; ++j) {
add_clause(~mk_eq(n, a.mk_int(j)), mk_seq_eq(e, pow));
pow = mk_concat(s, pow);
@ -1386,7 +1401,12 @@ namespace seq {
expr_ref axioms::length_limit(expr* s, unsigned k) {
expr_ref bound_tracker = m_sk.mk_length_limit(s, k);
expr* s0 = nullptr;
expr* s0 = nullptr, *n = nullptr;
// the unfolding of a power is bounded by its exponent, not by its length
if (seq.str.is_power(s, s0, n)) {
add_clause(~bound_tracker, mk_le(n, k));
return bound_tracker;
}
if (seq.str.is_stoi(s, s0))
s = s0;
add_clause(~bound_tracker, mk_le(mk_len(s), k));

28
src/ast/rewriter/seq_rewriter.cpp
View file

@ -545,7 +545,7 @@ br_status seq_rewriter::mk_seq_length(expr* a, expr_ref& result) {
result = str().mk_length(z);
return BR_REWRITE1;
}
// len(s^n) = n * len(s) for n > 0
// len(s^n) = n * len(s) for n >= 0
if (str().is_power(a, x, y) && m_autil.is_numeral(y, r) && r >= 0) {
result = m_autil.mk_mul(y, str().mk_length(x));
return BR_REWRITE2;
@ -597,13 +597,13 @@ br_status seq_rewriter::mk_seq_power(expr* a, expr* b, expr_ref& result) {
if (!(n * rational(t.length())).is_unsigned())
return BR_FAILED;
zstring r = t;
for (unsigned i = 1; i < v; i++)
for (unsigned i = 1; i < v; ++i)
r += t;
result = str().mk_string(r);
return BR_DONE;
}
expr_ref_vector es(m());
for (unsigned i = 0; i < v; i++)
for (unsigned i = 0; i < v; ++i)
es.push_back(a);
result = str().mk_concat(es, a->get_sort());
return BR_REWRITE_FULL;
@ -4620,14 +4620,15 @@ br_status seq_rewriter::mk_eq_core(expr * l, expr * r, expr_ref & result) {
bool changed = false;
if (reduce_eq_empty(l, r, result))
return BR_REWRITE_FULL;
// s^n = s^k <=> s = "" or (n <= 0 and k <= 0) or (0 < n = k)
expr* s1 = nullptr, *n1 = nullptr, *s2 = nullptr, *n2 = nullptr;
if (str().is_power(l, s1, n1) && str().is_power(r, s2, n2) && s1 == s2) {
expr* emp = str().mk_empty(s1->get_sort());
expr_ref_vector disj(m());
disj.push_back(m().mk_eq(s1, emp));
disj.push_back(m().mk_and(m_autil.mk_le(n1, zero()), m_autil.mk_le(n2, zero())));
disj.push_back(m().mk_and(m_autil.mk_lt(zero(), n1), m_autil.mk_lt(zero(), n2), m().mk_eq(n1, n2)));
result = m().mk_or(disj);
expr_ref emp(str().mk_empty(s1->get_sort()), m());
expr_ref_vector fmls(m());
fmls.push_back(m().mk_eq(s1, emp));
fmls.push_back(m().mk_and(m_autil.mk_le(n1, zero()), m_autil.mk_le(n2, zero())));
fmls.push_back(m().mk_and(m_autil.mk_lt(zero(), n1), m_autil.mk_lt(zero(), n2), m().mk_eq(n1, n2)));
result = m().mk_or(fmls);
return BR_REWRITE_FULL;
}
@ -5292,12 +5293,13 @@ bool seq_rewriter::reduce_eq_empty(expr* l, expr* r, expr_ref& result) {
result = m_autil.mk_lt(s, zero());
return true;
}
// s^n = "" <=> n <= 0 or s = ""
expr* base = nullptr, *n = nullptr;
if (str().is_power(r, base, n)) {
expr_ref_vector disj(m());
disj.push_back(m_autil.mk_le(n, zero()));
disj.push_back(m().mk_eq(base, l));
result = m().mk_or(disj);
expr_ref_vector fmls(m());
fmls.push_back(m_autil.mk_le(n, zero()));
fmls.push_back(m().mk_eq(base, l));
result = m().mk_or(fmls);
return true;
}
// at(s, offset) = "" <=> len(s) <= offset or offset < 0

11
src/smt/theory_seq.cpp
View file

@ -2855,6 +2855,10 @@ void theory_seq::deque_axiom(expr* n) {
else if (m_util.str.is_unit(n)) {
m_ax.add_unit_axiom(n);
}
else if (m_util.str.is_power(n)) {
m_ax.add_power_axiom(n);
add_length_limit(n, m_max_unfolding_depth, true);
}
else if (m_util.str.is_is_digit(n)) {
m_ax.add_is_digit_axiom(n);
}
@ -3451,6 +3455,7 @@ void theory_seq::relevant_eh(expr* _n) {
m_util.str.is_from_code(n) ||
m_util.str.is_to_code(n) ||
m_util.str.is_unit(n) ||
m_util.str.is_power(n) ||
m_util.str.is_last_index(n) ||
m_util.str.is_length(n) ||
/* m_util.str.is_replace_all(n) || uncomment to enable axiomatization */
@ -3482,8 +3487,7 @@ void theory_seq::relevant_eh(expr* _n) {
if (m_util.str.is_length(n, arg) && !has_length(arg) && ctx.e_internalized(arg))
add_length_to_eqc(arg);
if (m_util.str.is_power(n) ||
m_util.str.is_replace_all(n) ||
if (m_util.str.is_replace_all(n) ||
m_util.str.is_replace_re(n) ||
m_util.str.is_replace_re_all(n)) {
add_unhandled_expr(n);
@ -3571,6 +3575,9 @@ void theory_seq::propagate_length_limit(expr* e) {
if (m_util.str.is_itos(s)) {
m_ax.add_itos_axiom(s, k);
}
if (m_util.str.is_power(s)) {
m_ax.add_power_unfold_axiom(s, k);
}
}
/*

22
src/test/seq_power.cpp
View file

@ -91,26 +91,32 @@ static void tst_power_solver() {
expr_ref ab(seq.str.mk_string(zstring("ab")), m);
expr_ref_vector fmls(m);
// symbolic exponents are unsupported by theory_seq
// "ab"^n = "abab" has the solution n = 2
fmls.push_back(m.mk_eq(seq.str.mk_power(ab, n), seq.str.mk_string(zstring("abab"))));
ENSURE(check(m, fmls) == l_undef);
ENSURE(check(m, fmls) == l_true);
// symbolic exponents are unsupported by theory_seq
// the length of "ab"^n is even
fmls.reset();
fmls.push_back(m.mk_eq(seq.str.mk_power(ab, n), seq.str.mk_string(zstring("aba"))));
ENSURE(check(m, fmls) == l_undef);
ENSURE(check(m, fmls) == l_false);
// symbolic exponents are unsupported by theory_seq
// x^n is empty for n <= 0
fmls.reset();
fmls.push_back(a.mk_le(n, a.mk_int(0)));
fmls.push_back(m.mk_eq(seq.str.mk_power(x, n), seq.str.mk_string(zstring("a"))));
ENSURE(check(m, fmls) == l_undef);
ENSURE(check(m, fmls) == l_false);
// symbolic exponents are unsupported by theory_seq
// x^n = "aaaa" with |x| = 2 has the solution x = "aa", n = 2
fmls.reset();
fmls.push_back(m.mk_eq(seq.str.mk_power(x, n), seq.str.mk_string(zstring("aaaa"))));
fmls.push_back(m.mk_eq(seq.str.mk_length(x), a.mk_int(2)));
ENSURE(check(m, fmls) == l_undef);
ENSURE(check(m, fmls) == l_true);
// the unfolding is exact for a fixed exponent
fmls.reset();
fmls.push_back(a.mk_eq(n, a.mk_int(3)));
fmls.push_back(m.mk_not(m.mk_eq(seq.str.mk_power(x, n), seq.str.mk_concat(x, seq.str.mk_concat(x, x)))));
ENSURE(check(m, fmls) == l_false);
}
void tst_seq_power() {