mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-07-19 19:02:02 +00:00
Code Activity

improved SLS

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2014-03-20 22:19:30 -07:00
parent 38a915d46f
commit d9796ec030
1 changed files with 9 additions and 2 deletions
Download patch file Download diff file Expand all files Collapse all files

11
src/opt/pb_sls.cpp
View file

@ -180,7 +180,7 @@ namespace smt {
if (m_cancel) { if (m_cancel) {
return l_undef; return l_undef;
} }
IF_VERBOSE(1, verbose_stream() IF_VERBOSE(3, verbose_stream()
<< "(pb.sls violated: " << m_hard_false.num_elems() << "(pb.sls violated: " << m_hard_false.num_elems()
<< " penalty: " << m_penalty << " " << lit << ")\n";); << " penalty: " << m_penalty << " " << lit << ")\n";);
if (m_hard_false.empty() && m_best_penalty.is_zero()) { if (m_hard_false.empty() && m_best_penalty.is_zero()) {
@ -194,18 +194,25 @@ namespace smt {
if (!m_best_assignment.empty()) { if (!m_best_assignment.empty()) {
assignment.reset(); assignment.reset();
assignment.append(m_best_assignment); assignment.append(m_best_assignment);
i = 0;
} }
m_assignment.reset(); m_assignment.reset();
m_assignment.append(assignment); m_assignment.append(assignment);
m_penalty = m_best_penalty;
m_best_assignment.reset(); m_best_assignment.reset();
m_soft_false.reset(); m_soft_false.reset();
m_hard_false.reset();
m_penalty.reset();
for (unsigned i = 0; i < m_soft.size(); ++i) { for (unsigned i = 0; i < m_soft.size(); ++i) {
if (!eval(m_soft[i])) { if (!eval(m_soft[i])) {
m_soft_false.insert(i); m_soft_false.insert(i);
m_penalty += m_weights[i]; m_penalty += m_weights[i];
} }
} }
for (unsigned i = 0; i < m_clauses.size(); ++i) {
if (!eval(m_clauses[i])) {
m_hard_false.insert(i);
}
}
} }
m_assignment.reset(); m_assignment.reset();
m_assignment.append(assignment); m_assignment.append(assignment);