mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-07-15 03:25:43 +00:00
Code Activity

Guard seq length propagation for foldl

Browse source
This commit is contained in:
copilot-swe-agent[bot] 2026-07-13 21:39:40 +00:00 • committed by GitHub
parent c75a034739
commit bc9d35567f
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
2 changed files with 55 additions and 12 deletions
Download patch file Download diff file Expand all files Collapse all files

28
src/smt/theory_seq.cpp
View file

@ -1001,22 +1001,26 @@ bool theory_seq::add_solution(expr* l, expr* r, dependency* deps) {
enode* n1 = ensure_enode(l); enode* n1 = ensure_enode(l);
enode* n2 = ensure_enode(r); enode* n2 = ensure_enode(r);
ptr_vector<expr> len_parents; ptr_vector<expr> len_parents;
auto collect_len_parents = [&](enode* n) { if (m_util.is_seq(r)) {
for (enode* p : n->get_parents()) { auto collect_len_parents = [&](enode* n) {
if (m_util.str.is_length(p->get_expr())) for (enode* p : n->get_parents()) {
len_parents.push_back(p->get_expr()); if (m_util.str.is_length(p->get_expr()))
} len_parents.push_back(p->get_expr());
}; }
collect_len_parents(n1); };
collect_len_parents(n2); collect_len_parents(n1);
collect_len_parents(n2);
}
TRACE(seq, tout << mk_bounded_pp(l, m, 2) << " ==> " << mk_bounded_pp(r, m, 2) << "\n"; display_deps(tout, deps); TRACE(seq, tout << mk_bounded_pp(l, m, 2) << " ==> " << mk_bounded_pp(r, m, 2) << "\n"; display_deps(tout, deps);
tout << "#" << n1->get_owner_id() << " ==> #" << n2->get_owner_id() << "\n"; tout << "#" << n1->get_owner_id() << " ==> #" << n2->get_owner_id() << "\n";
tout << (n1->get_root() == n2->get_root()) << "\n";); tout << (n1->get_root() == n2->get_root()) << "\n";);
propagate_eq(deps, n1, n2); propagate_eq(deps, n1, n2);
expr_ref len_r(m_util.str.mk_length(r), m); if (m_util.is_seq(r)) {
m_rewrite(len_r); expr_ref len_r(m_util.str.mk_length(r), m);
for (expr* len_e : len_parents) { m_rewrite(len_r);
propagate_eq(deps, len_e, len_r, false); for (expr* len_e : len_parents) {
propagate_eq(deps, len_e, len_r, false);
}
} }
return true; return true;
} }

39
src/test/seq_rewriter.cpp
View file

@ -54,6 +54,44 @@ static void test_seq_foldl_nth_model_validation() {
Z3_del_context(ctx); Z3_del_context(ctx);
} }
static void test_seq_foldl_scalar_model_validation() {
Z3_context ctx = Z3_mk_context(nullptr);
char const* result =
Z3_eval_smtlib2_string(ctx,
"(set-option :model_validate true)\n"
"(push)\n"
"(declare-fun f (Int Int) Int)\n"
"(declare-const il (Seq Int))\n"
"(assert (= (seq.foldl f 0 il) 5))\n"
"(check-sat)\n"
"(pop)\n"
"(push)\n"
"(declare-const il (Seq Int))\n"
"(declare-const F (Array Bool Int Bool))\n"
"(assert (= (seq.foldl F true il) true))\n"
"(assert (> (seq.len il) 0))\n"
"(assert (not (= F ((as const (Array Bool Int Bool)) true))))\n"
"(check-sat)\n"
"(pop)\n"
"(push)\n"
"(declare-fun f (Int Int Int) Int)\n"
"(declare-const il (Seq Int))\n"
"(assert (= (seq.foldli f 0 0 il) 5))\n"
"(check-sat)\n"
"(pop)\n"
"(push)\n"
"(declare-const il (Seq Int))\n"
"(declare-const F (Array Int Bool Int Bool))\n"
"(assert (= (seq.foldli F 5 true il) true))\n"
"(assert (> (seq.len il) 0))\n"
"(assert (not (= F ((as const (Array Int Bool Int Bool)) true))))\n"
"(check-sat)\n"
"(pop)\n");
ENSURE(std::strstr(result, "unknown") == nullptr);
ENSURE(std::strstr(result, "sat\nsat\nsat\nsat") != nullptr);
Z3_del_context(ctx);
}
void tst_seq_rewriter() { void tst_seq_rewriter() {
ast_manager m; ast_manager m;
reg_decl_plugins(m); reg_decl_plugins(m);
@ -78,6 +116,7 @@ void tst_seq_rewriter() {
rw(e); rw(e);
std::cout << "empty range lo>hi: " << mk_pp(e, m) << "\n"; std::cout << "empty range lo>hi: " << mk_pp(e, m) << "\n";
ENSURE(su.re.is_empty(e)); ENSURE(su.re.is_empty(e));
test_seq_foldl_scalar_model_validation();
} }
// ----------------------------------------------------------------------- // -----------------------------------------------------------------------