mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-22 16:45:31 +00:00
Code Activity

preparing for inf extension of arithmetic

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2013-10-31 02:15:08 -07:00
parent 5106c74b3e
commit 637b63cbe1
1 changed files with 16 additions and 14 deletions
Download patch file Download diff file Expand all files Collapse all files

30
src/opt/optimize_objectives.cpp
View file

@ -96,21 +96,23 @@ namespace opt {
lbool optimize_objectives::update_lower() {
lbool is_sat = s->check_sat(0, 0);
set_max(m_lower, s->get_objective_values());
IF_VERBOSE(1,
for (unsigned i = 0; i < m_lower.size(); ++i) {
verbose_stream() << m_lower[i] << " ";
}
verbose_stream() << "\n";);
expr_ref_vector disj(m);
expr_ref constraint(m);
for (unsigned i = 0; i < m_lower.size(); ++i) {
inf_eps const& v = m_lower[i];
disj.push_back(s->block_lower_bound(i, v));
if (is_sat == l_true) {
set_max(m_lower, s->get_objective_values());
IF_VERBOSE(1,
for (unsigned i = 0; i < m_lower.size(); ++i) {
verbose_stream() << m_lower[i] << " ";
}
verbose_stream() << "\n";);
expr_ref_vector disj(m);
expr_ref constraint(m);
for (unsigned i = 0; i < m_lower.size(); ++i) {
inf_eps const& v = m_lower[i];
disj.push_back(s->block_lower_bound(i, v));
}
constraint = m.mk_or(disj.size(), disj.c_ptr());
s->assert_expr(constraint);
}
constraint = m.mk_or(disj.size(), disj.c_ptr());
s->assert_expr(constraint);
return is_sat;
}