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:22:46 -07:00
parent d9796ec030
commit 25383796c6
1 changed files with 2 additions and 2 deletions
Download patch file Download diff file Expand all files Collapse all files

4
src/opt/pb_sls.cpp
View file

@ -172,7 +172,7 @@ namespace smt {
verbose_stream() << "(pb.sls violated: " << m_hard_false.num_elems() verbose_stream() << "(pb.sls violated: " << m_hard_false.num_elems()
<< " penalty: " << m_penalty << ")\n";); << " penalty: " << m_penalty << ")\n";);
svector<bool> assignment(m_assignment); svector<bool> assignment(m_assignment);
for (unsigned i = 0; i < 20; ++i) { for (unsigned round = 0; round < 40; ++round) {
init_max_flips(); init_max_flips();
while (m_max_flips > 0) { while (m_max_flips > 0) {
--m_max_flips; --m_max_flips;
@ -194,7 +194,7 @@ 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; round = 0;
} }
m_assignment.reset(); m_assignment.reset();
m_assignment.append(assignment); m_assignment.append(assignment);