mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-15 13:28:47 +00:00
Code Activity

use iterators

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2017-03-03 19:30:44 -08:00
parent f16dcef7e2
commit a7db118ebc
2 changed files with 27 additions and 37 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

63
src/sat/sat_local_search.cpp
View file

@ -225,7 +225,6 @@ namespace sat {
m_vars[t.var()].m_watch[is_pos(t)].push_back(id); m_vars[t.var()].m_watch[is_pos(t)].push_back(id);
m_constraints.back().push(t); m_constraints.back().push(t);
} }
m_constraints.back().seal();
if (sz == 1 && k == 0) { if (sz == 1 && k == 0) {
m_vars[c[0].var()].m_bias = c[0].sign() ? 0 : 100; m_vars[c[0].var()].m_bias = c[0].sign() ? 0 : 100;
} }
@ -443,64 +442,56 @@ namespace sat {
void local_search::pick_flip_walksat() { void local_search::pick_flip_walksat() {
m_good_vars.reset(); m_good_vars.reset();
bool_var v; bool_var v = null_bool_var;
unsigned num_unsat = m_unsat_stack.size();
constraint const& c = m_constraints[m_unsat_stack[m_rand() % m_unsat_stack.size()]]; constraint const& c = m_constraints[m_unsat_stack[m_rand() % m_unsat_stack.size()]];
SASSERT(c.m_k < constraint_value(c)); SASSERT(c.m_k < constraint_value(c));
if (m_rand() % 100 < 98) { if (m_rand() % 100 < 98) {
// take this branch with 98% probability. // take this branch with 98% probability.
unsigned best_bsb = 0;
// find the first one, to fast break the rest // find the first one, to fast break the rest
unsigned i = 0; unsigned best_bsb = 0;
literal const* lits = c.m_literals.c_ptr(); literal_vector::const_iterator cit = c.m_literals.begin(), cend = c.m_literals.end();
literal l; literal l;
while (true) { for (; !is_true(*cit); ++cit) { SASSERT(cit != cend); }
l = *lits; l = *cit;
if (is_true(l)) { v = l.var();
v = l.var(); bool tt = cur_solution(v);
bool tt = cur_solution(v); int_vector const& falsep = m_vars[v].m_watch[!tt];
int_vector const& falsep = m_vars[v].m_watch[!tt]; int_vector::const_iterator it = falsep.begin(), end = falsep.end();
unsigned sz = falsep.size(); for (; it != end; ++it) {
for (unsigned j = 0; j < sz; ++j) { int slack = constraint_slack(*it);
unsigned ci = falsep[j]; if (slack < 0)
if (constraint_slack(ci) < 0) ++best_bsb;
++best_bsb; else if (slack == 0)
else if (constraint_slack(ci) == 0) best_bsb += num_unsat;
best_bsb += m_unsat_stack.size();
}
break;
}
++lits;
} }
++lits;
m_good_vars.push_back(v); m_good_vars.push_back(v);
for (; (l = *lits) != null_literal; ++lits) { ++cit;
for (; cit != cend; ++cit) {
l = *cit;
if (is_true(l)) { if (is_true(l)) {
v = l.var(); v = l.var();
bool found = false;
unsigned bsb = 0; unsigned bsb = 0;
bool tt = cur_solution(v); int_vector const& falsep = m_vars[v].m_watch[!cur_solution(v)];
int_vector const& falsep = m_vars[v].m_watch[!tt]; int_vector::const_iterator it = falsep.begin(), end = falsep.end();
unsigned sz = falsep.size(); for (; it != end; ++it) {
for (unsigned j = 0; j < sz; ++j) { int slack = constraint_slack(*it);
unsigned ci = falsep[j]; if (slack < 0) {
if (constraint_slack(ci) < 0) {
if (bsb == best_bsb) { if (bsb == best_bsb) {
found = true;
break; break;
} }
else { else {
++bsb; ++bsb;
} }
} }
else if (constraint_slack(ci) == 0) { else if (slack == 0) {
bsb += m_unsat_stack.size(); bsb += num_unsat;
if (bsb > best_bsb) { if (bsb > best_bsb) {
found = true;
break; break;
} }
} }
} }
if (!found) { if (it == end) {
if (bsb < best_bsb) { if (bsb < best_bsb) {
best_bsb = bsb; best_bsb = bsb;
m_good_vars.reset(); m_good_vars.reset();

1
src/sat/sat_local_search.h
View file

@ -98,7 +98,6 @@ namespace sat {
literal_vector m_literals; literal_vector m_literals;
constraint(unsigned k) : m_k(k), m_slack(0), m_size(0) {} constraint(unsigned k) : m_k(k), m_slack(0), m_size(0) {}
void push(literal l) { m_literals.push_back(l); ++m_size; } void push(literal l) { m_literals.push_back(l); ++m_size; }
void seal() { m_literals.push_back(null_literal); }
unsigned size() const { return m_size; } unsigned size() const { return m_size; }
literal const& operator[](unsigned idx) const { return m_literals[idx]; } literal const& operator[](unsigned idx) const { return m_literals[idx]; }
}; };