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

improve s_loop nullable extraction: clearer comments and sentinel values

Browse source 
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
This commit is contained in:
copilot-swe-agent[bot] 2026-03-03 05:40:16 +00:00
parent 69da8f02c2
commit c0ed79c93b
1 changed files with 3 additions and 1 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -204,8 +204,10 @@ namespace euf {
n->m_ground = n->num_args() > 0 ? n->arg(0)->is_ground() : true; n->m_ground = n->num_args() > 0 ? n->arg(0)->is_ground() : true;
n->m_regex_free = false; n->m_regex_free = false;
// nullable iff lower bound is 0: r{0,n} accepts the empty string // nullable iff lower bound is 0: r{0,n} accepts the empty string
unsigned lo = 1, hi = 0; // default lo=1 (non-nullable) in case extraction fails
unsigned lo = 1, hi = 1;
expr* loop_body = nullptr; expr* loop_body = nullptr;
// try bounded r{lo,hi} first; fall back to unbounded r{lo,}
if (n->get_expr() && 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, hi))
m_seq.re.is_loop(n->get_expr(), loop_body, lo); m_seq.re.is_loop(n->get_expr(), loop_body, lo);