mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-03-23 04:49:11 +00:00
Code Activity

port range regular expressions to snode from ZIPT (#9048)

Browse source 
Co-authored-by: copilot-swe-agent[bot] <198982749+Copilot@users.noreply.github.com>
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
This commit is contained in:
Copilot 2026-03-19 15:59:20 -07:00 • committed by GitHub
parent 59bc9b17ea
commit 2ec305f206
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
3 changed files with 16 additions and 2 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -96,6 +96,9 @@ namespace euf {
if (m_seq.re.is_full_seq(e))
return snode_kind::s_full_seq;
if (m_seq.re.is_range(e))
return snode_kind::s_range;
if (m_seq.re.is_to_re(e))
return snode_kind::s_to_re;
@ -252,8 +255,16 @@ namespace euf {
n->m_length = 1;
break;
case snode_kind::s_range:
SASSERT(n->num_args() == 2);
n->m_ground = n->arg(0)->is_ground() && n->arg(1)->is_ground();
n->m_regex_free = false;
n->m_nullable = false;
n->m_level = 1;
n->m_length = 1;
break;
case snode_kind::s_to_re:
// NSB review: are strings nullable or just empty
SASSERT(n->num_args() == 1);
n->m_ground = n->arg(0)->is_ground();
n->m_regex_free = false;
@ -746,6 +757,7 @@ namespace euf {
case snode_kind::s_fail: return "fail";
case snode_kind::s_full_char: return "full_char";
case snode_kind::s_full_seq: return "full_seq";
case snode_kind::s_range: return "range";
case snode_kind::s_to_re: return "to_re";
case snode_kind::s_in_re: return "in_re";
case snode_kind::s_other: return "other";

2
src/ast/euf/euf_sgraph.h
View file

@ -17,7 +17,7 @@ Abstract:
-- snode classification: empty, char, variable, unit, concat, power,
star, loop, union, intersection, complement, fail, full_char,
full_seq, to_re, in_re, other.
full_seq, range, to_re, in_re, other.
-- Metadata computation: ground, regex_free, nullable, level, length.
-- Expression registration via mk(expr*), lookup via find(expr*).
-- Scope management: push/pop with backtracking.

2
src/ast/euf/euf_snode.h
View file

@ -50,6 +50,7 @@ namespace euf {
s_fail, // empty language (OP_RE_EMPTY_SET)
s_full_char, // full character set (OP_RE_FULL_CHAR_SET)
s_full_seq, // full sequence set r=.* (OP_RE_FULL_SEQ_SET)
s_range, // character range [lo,hi] (OP_RE_RANGE)
s_to_re, // string to regex (OP_SEQ_TO_RE)
s_in_re, // regex membership (OP_SEQ_IN_RE)
s_other, // other sequence expression not directly classified
@ -125,6 +126,7 @@ namespace euf {
bool is_fail() const { return m_kind == snode_kind::s_fail; }
bool is_full_char() const { return m_kind == snode_kind::s_full_char; }
bool is_full_seq() const { return m_kind == snode_kind::s_full_seq; }
bool is_range() const { return m_kind == snode_kind::s_range; }
bool is_to_re() const { return m_kind == snode_kind::s_to_re; }
bool is_in_re() const { return m_kind == snode_kind::s_in_re; }