mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-24 09:35:32 +00:00
Code Activity

correct handling of integer vars by NB

Browse source 
Signed-off-by: Lev Nachmanson <levnach@microsoft.com>
This commit is contained in:
Lev Nachmanson 2017-07-06 14:06:33 -07:00
parent 2e95a9d6b2
commit 0e0e9c7041
1 changed files with 12 additions and 5 deletions
Download patch file Download diff file Expand all files Collapse all files

17
src/smt/theory_lra.cpp
View file

@ -314,6 +314,7 @@ namespace smt {
}
}
void found_not_handled(expr* n) {
m_not_handled = n;
if (is_app(n) && is_underspecified(to_app(n))) {
@ -419,9 +420,6 @@ namespace smt {
if (is_app(n)) {
internalize_args(to_app(n));
}
if (a.is_int(n)) {
found_not_handled(n);
}
theory_var v = mk_var(n);
coeffs[vars.size()] = coeffs[index];
vars.push_back(v);
@ -1189,6 +1187,7 @@ namespace smt {
case l_false:
return FC_CONTINUE;
case l_undef:
TRACE("arith", tout << "check-lia giveup\n";);
st = FC_GIVEUP;
break;
}
@ -1199,23 +1198,27 @@ namespace smt {
case l_false:
return FC_CONTINUE;
case l_undef:
TRACE("arith", tout << "check-nra giveup\n";);
st = FC_GIVEUP;
break;
}
if (m_not_handled != 0) {
if (m_not_handled != 0) {
TRACE("arith", tout << "unhandled operator " << mk_pp(m_not_handled, m) << "\n";);
st = FC_GIVEUP;
}
return st;
case l_false:
set_conflict();
return FC_CONTINUE;
case l_undef:
TRACE("arith", tout << "check feasiable is undef\n";);
return m.canceled() ? FC_CONTINUE : FC_GIVEUP;
default:
UNREACHABLE();
break;
}
TRACE("arith", tout << "default giveup\n";);
return FC_GIVEUP;
}
@ -1268,10 +1271,12 @@ namespace smt {
set_conflict1();
return l_false;
case lean::lia_move::give_up:
TRACE("arith", tout << "lia giveup\n";);
return l_undef;
default:
UNREACHABLE();
}
UNREACHABLE();
return l_undef;
}
@ -1294,6 +1299,8 @@ namespace smt {
return l_false;
}
break;
case l_undef:
TRACE("arith", tout << "nra-undef\n";);
default:
break;
}