mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-27 10:55:50 +00:00
Code Activity

fixes to failure conditions for unification

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2025-02-16 13:41:17 -08:00
parent fe27ca1dd0
commit 528efbb535
1 changed files with 13 additions and 6 deletions
Download patch file Download diff file Expand all files Collapse all files

19
src/qe/mbp/mbp_euf.cpp
View file

@ -214,7 +214,8 @@ namespace mbp {
expr* x = a->get_arg(i);
expr* y = b->get_arg(i);
todo.push_back({x, y});
}
}
bool failed = false;
while (!todo.empty()) {
auto [x, y] = todo.back();
todo.pop_back();
@ -223,8 +224,10 @@ namespace mbp {
SASSERT(ry);
if (rx == ry)
continue;
if (rx)
break; // fail
if (rx) {
failed = true;
break;
}
if (m_parents[x].size() > 1)
// a crude safey hatch to preserve models
// we could require that every parent of x
@ -233,16 +236,20 @@ namespace mbp {
break;
expr* s = nullptr;
if (soln.find(x, s)) {
if (s != ry)
if (s != ry) {
failed = true;
break;
}
continue;
}
if (is_var(x)) {
soln.insert(x, ry);
continue;
}
if (!same_decl(x, y))
if (!same_decl(x, y)) {
failed = true;
break;
}
app* ax = to_app(x);
app* ay = to_app(y);
for (unsigned i = 0; i < ax->get_num_args(); ++i)
@ -257,7 +264,7 @@ namespace mbp {
);
if (todo.empty() && !soln.empty()) {
if (!failed && todo.empty() && !soln.empty()) {
for (auto [key, value] : soln) {
vars.erase(to_app(key));
defs.push_back( { expr_ref(key, m), expr_ref(value, m) });