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

The side-condition of the "if"-split belongs on the edges

Browse source
This commit is contained in:
CEisenhofer 2026-05-12 10:30:29 +02:00
parent bb639af485
commit c9fb432191
5 changed files with 44 additions and 22 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -1443,7 +1443,7 @@ namespace seq {
euf::snode* deriv = fwd
? sg.brzozowski_deriv(mem.m_regex, tok)
: reverse_brzozowski_deriv(sg, mem.m_regex, tok);
TRACE(seq, tout << mem_pp(m, mem) << " d: " << spp(deriv, m) << "\n");
TRACE(seq, tout << mem_pp(mem, m) << " d: " << spp(deriv, m) << "\n");
if (!deriv)
break;
if (deriv->is_fail()) {
@ -1529,7 +1529,7 @@ namespace seq {
// check for regex memberships that are immediately infeasible
for (str_mem& mem : m_str_mem) {
if (mem.is_contradiction(this)) {
TRACE(seq, tout << "contradiction " << mem_pp(m, mem) << "\n");
TRACE(seq, tout << "contradiction " << mem_pp(mem, m) << "\n");
set_general_conflict();
set_conflict(backtrack_reason::regex, mem.m_dep);
return simplify_result::conflict;
@ -3521,7 +3521,7 @@ namespace seq {
for (str_mem const& mem : node->str_mems()) {
SASSERT(mem.well_formed());
if (mem.is_primitive() || !mem.m_regex->is_classical())
if (mem.m_str->is_empty() || mem.is_primitive() || !mem.m_regex->is_classical())
continue;
euf::snode* first = mem.m_str->first();
@ -3529,6 +3529,7 @@ namespace seq {
SASSERT(!first->is_char());
euf::snode* tail = m_sg.drop_first(mem.m_str);
SASSERT(tail);
std::cout << "Processing: " << mem_pp(mem, m) << std::endl;
tau_pairs pairs;
compute_tau(m, m_seq, m_sg, mem.m_regex->get_expr(), pairs);
@ -3913,14 +3914,17 @@ namespace seq {
// No ite remaining: leaf → create child node with regex updated to r
euf::snode *new_regex_snode = m_sg.mk(r);
nielsen_node *child = mk_child(node);
for (auto f : cs)
child->add_constraint(constraint(f, mem.m_dep, m));
mk_edge(node, child, true);
for (str_mem &cm : child->str_mems())
nielsen_edge* e = mk_edge(node, child, true);
for (auto f : cs) {
std::cout << "sc: " << mk_pp(f, m) << std::endl;
e->add_side_constraint(constraint(f, mem.m_dep, m));
}
for (str_mem &cm : child->str_mems()) {
if (cm == mem) {
cm.m_regex = new_regex_snode;
break;
}
}
created = true;
continue;
}
@ -4743,7 +4747,7 @@ namespace seq {
// TODO: Minimize the conflict here
lbool result = m_seq_regex->is_empty_bfs(inter_sn, 5000);
TRACE(seq, tout << "widen empty-intersect: " << result << " " << mk_pp(re, m)
<< " <= " << mk_pp(ae, m) << "\n" << mem_pp(m, mem) << "\n";
<< " <= " << mk_pp(ae, m) << "\n" << mem_pp(mem, m) << "\n";
display(tout, &node) << "\n");
return result == l_true;
}

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

@ -440,9 +440,9 @@ namespace seq {
};
struct mem_pp {
ast_manager &m;
str_mem const& mem;
mem_pp(ast_manager &m, str_mem const&mem) : m(m), mem(mem) {}
ast_manager &m;
mem_pp(str_mem const& mem, ast_manager& m) : m(m), mem(mem) {}
};
inline std::ostream &operator<<(std::ostream &out, mem_pp const &p) {
return out << mk_pp(p.mem.m_str->get_expr(), p.m) << " in " << mk_pp(p.mem.m_regex->get_expr(), p.m) << "\n";
@ -490,9 +490,9 @@ namespace seq {
dep_tracker dep; // tracks which input constraints contributed
static expr_ref simplify(expr* f, ast_manager& m) {
th_rewriter th(m);
//th_rewriter th(m);
expr_ref fml(f, m);
th(fml);
//th(fml);
return fml;
}

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

@ -613,7 +613,7 @@ namespace seq {
SASSERT(first);
if (first != var)
continue;
TRACE(seq, tout << spp(first, m) << " " << mem_pp(m, mem) << "\n");
TRACE(seq, tout << spp(first, m) << " " << mem_pp(mem, m) << "\n");
if (!result) {
result = mem.m_regex;

35
src/smt/theory_nseq.cpp
View file

@ -473,10 +473,12 @@ namespace smt {
if (!get_fparams().m_nseq_regex_factorization_threshold)
return;
std::cout << "Trying " << seq::mem_pp(mem, m);
// Boolean Closure Propagations
expr* re_expr = mem.m_regex->get_expr();
if (m_seq.re.is_intersection(re_expr)) {
std::cout << "Propagating intersection " << seq::mem_pp(mem, m) << std::endl;
for (expr* arg : *to_app(re_expr)) {
expr_ref in_r(m_seq.re.mk_in_re(s_expr, arg), m);
literal_vector lits;
@ -484,8 +486,12 @@ namespace smt {
lits.push_back(mk_literal(in_r));
ctx.mk_th_axiom(get_id(), lits.size(), lits.data());
}
m_ignored_mem.insert(mem.lit);
ctx.push_trail(insert_map(m_ignored_mem, mem.lit));
return;
}
else if (m_seq.re.is_union(re_expr)) {
if (m_seq.re.is_union(re_expr)) {
std::cout << "Propagating union " << seq::mem_pp(mem, m) << std::endl;
literal_vector lits;
lits.push_back(~mem.lit);
for (expr* arg : *to_app(re_expr)) {
@ -493,14 +499,23 @@ namespace smt {
lits.push_back(mk_literal(in_r));
}
ctx.mk_th_axiom(get_id(), lits.size(), lits.data());
m_ignored_mem.insert(mem.lit);
ctx.push_trail(insert_map(m_ignored_mem, mem.lit));
return;
}
else if (m_seq.re.is_complement(re_expr)) {
expr* arg = to_app(re_expr)->get_arg(0);
expr_ref in_r(m_seq.re.mk_in_re(s_expr, arg), m);
literal_vector lits;
lits.push_back(~mem.lit);
lits.push_back(~mk_literal(in_r));
ctx.mk_th_axiom(get_id(), lits.size(), lits.data());
if (m_seq.re.is_to_re(re_expr)) {
return;
zstring s;
expr_ref arg(to_app(re_expr)->get_arg(0), m);
if (m_seq.str.is_string(arg, s)) {
std::cout << "Propagating const matching " << seq::mem_pp(mem, m) << std::endl;
literal_vector lits;
lits.push_back(~mem.lit);
lits.push_back(mk_literal(m.mk_eq(s_expr, arg)));
ctx.mk_th_axiom(get_id(), lits.size(), lits.data());
m_ignored_mem.insert(mem.lit);
ctx.push_trail(insert_map(m_ignored_mem, mem.lit));
}
}
}
@ -618,6 +633,8 @@ namespace smt {
++num_mems;
continue;
}
/*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)) {
@ -997,7 +1014,7 @@ namespace smt {
}
idx = 0;
for (auto& mem : m_nielsen.root()->str_mems()) {
std::cout << "[" << (idx++) << "]: " << seq::mem_pp(m, mem);
std::cout << "[" << (idx++) << "]: " << seq::mem_pp(mem, m);
}
std::flush(std::cout);
#endif

1
src/smt/theory_nseq.h
View file

@ -62,6 +62,7 @@ namespace smt {
unsigned m_prop_qhead = 0;
obj_hashtable<expr> m_axiom_set; // dedup guard for axiom_item enqueues
obj_hashtable<expr> m_no_diseq_set; // track expressions that should not trigger new disequality axioms
hashtable<literal, obj_hash<literal>, default_eq<literal>> m_ignored_mem; // track membership constraints that should not be passed to Nielsen
expr_ref_vector m_relevant_lengths; // track variables whose lengths are relevant
obj_map<expr, unsigned> m_gradient_cache;
sat::literal_vector m_nielsen_literals; // literals created by a Nilsen check