mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-13 20:38:43 +00:00
Code Activity

deal with case of unsatisfiable context and bit-vector objectives that are not normalized to maxsmt. Issue #304

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2015-11-11 11:39:34 -05:00
parent 315dc80eb0
commit 2865f60f8c
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);
}
}
// 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) {
@ -1000,7 +1015,10 @@ namespace opt {
switch(obj.m_type) {
case O_MINIMIZE: {
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);
break;
}