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

Complement

Browse source
This commit is contained in:
CEisenhofer 2026-06-09 15:12:50 +02:00
parent 9b357373b0
commit 3c39fc4238
1 changed files with 8 additions and 2 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -3627,9 +3627,15 @@ namespace seq {
next.push_back(sigma_pair(seq.re.mk_complement(sp[i].m_p), full, m));
next.push_back(sigma_pair(full, seq.re.mk_complement(sp[i].m_q), m));
sigma_pairs tmp;
if (intersect_sigma_pairs(m, seq, acc, next, tmp, threshold) || tmp.empty())
break;
// De Morgan fold: acc := acc ⊓ ~sp[i]. intersect_sigma_pairs returns
// false ONLY when it overruns the threshold; in that case we must give
// up entirely (a partial fold is a strictly weaker — hence unsound —
// split set, since each ~sp[i] further constrains ~S).
if (!intersect_sigma_pairs(m, seq, acc, next, tmp, threshold))
return false;
acc = std::move(tmp);
if (acc.empty()) // intersection empty ⇒ ~S is empty
break;
if (acc.size() > threshold)
return false;
}