mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-03-07 05:44:51 +00:00
Code Activity

Merge pull request #8849 from Z3Prover/copilot/fix-reconcat-classification

Browse source 
sgraph: fix re.concat classification and s_loop nullability
This commit is contained in:
Nikolaj Bjorner 2026-03-03 13:10:39 -08:00 • committed by GitHub
commit a9d0559076
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
1 changed files with 10 additions and 6 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -80,7 +80,7 @@ namespace euf {
return snode_kind::s_other;
}
if (m_seq.str.is_concat(e))
if (m_seq.str.is_concat(e) || m_seq.re.is_concat(e))
return snode_kind::s_concat;
if (m_seq.str.is_unit(e)) {
@ -201,13 +201,17 @@ namespace euf {
break;
case snode_kind::s_loop: {
bool body_nullable = n->num_args() > 0 && n->arg(0)->is_nullable();
unsigned lo = 0, hi = 0;
expr* body = nullptr;
bool lo_zero = n->get_expr() && m_seq.re.is_loop(n->get_expr(), body, lo, hi) && lo == 0;
n->m_ground = n->num_args() > 0 ? n->arg(0)->is_ground() : true;
n->m_regex_free = false;
n->m_nullable = lo_zero || body_nullable;
// nullable iff lower bound is 0: r{0,n} accepts the empty string
// default lo=1 (non-nullable) in case extraction fails
unsigned lo = 1, hi = 1;
expr* loop_body = nullptr;
// try bounded r{lo,hi} first; fall back to unbounded r{lo,}
if (n->get_expr() &&
!m_seq.re.is_loop(n->get_expr(), loop_body, lo, hi))
m_seq.re.is_loop(n->get_expr(), loop_body, lo);
n->m_nullable = (lo == 0);
n->m_level = 1;
n->m_length = 1;
break;