mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-07-15 03:25:43 +00:00
Code Activity

bug fix

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2026-07-03 11:21:38 -07:00
parent d43d61a4bf
commit f30650b4b4
3 changed files with 108 additions and 25 deletions
Download patch file Download diff file Expand all files Collapse all files

4
src/ast/rewriter/seq_split.cpp
View file

@ -376,8 +376,8 @@ struct split_set::iterator::imp {
}
else if (seq.str.is_unit(a, b)) {
auto eps = mk_eps();
push_split(eps, a);
push_split(a, eps);
push_split(eps, r);
push_split(r, eps);
}
else if (seq.str.is_string(a, str)) {
for (unsigned i = 0; i <= str.length(); ++i) {

82
src/smt/seq_regex.cpp
View file

@ -26,6 +26,83 @@ Author:
namespace smt {
seq_regex::split_cont::split_cont(seq_regex &sr, split_set &&ss, literal lit, expr *u, expr *v, expr *r)
: m_regex(sr), m_u(u), m_v(v), m_split(std::move(ss)), m_it(m_split.begin()), m_end(m_split.end()),
m_in_re2(sr.m), m_lit(lit) {}
bool seq_regex::split_cont::failed() const {
return m_split.failed();
}
bool seq_regex::split_cont::next_split() {
if (m_split.failed())
return false;
auto &ctx = m_regex.ctx;
auto &re = m_regex.re();
auto &m = m_regex.m;
literal lit_undef = null_literal;
for (auto e : m_in_re2) {
auto lit = m_regex.th.mk_literal(e);
auto rel = ctx.is_relevant(lit);
switch (ctx.get_assignment(lit)) {
case l_undef:
lit_undef = lit;
break;
case l_true:
if (!rel)
ctx.mark_as_relevant(lit);
return rel;
case l_false:
break;
}
if (lit_undef != null_literal)
break;
}
if (lit_undef == null_literal) {
while (m_it != m_end) {
auto [pre, post] = *m_it;
auto a = re.mk_in_re(m_u, pre);
auto b = re.mk_in_re(m_v, post);
auto e = m.mk_and(a, b);
m_in_re2.push_back(e);
auto lit = m_regex.th.mk_literal(e);
auto rel = ctx.is_relevant(lit);
switch (ctx.get_assignment(lit)) {
case l_undef: lit_undef = lit; break;
case l_true:
if (!rel)
ctx.mark_as_relevant(lit);
return rel;
case l_false: break;
}
++m_it;
if (lit_undef != null_literal)
break;
}
}
if (m_split.failed())
return false;
if (lit_undef != null_literal) {
ctx.mark_as_relevant(lit_undef);
ctx.force_phase(lit_undef);
return true;
}
// all literals are false:
enode_pair_vector eqs;
literal_vector lits;
lits.push_back(m_lit);
for (auto e : m_in_re2) {
auto lit = m_regex.th.mk_literal(e);
SASSERT(ctx.get_assignment(lit) == l_false);
lits.push_back(~lit);
}
m_regex.th.set_conflict(eqs, lits);
return true;
}
seq_regex::seq_regex(theory_seq& th):
th(th),
ctx(th.get_context()),
@ -368,6 +445,8 @@ namespace smt {
}
bool seq_regex::factor_membership(literal lit) {
if (!th.get_fparams().m_seq_regex_factorization_enabled)
return false;
expr *s = nullptr, *r = nullptr;
expr *e = ctx.bool_var2expr(lit.var());
VERIFY(str().is_in_re(e, s, r));
@ -385,8 +464,7 @@ namespace smt {
// Final check also unfolds this axiomatization
// (we have to add a final check to seq_regex for this).
if (!th.get_fparams().m_seq_regex_factorization_enabled)
return false;
unsigned threshold = th.get_fparams().m_seq_regex_factorization_threshold;
expr_ref_vector prefix(m);

47
src/smt/seq_regex.h
View file

@ -94,27 +94,6 @@ namespace smt {
class theory_seq;
class seq_regex;
// a split continuation is a closure that contains a split set
// and in_re2 literals that were extracted from a partial split.
// there are the following outcomes:
// 1. it was not possible to split:failed()
// 2. one of the in_re2 literals is true: in_re2(u, r1, v, r2) and in_re(u, r1), in_re(v, r2) are true
// 3. one of in_re2(u, r1, v, r2) is true: but in_re(u, r1) or in_re(v, r2) is undef or false.
// 4. all in_re2(u, r1, v, r2) are false: there is a next split from m_split -> add propagation axioms and set phase of in_re2.
// 5. all in_re2(u, r1, v, r2) are false: there is no next split from m_split -> conflict
// split continuations are assigned at scope level and map propagation literal lit to a split continuation.
// they are checked during propagation and during final check.
class split_cont {
split_set m_split;
expr_ref_vector m_in_re2;
public:
split_cont(seq_regex &r, literal lit);
bool failed() const;
bool is_sat();
bool is_unsat();
literal next_split();
};
class seq_regex {
// Data about a constraint of the form (str.in_re s R)
struct s_in_re {
@ -126,6 +105,32 @@ namespace smt {
m_lit(l), m_s(s), m_re(r), m_active(true) {}
};
// a split continuation is a closure that contains a split set
// and in_re2 literals that were extracted from a partial split.
// there are the following outcomes:
// 1. it was not possible to split:failed()
// 2. one of the in_re2 literals is true: in_re2(u, r1, v, r2) and in_re(u, r1), in_re(v, r2) are true
// 3. one of in_re2(u, r1, v, r2) is true: but in_re(u, r1) or in_re(v, r2) is undef or false.
// 4. all in_re2(u, r1, v, r2) are false: there is a next split from m_split -> add propagation axioms and set
// phase of in_re2.
// 5. all in_re2(u, r1, v, r2) are false: there is no next split from m_split -> conflict
// split continuations are assigned at scope level and map propagation literal lit to a split continuation.
// they are checked during propagation and during final check.
class split_cont {
seq_regex &m_regex;
split_set m_split;
expr *m_u, *m_v, *m_r;
split_set::iterator m_it;
split_set::iterator m_end;
expr_ref_vector m_in_re2;
literal m_lit;
public:
split_cont(seq_regex &sr, split_set&& ss, literal lit, expr* u, expr* v, expr* r);
bool failed() const;
bool next_split();
};
theory_seq& th;
context& ctx;
ast_manager& m;