mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-18 20:03:38 +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-04-23 08:23:04 +02:00
commit a5ec46b167
1 changed files with 5 additions and 2 deletions
Download patch file Download diff file Expand all files Collapse all files

5
src/tactic/sls/bvsls_opt_engine.cpp
View file

@ -53,11 +53,14 @@ bvsls_opt_engine::optimization_result bvsls_opt_engine::optimize(
tout << fd->get_name() << " := " << mk_ismt2_pp(val, m()) << std::endl; tout << fd->get_name() << " := " << mk_ismt2_pp(val, m()) << std::endl;
}); });
m_hard_tracker.set_model(initial_model); m_hard_tracker.set_model(initial_model);
m_evaluator.update_all();
} }
optimization_result res(m_manager); optimization_result res(m_manager);
lbool is_sat = m_hard_tracker.is_sat() ? l_true : l_undef; lbool is_sat = m_hard_tracker.is_sat() ? l_true : l_undef;
TRACE("sls_opt", tout << "initial model is sat? " << is_sat << std::endl;);
for (m_stats.m_restarts = 0; for (m_stats.m_restarts = 0;
m_stats.m_restarts < m_max_restarts; m_stats.m_restarts < m_max_restarts;
m_stats.m_restarts++) m_stats.m_restarts++)
@ -65,7 +68,7 @@ bvsls_opt_engine::optimization_result bvsls_opt_engine::optimize(
mpz old_best; mpz old_best;
m_mpz_manager.set(old_best, m_best_model_score); m_mpz_manager.set(old_best, m_best_model_score);
if (!is_sat) { if (is_sat != l_true) {
do { do {
checkpoint(); checkpoint();