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

Bugfix in regex overapproximation

Browse source
This commit is contained in:
CEisenhofer 2026-03-16 19:54:12 +01:00
parent 16f693b09a
commit 84d371f2e9
2 changed files with 25 additions and 27 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -1789,7 +1789,8 @@ namespace seq {
euf::snode* deriv = fwd
? sg.brzozowski_deriv(mem.m_regex, tok)
: reverse_brzozowski_deriv(sg, mem.m_regex, tok);
if (!deriv) break;
if (!deriv)
break;
if (deriv->is_fail()) {
m_is_general_conflict = true;
m_reason = backtrack_reason::regex;
@ -1833,11 +1834,15 @@ namespace seq {
if (!mt || mt->is_fail())
continue;
euf::snode* deriv = sg.brzozowski_deriv(mem.m_regex, mt);
if (!deriv) { is_uniform = false; break; }
if (!uniform) {
if (!deriv) {
is_uniform = false;
break;
}
if (!uniform)
uniform = deriv;
} else if (uniform->id() != deriv->id()) {
is_uniform = false; break;
else if (uniform->id() != deriv->id()) {
is_uniform = false;
break;
}
}
if (is_uniform && uniform) {
@ -4427,17 +4432,17 @@ namespace seq {
if (tok->is_char()) {
// Concrete character → to_re(unit(c))
expr* te = tok->get_expr();
if (!te) return false;
expr_ref unit_s(seq.str.mk_unit(te), mgr);
expr_ref tre(seq.re.mk_to_re(unit_s), mgr);
if (!te)
return false;
expr_ref tre(seq.re.mk_to_re(te), mgr);
tok_re = m_sg.mk(tre);
}
else if (tok->is_var()) {
// Variable → intersection of primitive regex constraints, or Σ*
euf::snode* x_range = m_seq_regex->collect_primitive_regex_intersection(tok, node);
if (x_range) {
if (x_range)
tok_re = x_range;
} else {
else {
// Unconstrained variable: approximate as Σ*
sort* str_sort = seq.str.mk_string_sort();
expr_ref all_re(seq.re.mk_full_seq(seq.re.mk_re(str_sort)), mgr);
@ -4485,12 +4490,14 @@ namespace seq {
if (!tok_re)
return false;
if (!approx) {
if (!approx)
approx = tok_re;
} else {
else {
expr* ae = approx->get_expr();
expr* te = tok_re->get_expr();
if (!ae || !te) return false;
expr* te = tok_re->get_expr(
);
if (!ae || !te)
return false;
expr_ref cat(seq.re.mk_concat(ae, te), mgr);
approx = m_sg.mk(cat);
}

17
src/smt/theory_nseq.cpp
View file

@ -19,9 +19,6 @@ Author:
#include "smt/theory_nseq.h"
#include "smt/smt_context.h"
#include "smt/smt_justification.h"
#include "smt/proto_model/proto_model.h"
#include "ast/array_decl_plugin.h"
#include "ast/ast_pp.h"
#include "util/statistics.h"
#include "util/trail.h"
@ -87,8 +84,9 @@ namespace smt {
bool theory_nseq::internalize_term(app* term) {
// ensure ALL children are internalized (following theory_seq pattern)
for (auto arg : *term)
for (auto arg : *term) {
mk_var(ensure_enode(arg));
}
if (ctx.e_internalized(term)) {
mk_var(ctx.get_enode(term));
@ -102,12 +100,10 @@ namespace smt {
}
enode* en;
if (ctx.e_internalized(term)) {
if (ctx.e_internalized(term))
en = ctx.get_enode(term);
}
else {
else
en = ctx.mk_enode(term, false, m.is_bool(term), true);
}
mk_var(en);
// register in our private sgraph
@ -859,15 +855,10 @@ namespace smt {
// jointly unsatisfiable. Assert a conflict from all their literals.
enode_pair_vector eqs;
literal_vector lits;
std::cout << "CONFLICT:\n";
for (unsigned i : mem_indices) {
mem_source const& src = m_state.get_mem_source(i);
SASSERT(ctx.get_assignment(src.m_lit) == l_true); // we already stored the polarity of the literal
lits.push_back(src.m_lit);
std::cout << "\t\t";
std::cout << mk_pp(ctx.literal2expr(src.m_lit), m) << std::endl;
std::cout << "\t\t";
std::cout << src.m_lit << std::endl;
}
TRACE(seq, tout << "nseq regex precheck: empty intersection for var "
<< var_id << ", conflict with " << lits.size() << " lits\n";);