mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-07-25 21:57:00 +00:00
Code Activity

Skip lower bound assertions for unbounded objectives

Browse source
This commit is contained in:
Anh-Dung Phan 2013-12-11 12:56:48 -08:00
parent 1c0442ea31
commit a737639790
1 changed files with 4 additions and 2 deletions
Download patch file Download diff file Expand all files Collapse all files

6
src/opt/optsmt.cpp
View file

@ -291,8 +291,10 @@ namespace opt {
m_lower[i] = mid; m_lower[i] = mid;
m_upper[i] = mid; m_upper[i] = mid;
TRACE("opt", tout << "set lower bound of "; display_objective(tout, i) << " to: " << mid << "\n"; TRACE("opt", tout << "set lower bound of "; display_objective(tout, i) << " to: " << mid << "\n";
tout << get_lower(i) << ":" << get_upper(i) << "\n";); tout << get_lower(i) << ":" << get_upper(i) << "\n";);
m_s->assert_expr(m_s->mk_ge(i, mid)); // Only assert bounds for bounded objectives
if (mid.get_infinity().is_zero())
m_s->assert_expr(m_s->mk_ge(i, mid));
} }
std::ostream& optsmt::display_objective(std::ostream& out, unsigned i) const { std::ostream& optsmt::display_objective(std::ostream& out, unsigned i) const {