mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-06-19 15:16:29 +00:00
Code Activity

A bit of cleanup

Browse source
This commit is contained in:
CEisenhofer 2026-06-05 20:26:58 +02:00
parent 67906da97a
commit eee5a9dcef
2 changed files with 11 additions and 35 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -937,16 +937,15 @@ namespace seq {
}
void nielsen_graph::record_partial_derivative_edge(euf::snode* src_re, euf::snode* label, euf::snode* dst_re) {
if (!src_re || !dst_re || !src_re->get_expr() || !dst_re->get_expr())
return;
SASSERT(src_re && dst_re);
if (!src_re->is_ground() || !dst_re->is_ground())
return;
if (src_re->is_fail() || dst_re->is_fail())
return;
euf::snode* label_re = to_partial_label_regex(label);
if (!label_re || !label_re->get_expr())
return;
SASSERT(label_re);
if (!m_seq.is_re(label_re->get_expr()) || !label_re->is_ground())
return;
@ -3269,7 +3268,8 @@ namespace seq {
// -----------------------------------------------------------------------
void nielsen_graph::precompute_partial_dfa(euf::snode* root_re, const unsigned depth) {
if (!root_re || !root_re->is_ground())
SASSERT(root_re);
if (!root_re->is_ground())
return;
struct work_item { euf::snode* re; unsigned d; };
@ -3284,6 +3284,7 @@ namespace seq {
euf::snode_vector mts;
m_sg.compute_minterms(re, mts);
for (euf::snode* mt : mts) {
std::cout << "minterm: " << mk_pp(mt->get_expr(), m) << std::endl;
euf::snode* deriv = m_sg.brzozowski_deriv(re, mt);
if (!deriv || deriv->is_fail())
continue;
@ -3294,6 +3295,8 @@ namespace seq {
}
}
}
std::string s = partial_dfa_to_dot(root_re, false);
std::cout << s << std::endl;
}
// -----------------------------------------------------------------------

33
src/smt/theory_nseq.cpp
View file

@ -493,36 +493,6 @@ namespace smt {
return;
}
if (!get_fparams().m_nseq_regex_factorization_threshold)
return;
//if (mem.m_regex->is_intersect()) {
// // u \in r1 & r_2 → u \in r1 && u \in r2
// for (const euf::snode* const arg : *mem.m_regex) {
// expr_ref in_r(m_seq.re.mk_in_re(s, arg->get_expr()), 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());
// }
// m_ignored_mem.insert(mem.lit);
// ctx.push_trail(insert_map(m_ignored_mem, mem.lit));
// return;
//}
//if (mem.m_regex->is_union()) {
// // u \in r1 | r_2 → u \in r1 || u \in r2
// literal_vector lits;
// lits.push_back(~mem.lit);
// for (const euf::snode* const arg : *mem.m_regex) {
// expr_ref in_r(m_seq.re.mk_in_re(s, arg->get_expr()), m);
// 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;
//}
if (mem.m_regex->is_to_re()) {
// u \in v (with v is constant) → u = v
zstring str;
@ -537,6 +507,9 @@ namespace smt {
}
}
if (!get_fparams().m_nseq_regex_factorization_threshold)
return;
// Eager sigma factorization (token-level): when enabled, split a non-primitive
// membership s ∈ r at the boundary between the first concat argument (head) and
// the rest (tail), using compute_sigma. This mirrors the lazy Nielsen