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 branch 'opt' of https://git01.codeplex.com/z3 into opt

Browse source
This commit is contained in:
Nikolaj Bjorner 2014-12-09 20:57:34 +01:00
parent 08cb8b8de8 e9baaa0900
commit f4dfb9ac82
2 changed files with 7 additions and 6 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

3
src/opt/opt_context.cpp
View file

@ -218,6 +218,7 @@ namespace opt {
}
IF_VERBOSE(1, verbose_stream() << "(optimize:sat)\n";);
s.get_model(m_model);
TRACE("opt", model_smt2_pp(tout, m, *m_model, 0););
m_optsmt.setup(*m_opt_solver.get());
update_lower();
switch (m_objectives.size()) {
@ -566,7 +567,7 @@ namespace opt {
and_then(mk_simplify_tactic(m),
mk_propagate_values_tactic(m),
mk_solve_eqs_tactic(m),
mk_elim_uncnstr_tactic(m),
// NB: mk_elim_uncstr_tactic(m) is not sound with soft constraints
mk_simplify_tactic(m));
opt_params optp(m_params);
tactic_ref tac2, tac3;

10
src/opt/optsmt.cpp
View file

@ -124,14 +124,14 @@ namespace opt {
expr_ref_vector ors(m), disj(m);
expr_ref or(m), bound(m.mk_true(), m);
expr_ref fml(m), bound(m.mk_true(), m);
for (unsigned i = 0; i < m_upper.size(); ++i) {
ors.push_back(m_s->mk_ge(i, m_upper[i]));
}
{
solver::scoped_push _push(*m_s);
or = m.mk_or(ors.size(), ors.c_ptr());
m_s->assert_expr(or);
fml = m.mk_or(ors.size(), ors.c_ptr());
m_s->assert_expr(fml);
lbool is_sat = l_true;
while (!m_cancel) {
is_sat = m_s->check_sat(0,0);
@ -149,8 +149,8 @@ namespace opt {
}
}
set_max(m_lower, m_s->get_objective_values(), disj);
or = m.mk_or(ors.size(), ors.c_ptr());
m_s->assert_expr(or);
fml = m.mk_or(ors.size(), ors.c_ptr());
m_s->assert_expr(fml);
}
else if (is_sat == l_undef) {
return l_undef;