mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-04-05 03:09:01 +00:00
Code Activity

add deterministic solving for unit equations

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2026-03-22 15:33:54 -07:00
parent 6b5401ef68
commit 1863290b71
2 changed files with 18 additions and 2 deletions
Download patch file Download diff file Expand all files Collapse all files

12
src/ast/euf/euf_sgraph.cpp
View file

@ -514,9 +514,17 @@ namespace euf {
if (n->is_empty() || n->is_char())
return n;
if (n->is_concat()) {
return mk_concat(subst(n->arg(0), var, replacement),
subst(n->arg(1), var, replacement));
auto s1 = subst(n->arg(0), var, replacement);
auto s2 = subst(n->arg(1), var, replacement);
if (s1 != n->arg(0) || s2 != n->arg(1))
return mk_concat(s1, s2);
else
return n;
}
// substitution can also work for expressions under unit.
// this unifies two kinds of substitutions used in ZIPT (right Clemens ?).
if (n->is_unit() && n->arg(0) == var)
return mk(m_seq.str.mk_unit(replacement->get_expr()));
// for non-concat compound nodes (power, star, etc.), no substitution into children
return n;
}

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

@ -2546,6 +2546,14 @@ namespace seq {
var = r;
def = l;
}
else if (l->is_unit() && l->arg(0)->is_var() && m_seq.str.is_unit(r->get_expr())) {
var = l->arg(0);
def = r->arg(0);
}
else if (r->is_unit() && r->arg(0)->is_var() && m_seq.str.is_unit(l->get_expr())) {
var = r->arg(0);
def = l->arg(0);
}
if (var) {