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

Unique name for decomposed regex

Browse source
This commit is contained in:
CEisenhofer 2026-05-28 18:45:48 +02:00
parent e5d5b493d3
commit ff99cb442a
2 changed files with 4 additions and 3 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -3498,8 +3498,8 @@ namespace seq {
VERIFY(m_seq.is_re(stabilizer_re->get_expr(), seq_sort)); VERIFY(m_seq.is_re(stabilizer_re->get_expr(), seq_sort));
// Construct the replacement x = x' x'' // Construct the replacement x = x' x''
euf::snode* xp = mk_fresh_var(x->get_sort()); euf::snode* xp = m_sg.mk(m_sk.mk("cycle", x->get_expr(), stabilizer_re->get_expr(), seq_sort));
euf::snode* xpp = mk_fresh_var(x->get_sort()); euf::snode* xpp = get_tail(x, compute_length_expr(xp).get());
euf::snode* xp_xpp = m_sg.mk_concat(xp, xpp); euf::snode* xp_xpp = m_sg.mk_concat(xp, xpp);
nielsen_node* child = mk_child(node); nielsen_node* child = mk_child(node);

3
src/smt/seq_model.cpp
View file

@ -460,7 +460,8 @@ namespace smt {
expr_ref witness(m); expr_ref witness(m);
// We checked non-emptiness during Nielsen already // We checked non-emptiness during Nielsen already
lbool wr = m_rewriter.some_seq_in_re(re_expr, witness); lbool wr = m_rewriter.some_seq_in_re(re_expr, witness);
if (wr == l_true && witness) { if (wr == l_true) {
SASSERT(witness);
m_trail.push_back(witness); m_trail.push_back(witness);
m_factory->register_value(witness); m_factory->register_value(witness);
return witness; return witness;