mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-05-25 19:36:20 +00:00
Code Activity

re.plus is a regex as well

Browse source
This commit is contained in:
CEisenhofer 2026-05-22 14:03:22 +02:00
parent 2ea1c74071
commit 7ede1b9c3d
3 changed files with 34 additions and 24 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -73,6 +73,9 @@ namespace euf {
if (m_seq.re.is_star(e))
return snode_kind::s_star;
if (m_seq.re.is_plus(e))
return snode_kind::s_plus;
if (m_seq.re.is_loop(e))
return snode_kind::s_loop;
@ -172,6 +175,7 @@ namespace euf {
}
case snode_kind::s_star:
case snode_kind::s_plus:
SASSERT(n->num_args() == 1);
n->m_ground = n->arg(0)->is_ground();
n->m_regex_free = false;
@ -759,6 +763,7 @@ namespace euf {
case snode_kind::s_concat: return "concat";
case snode_kind::s_power: return "power";
case snode_kind::s_star: return "star";
case snode_kind::s_plus: return "plus";
case snode_kind::s_loop: return "loop";
case snode_kind::s_union: return "union";
case snode_kind::s_intersect: return "intersect";

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

@ -45,6 +45,7 @@ namespace euf {
s_concat, // concatenation of two snodes (OP_SEQ_CONCAT)
s_power, // string exponentiation s^n (OP_SEQ_POWER)
s_star, // Kleene star r* (OP_RE_STAR)
s_plus, // Kleene plus r+ (OP_RE_PLUS)
s_loop, // bounded loop r{lo,hi} (OP_RE_LOOP)
s_union, // union r1|r2 (OP_RE_UNION)
s_intersect, // intersection r1&r2 (OP_RE_INTERSECT)
@ -165,6 +166,9 @@ namespace euf {
bool is_star() const {
return m_kind == snode_kind::s_star;
}
bool is_plus() const {
return m_kind == snode_kind::s_plus;
}
bool is_loop() const {
return m_kind == snode_kind::s_loop;
}

49
src/smt/theory_nseq.cpp
View file

@ -613,8 +613,8 @@ namespace smt {
++num_mems;
continue;
}
/*if (m_ignored_mem.contains(mem.lit))
continue; // already handled via Boolean closure, skip*/
if (m_ignored_mem.contains(mem.lit))
continue; // already handled via Boolean closure, skip
// pre-process: consume ground prefix characters
vector<seq::str_mem> processed;
if (!m_regex.process_str_mem(mem, processed)) {
@ -753,31 +753,31 @@ namespace smt {
m_nielsen.set_parikh_enabled(get_fparams().m_nseq_parikh);
m_nielsen.set_signature_split(get_fparams().m_nseq_signature);
m_nielsen.set_regex_factorization_threshold(get_fparams().m_nseq_regex_factorization_threshold);
}
SASSERT(!m_nielsen.root()->is_currently_conflict());
SASSERT(!m_nielsen.root()->is_currently_conflict());
// Regex membership pre-check: before running DFS, check intersection
// emptiness for each variable's regex constraints. This handles
// regex-only problems that the DFS cannot efficiently solve.
if (!m_nielsen.root()->is_currently_conflict() && get_fparams().m_nseq_regex_precheck) {
switch (check_regex_memberships_precheck()) {
case l_true:
// conflict was asserted inside check_regex_memberships_precheck
TRACE(seq, tout << "nseq final_check: regex precheck UNSAT\n");
// Regex membership pre-check: before running DFS, check intersection
// emptiness for each variable's regex constraints. This handles
// regex-only problems that the DFS cannot efficiently solve.
if (!m_nielsen.root()->is_currently_conflict() && get_fparams().m_nseq_regex_precheck) {
switch (check_regex_memberships_precheck()) {
case l_true:
// conflict was asserted inside check_regex_memberships_precheck
TRACE(seq, tout << "nseq final_check: regex precheck UNSAT\n");
return FC_CONTINUE;
case l_false:
// all regex constraints satisfiable, no word eqs → SAT
TRACE(seq, tout << "nseq final_check: regex precheck SAT\n");
m_nielsen.set_sat_node(m_nielsen.root());
if (!check_length_coherence())
return FC_CONTINUE;
case l_false:
// all regex constraints satisfiable, no word eqs → SAT
TRACE(seq, tout << "nseq final_check: regex precheck SAT\n");
m_nielsen.set_sat_node(m_nielsen.root());
if (!check_length_coherence())
return FC_CONTINUE;
if (!check_stoi_coherence())
return FC_CONTINUE;
TRACE(seq, tout << "pre-check done\n");
return FC_DONE;
default:
break;
}
if (!check_stoi_coherence())
return FC_CONTINUE;
TRACE(seq, tout << "pre-check done\n");
return FC_DONE;
default:
break;
}
}
@ -1659,6 +1659,7 @@ namespace smt {
bool theory_nseq::check_length_coherence() {
if (m_relevant_lengths.empty())
// TODO: Make use of this; so far we always introduce lengths always
return true;
SASSERT(m_nielsen.sat_node());