mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-04-27 14:23:35 +00:00
Code Activity

Merge branch 'c3' into copilot/fix-reconcat-classification

Browse source
This commit is contained in:
Nikolaj Bjorner 2026-03-03 13:10:25 -08:00 • committed by GitHub
commit a80652270d
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
3 changed files with 204 additions and 3 deletions
Download patch file Download diff file Expand all files Collapse all files

7
src/ast/euf/euf_seq_plugin.cpp
View file

@ -212,11 +212,16 @@ namespace euf {
if (same_star_body(a, b))
push_merge(n, a);
// Rule 1 extended: concat(v*, concat(v*, c)) = concat(v*, c)
// Rule 1 extended (right): concat(v*, concat(v*, c)) = concat(v*, c)
enode* b1, *b2;
if (is_concat(b, b1, b2) && same_star_body(a, b1))
push_merge(n, b);
// Rule 1 extended (left): concat(concat(c, v*), v*) = concat(c, v*)
enode* a1, *a2;
if (is_concat(a, a1, a2) && same_star_body(a2, b))
push_merge(n, a);
// Rule 2: Nullable absorption by .*
// concat(.*, v) = .* when v is nullable
if (is_full_seq(a) && is_nullable(b))

8
src/ast/euf/euf_sgraph.cpp
View file

@ -470,13 +470,17 @@ namespace euf {
}
snode* sgraph::drop_left(snode* n, unsigned count) {
for (unsigned i = 0; i < count && !n->is_empty(); ++i)
if (count == 0 || n->is_empty()) return n;
if (count >= n->length()) return mk_empty();
for (unsigned i = 0; i < count; ++i)
n = drop_first(n);
return n;
}
snode* sgraph::drop_right(snode* n, unsigned count) {
for (unsigned i = 0; i < count && !n->is_empty(); ++i)
if (count == 0 || n->is_empty()) return n;
if (count >= n->length()) return mk_empty();
for (unsigned i = 0; i < count; ++i)
n = drop_last(n);
return n;
}