mirror of
https://github.com/Z3Prover/z3
synced 2025-04-08 10:25:18 +00:00
parent
fc73271b83
commit
0589a20b46
|
@ -229,6 +229,7 @@ public:
|
|||
}
|
||||
|
||||
lbool primal_dual_solver() {
|
||||
std::cout << "pd\n";
|
||||
if (!init()) return l_undef;
|
||||
lbool is_sat = init_local();
|
||||
trace();
|
||||
|
@ -315,14 +316,13 @@ public:
|
|||
|
||||
void found_optimum() {
|
||||
IF_VERBOSE(1, verbose_stream() << "found optimum\n";);
|
||||
rational upper(0);
|
||||
m_lower.reset();
|
||||
for (unsigned i = 0; i < m_soft.size(); ++i) {
|
||||
m_assignment[i] = is_true(m_soft[i]);
|
||||
if (!m_assignment[i]) {
|
||||
upper += m_weights[i];
|
||||
m_lower += m_weights[i];
|
||||
}
|
||||
}
|
||||
SASSERT(upper == m_lower);
|
||||
m_upper = m_lower;
|
||||
m_found_feasible_optimum = true;
|
||||
}
|
||||
|
@ -397,10 +397,11 @@ public:
|
|||
void get_current_correction_set(model* mdl, exprs& cs) {
|
||||
cs.reset();
|
||||
if (!mdl) return;
|
||||
for (unsigned i = 0; i < m_asms.size(); ++i) {
|
||||
if (is_false(mdl, m_asms[i].get())) {
|
||||
cs.push_back(m_asms[i].get());
|
||||
for (expr* a : m_asms) {
|
||||
if (is_false(mdl, a)) {
|
||||
cs.push_back(a);
|
||||
}
|
||||
TRACE("opt", expr_ref tmp(m); mdl->eval(a, tmp, true); tout << mk_pp(a, m) << ": " << tmp << "\n";);
|
||||
}
|
||||
TRACE("opt", display_vec(tout << "new correction set: ", cs););
|
||||
}
|
||||
|
@ -509,6 +510,7 @@ public:
|
|||
trace();
|
||||
if (m_c.num_objectives() == 1 && m_pivot_on_cs && m_csmodel.get() && m_correction_set_size < core.size()) {
|
||||
exprs cs;
|
||||
TRACE("opt", tout << "cs " << m_correction_set_size << " " << core.size() << "\n";);
|
||||
get_current_correction_set(m_csmodel.get(), cs);
|
||||
m_correction_set_size = cs.size();
|
||||
if (m_correction_set_size < core.size()) {
|
||||
|
|
|
@ -819,7 +819,7 @@ namespace opt {
|
|||
bool is_max = is_maximize(fml, term, orig_term, index);
|
||||
bool is_min = !is_max && is_minimize(fml, term, orig_term, index);
|
||||
if (is_min && get_pb_sum(term, terms, weights, offset)) {
|
||||
TRACE("opt", tout << "try to convert minimization" << mk_pp(term, m) << "\n";);
|
||||
TRACE("opt", tout << "try to convert minimization\n" << mk_pp(term, m) << "\n";);
|
||||
// minimize 2*x + 3*y
|
||||
// <=>
|
||||
// (assert-soft (not x) 2)
|
||||
|
|
Loading…
Reference in a new issue