mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-07-05 14:56:11 +00:00
Code Activity

sigma of full_seq was missing

Browse source
This commit is contained in:
CEisenhofer 2026-06-09 15:49:41 +02:00
parent 069068ce5e
commit 64f422abc5
1 changed files with 6 additions and 0 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -3690,6 +3690,11 @@ namespace seq {
result.push_back(sigma_pair(ex, eps, m)); result.push_back(sigma_pair(ex, eps, m));
return true; return true;
} }
if (r->is_full_seq()) {
const expr_ref ex(r->get_expr(), m);
result.push_back(sigma_pair(ex, ex, m));
return true;
}
if (r->is_union()) { if (r->is_union()) {
// σ(r₁ ⊔ r₂) = σ(r₁) ∪ σ(r₂) // σ(r₁ ⊔ r₂) = σ(r₁) ∪ σ(r₂)
SASSERT(r->num_args() >= 2); SASSERT(r->num_args() >= 2);
@ -3795,6 +3800,7 @@ namespace seq {
} }
// the simplifier should have eliminated most of them already // the simplifier should have eliminated most of them already
// TODO: so far, we are, however, still missing bounded repetitions and ite // TODO: so far, we are, however, still missing bounded repetitions and ite
std::cout << "Unknown element " << mk_pp(r->get_expr(), m) << std::endl;
return false; return false;
} }