mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-27 08:28:44 +00:00
Code Activity

fix #4575 - correction set resolution only works with uniform weights

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2020-07-20 15:05:06 -07:00
parent ebce0b3612
commit 1d8d85add9
1 changed files with 9 additions and 4 deletions
Download patch file Download diff file Expand all files Collapse all files

13
src/opt/maxres.cpp
View file

@ -535,14 +535,19 @@ public:
trace(); trace();
if (m_c.num_objectives() == 1 && m_pivot_on_cs && m_csmodel.get() && m_correction_set_size < core.size()) { if (m_c.num_objectives() == 1 && m_pivot_on_cs && m_csmodel.get() && m_correction_set_size < core.size()) {
exprs cs; exprs cs;
TRACE("opt", tout << "cs " << m_correction_set_size << " " << core.size() << "\n";);
get_current_correction_set(m_csmodel.get(), cs); get_current_correction_set(m_csmodel.get(), cs);
m_correction_set_size = cs.size(); m_correction_set_size = cs.size();
if (m_correction_set_size < core.size()) { TRACE("opt", tout << "cs " << m_correction_set_size << " " << core.size() << "\n";);
process_sat(cs); if (m_correction_set_size >= core.size())
return; return;
rational w(0);
for (expr* a : m_asms) {
rational w1 = m_asm2weight[a];
if (w != 0 && w1 != w) return;
w = w1;
} }
} process_sat(cs);
}
} }
bool get_mus_model(model_ref& mdl) { bool get_mus_model(model_ref& mdl) {