mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-03-20 03:53:10 +00:00
Code Activity

Fixed regex witness

Browse source
This commit is contained in:
CEisenhofer 2026-03-19 17:16:29 +01:00
parent d31968f0ad
commit 109ab7d098
2 changed files with 42 additions and 13 deletions
Download patch file Download diff file Expand all files Collapse all files

25
src/ast/rewriter/seq_rewriter.cpp
View file

@ -6112,8 +6112,29 @@ lbool seq_rewriter::some_string_in_re(expr_mark& visited, expr* r, unsigned_vect
// I want this case to be processed first => push it last
// reason: current string is only pruned
SASSERT(low <= high);
str.push_back(low); // ASSERT: low .. high does not intersect with exclude
todo.push_back({ expr_ref(th, m()), str.size(), {}, true });
unsigned ch = low;
bool found = true;
while (true) {
bool advanced = false;
for (auto [l, h] : exclude) {
if (l <= ch && ch <= h) {
if (h >= high) {
found = false;
break;
}
ch = h + 1;
advanced = true;
}
}
if (!found || ch > high)
break;
if (!advanced)
break;
}
if (found && ch <= high) {
str.push_back(ch);
todo.push_back({ expr_ref(th, m()), str.size(), {}, true });
}
}
continue;
}

30
src/smt/seq_model.cpp
View file

@ -137,7 +137,8 @@ namespace smt {
IF_VERBOSE(1, verbose_stream() << "nseq extract_assignments: " << bindings.size() << " bindings\n";);
for (auto const& b : bindings) {
unsigned id = b.first->id();
SASSERT(b.first);
unsigned id = b.first->first()->id();
if (m_var_values.contains(id))
continue;
expr_ref val = snode_to_value(b.second);
@ -278,39 +279,46 @@ namespace smt {
}
expr* seq_model::get_var_value(euf::snode* var) {
SASSERT(var);
unsigned key = var->first()->id();
expr* val = nullptr;
if (m_var_values.find(var->id(), val))
if (m_var_values.find(key, val))
return val;
// unconstrained or regex-constrained: delegate to mk_fresh_value
val = mk_fresh_value(var);
if (val) {
m_trail.push_back(val);
m_var_values.insert(var->id(), val);
m_var_values.insert(key, val);
}
return val;
}
expr* seq_model::mk_fresh_value(euf::snode* var) {
sort* srt = m_seq.str.mk_string_sort();
if (var->get_expr())
srt = var->get_expr()->get_sort();
// check if this variable has regex constraints
euf::snode* re = nullptr;
if (m_var_regex.find(var->id(), re) && re) {
unsigned key = var->first()->id();
if (m_var_regex.find(key, re) && re) {
expr* re_expr = re->get_expr();
SASSERT(re_expr);
expr_ref witness(m);
// We checked non-emptiness during Nielsen already
VERIFY(m_rewriter.some_seq_in_re(re_expr, witness) == l_true && witness);
lbool wr = m_rewriter.some_seq_in_re(re_expr, witness);
if (wr == l_true && witness) {
// std::cout << "Witness for " << mk_pp(var->get_expr(), m) << " in " <<
// mk_pp(re_expr, m) << ": " << mk_pp(witness, m) << std::endl;
m_trail.push_back(witness);
m_factory->register_value(witness);
return witness;
m_trail.push_back(witness);
m_factory->register_value(witness);
return witness;
}
UNREACHABLE();
}
// no regex constraint or witness generation failed: use empty string
sort* srt = m_seq.str.mk_string_sort();
if (var->get_expr())
srt = var->get_expr()->get_sort();
return m_seq.str.mk_empty(srt);
}