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

fix bugs

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2026-06-17 09:14:16 -06:00
parent 3d2d793f1d
commit 26feb16714
2 changed files with 14 additions and 5 deletions
Download patch file Download diff file Expand all files Collapse all files

13
src/ast/rewriter/seq_derive.cpp
View file

@ -778,9 +778,9 @@ namespace seq {
if (re().is_full_seq(a) && re().is_full_seq(b))
return expr_ref(a, m);
if (re().is_full_char(a) && re().is_full_seq(b))
return expr_ref(re().mk_plus(re().mk_full_char(ele_s)), m);
return expr_ref(re().mk_plus(re().mk_full_char(a->get_sort())), m);
if (re().is_full_seq(a) && re().is_full_char(b))
return expr_ref(re().mk_plus(re().mk_full_char(ele_s)), m);
return expr_ref(re().mk_plus(re().mk_full_char(a->get_sort())), m);
// to_re(s1) · to_re(s2) → to_re(s1 ++ s2)
expr* s1 = nullptr, * s2 = nullptr;
@ -898,7 +898,8 @@ namespace seq {
return mk_ite(c, then_r, else_r);
}
if (re().is_union(d, t, e)) {
// (t ∪ e) · tail → (t · tail) ∪ (e · tail)
if (m_antimirov_derivative && re().is_union(d, t, e)) {
expr_ref left = mk_deriv_concat(t, tail);
expr_ref right = mk_deriv_concat(e, tail);
return mk_union(left, right);
@ -1253,8 +1254,10 @@ namespace seq {
void derive::intersect_intervals(unsigned lo, unsigned hi) {
// Copy active suffix to end, update start, then filter
unsigned old_sz = m_intervals.size();
for (unsigned i = m_intervals_start; i < old_sz; ++i)
m_intervals.push_back(m_intervals[i]);
for (unsigned i = m_intervals_start; i < old_sz; ++i) {
auto e = m_intervals[i];
m_intervals.push_back(e);
}
m_intervals_start = old_sz;
// Filter in-place within new suffix: drop intervals disjoint from [lo,hi],
// keep the intersection for overlapping ones.

6
src/ast/rewriter/seq_derive.h
View file

@ -77,6 +77,8 @@ namespace seq {
seq_util::rex& re() { return m_util.re; }
seq_util& u() { return m_util; }
bool m_antimirov_derivative = true;
// The element (character) for the current derivative computation
expr_ref m_ele;
@ -189,6 +191,10 @@ namespace seq {
*/
expr_ref nullable(expr* r) { return is_nullable(r); }
void set_antimirov(bool flag) {
m_antimirov_derivative = flag;
}
};
}