mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-05-25 11:26:21 +00:00
Code Activity

Make var-nielsen case non-recursive

Browse source
This commit is contained in:
CEisenhofer 2026-05-21 19:12:15 +02:00
parent dafa3cf5bd
commit 2ea1c74071
2 changed files with 6 additions and 8 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -2345,12 +2345,10 @@ namespace seq {
const bool fwd = od == 0;
euf::snode* lhead = dir_token(eq.m_lhs, fwd);
euf::snode* rhead = dir_token(eq.m_rhs, fwd);
if (!lhead || !rhead)
continue;
SASSERT(lhead && rhead);
SASSERT(lhead->id() != rhead->id());
if (!lhead->is_var() || !rhead->is_var())
continue;
if (lhead->id() == rhead->id())
continue;
// x·A = y·B where x,y are distinct variables (classic Nielsen)
// child 1: x → ε (progress)
@ -2371,7 +2369,7 @@ namespace seq {
}
// child 3: x → y·x (no progress)
{
euf::snode* replacement = dir_concat(m_sg, rhead, lhead, fwd);
euf::snode* replacement = dir_concat(m_sg, rhead, get_tail(lhead, compute_length_expr(rhead).get(), fwd), fwd);
nielsen_node* child = mk_child(node);
nielsen_edge* e = mk_edge(node, child, false);
const nielsen_subst s(lhead, replacement,
@ -2382,7 +2380,7 @@ namespace seq {
}
// child 4: y → x·y (no progress)
{
euf::snode* replacement = dir_concat(m_sg, lhead, rhead, fwd);
euf::snode* replacement = dir_concat(m_sg, lhead, get_tail(rhead, compute_length_expr(lhead).get(), fwd), fwd);
nielsen_node* child = mk_child(node);
nielsen_edge* e = mk_edge(node, child, false);
const nielsen_subst s(rhead, replacement,

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

@ -501,9 +501,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;
}