mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-05-17 07:29:28 +00:00
Code Activity

tentative solution: use existing nullability check (we might want to check in the future which guards of the ITE are actually true)

Browse source
This commit is contained in:
CEisenhofer 2026-04-14 18:07:03 +02:00
parent f09f6d5097
commit 82df1afeaf
9 changed files with 33 additions and 85 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -166,12 +166,18 @@ namespace seq {
return m_str && m_str->length() == 1 && m_str->is_var() && m_regex->is_ground();
}
bool str_mem::is_trivial() const {
return m_str && m_regex && m_str->is_empty() && m_regex->is_nullable();
bool str_mem::is_trivial(nielsen_node const* n) const {
if (!(m_str && m_regex && m_str->is_empty()))
return false;
const auto& info = n->graph().seq().re.get_info(m_regex->get_expr());
return info.nullable == l_true;
}
bool str_mem::is_contradiction() const {
return (m_str && m_regex && m_str->is_empty() && !m_regex->is_nullable());
bool str_mem::is_contradiction(nielsen_node const* n) const {
if (!(m_str && m_regex && m_str->is_empty()))
return false;
const auto& info = n->graph().seq().re.get_info(m_regex->get_expr());
return info.nullable == l_false;
}
bool str_mem::contains_var(euf::snode* var) const {
@ -825,7 +831,7 @@ namespace seq {
unsigned wj = 0;
for (unsigned j = 0; j < m_str_mem.size(); ++j) {
str_mem& mem = m_str_mem[j];
if (mem.is_trivial())
if (mem.is_trivial(this))
continue;
m_str_mem[wj++] = mem;
}
@ -1136,7 +1142,7 @@ namespace seq {
// check for regex memberships that are immediately infeasible
for (str_mem& mem : m_str_mem) {
if (mem.is_contradiction()) {
if (mem.is_contradiction(this)) {
TRACE(seq, tout << "contradiction " << mem_pp(m, mem) << "\n");
set_general_conflict();
set_conflict(backtrack_reason::regex, mem.m_dep);
@ -1175,7 +1181,7 @@ namespace seq {
bool nielsen_node::is_satisfied() const {
if (any_of(m_str_eq, [](auto const &eq) { return !eq.is_trivial(); }))
return false;
if (any_of(m_str_mem, [](auto const &m) { return !m.is_trivial() && !m.is_primitive();}))
if (any_of(m_str_mem, [this](auto const &m) { return !m.is_trivial(this) && !m.is_primitive();}))
return false;
return true;
}
@ -2418,7 +2424,7 @@ namespace seq {
str_mem const*& mem_out,
bool& fwd) const {
for (str_mem const& mem : node->str_mems()) {
SASSERT(mem.m_str && mem.m_regex && !mem.is_trivial());
SASSERT(mem.m_str && mem.m_regex && !mem.is_trivial(node));
for (unsigned od = 0; od < 2; ++od) {
bool local_fwd = (od == 0);

5
src/smt/seq/seq_nielsen.h
View file

@ -410,9 +410,10 @@ namespace seq {
// check if the constraint has the form x in R with x a single variable
bool is_primitive() const;
bool is_trivial() const;
// TODO: These two functions need to aware of the truth of the ite-guards of the symbolic derivations
bool is_trivial(nielsen_node const* n) const;
bool is_contradiction() const;
bool is_contradiction(nielsen_node const* n) const;
// check if the constraint contains a given variable
bool contains_var(euf::snode* var) const;

54
src/smt/seq/seq_regex.cpp
View file

@ -157,40 +157,6 @@ namespace seq {
// -----------------------------------------------------------------------
bool seq_regex::compute_self_stabilizing(euf::snode* regex) const {
if (!regex)
return false;
// R* is always self-stabilizing: D(c, R*) = D(c,R) · R*,
// so R* appears as the tail of every derivative and acts as
// its own stabilizer.
if (regex->is_star())
return true;
// Σ* (full_seq, i.e., re.all / .*) is self-stabilizing:
// D(c, Σ*) = Σ* for every character c.
if (regex->is_full_seq())
return true;
// ∅ (fail / empty language) is trivially self-stabilizing:
// it has no live derivatives, so the flag is vacuously true.
if (regex->is_fail())
return true;
// Complement of full_seq is ∅ (complement of Σ*), which is
// also trivially self-stabilizing.
if (regex->is_complement() && regex->num_args() == 1 &&
regex->arg(0)->is_full_seq())
return true;
// Loop with lo=0 and no upper bound behaves like R*
// (r{0,} ≡ r*), so it is self-stabilizing.
if (regex->is_loop() && regex->is_nullable()) {
// A nullable loop with a star-like body: heuristic check.
// Only mark as self-stabilizing if the body is a Kleene closure.
// Loop(R, 0, ∞) ~ R* — but we rely on the sgraph to normalize
// these, so only catch exact star nodes above.
}
return false;
}
@ -367,7 +333,7 @@ namespace seq {
re->is_full_char() || re->is_full_seq())
return false;
// loop with lo == 0 accepts ε
if (re->is_loop() && re->is_nullable())
if (re->is_loop() && is_nullable(re))
return false;
expr* e = re->get_expr();
@ -394,7 +360,7 @@ namespace seq {
return true;
// loop(empty, lo, _) with lo > 0 is empty
if (re->is_loop() && re->num_args() >= 1 && is_empty_regex(re->arg(0)))
return !re->is_nullable(); // empty if not nullable (i.e., lo > 0)
return !is_nullable(re); // empty if not nullable (i.e., lo > 0)
return false;
}
@ -497,7 +463,7 @@ namespace seq {
return l_undef;
if (re->is_fail())
return l_true;
if (re->is_nullable())
if (is_nullable(re))
return l_false;
// Structural quick checks for kinds that are never empty
if (re->is_star() || re->is_full_char() || re->is_full_seq() || re->is_to_re() || re->is_range())
@ -554,7 +520,7 @@ namespace seq {
// std::cout << "Deriving by " << snode_label_html(ch, sg().get_manager()) << std::endl;
euf::snode* deriv = m_sg.brzozowski_deriv(current, ch);
SASSERT(deriv);
if (deriv->is_nullable())
if (is_nullable(deriv))
return l_false; // found an accepting state
if (deriv->is_fail())
continue; // dead-end, no need to explore further
@ -699,7 +665,7 @@ namespace seq {
// check final state
if (mem.m_str && mem.m_str->is_empty()) {
if (mem.m_regex->is_nullable())
if (is_nullable(mem.m_regex))
return simplify_status::satisfied;
return simplify_status::conflict;
}
@ -737,7 +703,7 @@ namespace seq {
return 1;
// empty string checks
if (mem.m_str->is_empty()) {
if (mem.m_regex->is_nullable())
if (is_nullable(mem.m_regex))
return 1;
return -1;
}
@ -768,15 +734,15 @@ namespace seq {
}
// -----------------------------------------------------------------------
// Membership processing
// Membership processing
// -----------------------------------------------------------------------
bool seq_regex::process_str_mem(seq::str_mem const& mem,
vector<seq::str_mem>& out_mems) {
bool seq_regex::process_str_mem(str_mem const& mem,
vector<str_mem>& out_mems) {
SASSERT(mem.m_str && mem.m_regex);
// empty string: check nullable
if (mem.m_str->is_empty())
return mem.m_regex->is_nullable();
return is_nullable(mem.m_regex);
// consume ground prefix: derive regex by each leading concrete char
seq::str_mem working = mem;

2
src/smt/seq/seq_regex.h
View file

@ -211,7 +211,7 @@ namespace seq {
// check if regex accepts the empty string
bool is_nullable(euf::snode* re) const {
return re && re->is_nullable();
return re && seq.re.get_info(re->get_expr()).nullable == l_true;
}
// check if regex is ground (no string variables)

2
src/smt/seq_model.cpp
View file

@ -558,7 +558,7 @@ namespace smt {
SASSERT(sat_node);
for (auto const& mem : sat_node->str_mems()) {
SASSERT(mem.m_str && mem.m_regex);
if (mem.is_trivial())
if (mem.is_trivial(sat_node))
continue; // empty string in nullable regex: already satisfied, no variable to constrain
VERIFY(mem.is_primitive()); // everything else should have been eliminated already
euf::snode* first = mem.m_str->first();

2
src/smt/theory_nseq.cpp
View file

@ -423,7 +423,7 @@ namespace smt {
}
// empty string in non-nullable regex → conflict
if (mem.m_str->is_empty() && !mem.m_regex->is_nullable()) {
if (mem.m_str->is_empty() && m_seq.re.get_info(mem.m_regex->get_expr()).nullable == l_false) {
enode_pair_vector eqs;
literal_vector lits;
lits.push_back(mem.lit);