mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-15 13:28:47 +00:00
Code Activity

Merge pull request #305 from NikolajBjorner/master

Browse source 
deal with case of unsatisfiable context and bit-vector objectives tha…
This commit is contained in:
Nikolaj Bjorner 2015-11-11 11:41:26 -05:00
parent 1ad45783b1 2865f60f8c
commit be2d215fac
1 changed files with 19 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

20
src/opt/opt_context.cpp
View file

@ -902,6 +902,21 @@ namespace opt {
m_hard_constraints.push_back(fml); m_hard_constraints.push_back(fml);
} }
} }
// fix types of objectives:
for (unsigned i = 0; i < m_objectives.size(); ++i) {
objective & obj = m_objectives[i];
expr* t = obj.m_term;
switch(obj.m_type) {
case O_MINIMIZE:
case O_MAXIMIZE:
if (!m_arith.is_int(t) && !m_arith.is_real(t)) {
obj.m_term = m_arith.mk_numeral(rational(0), true);
}
break;
default:
break;
}
}
} }
void context::purify(app_ref& term) { void context::purify(app_ref& term) {
@ -1000,7 +1015,10 @@ namespace opt {
switch(obj.m_type) { switch(obj.m_type) {
case O_MINIMIZE: { case O_MINIMIZE: {
app_ref tmp(m); app_ref tmp(m);
tmp = m_arith.mk_uminus(obj.m_term); tmp = obj.m_term;
if (m_arith.is_int(tmp) || m_arith.is_real(tmp)) {
tmp = m_arith.mk_uminus(obj.m_term);
}
obj.m_index = m_optsmt.add(tmp); obj.m_index = m_optsmt.add(tmp);
break; break;
} }