mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-13 20:38:43 +00:00
Code Activity

updates

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2017-03-03 18:09:41 -08:00
parent b5ace71bb8
commit f16dcef7e2
2 changed files with 25 additions and 16 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

34
src/sat/sat_local_search.cpp
View file

@ -223,8 +223,9 @@ namespace sat {
m_vars.reserve(c[i].var() + 1);
literal t(~c[i]);
m_vars[t.var()].m_watch[is_pos(t)].push_back(id);
m_constraints.back().m_literals.push_back(t);
m_constraints.back().push(t);
}
m_constraints.back().seal();
if (sz == 1 && k == 0) {
m_vars[c[0].var()].m_bias = c[0].sign() ? 0 : 100;
}
@ -447,50 +448,55 @@ namespace sat {
SASSERT(c.m_k < constraint_value(c));
if (m_rand() % 100 < 98) {
// take this branch with 98% probability.
// display(std::cout, c);
unsigned best_bsb = 0;
// find the first one, to fast break the rest
unsigned i = 0;
literal const* lits = c.m_literals.c_ptr();
literal l;
while (true) {
v = c[i].var();
if (is_true(c[i])) {
l = *lits;
if (is_true(l)) {
v = l.var();
bool tt = cur_solution(v);
int_vector const& falsep = m_vars[v].m_watch[!tt];
for (unsigned j = 0; j < falsep.size(); ++j) {
unsigned sz = falsep.size();
for (unsigned j = 0; j < sz; ++j) {
unsigned ci = falsep[j];
if (constraint_slack(ci) < 0)
++best_bsb;
else if (constraint_slack(ci) == 0)
// >= unsat_stack_fill_pointer is enough
best_bsb += m_constraints.size();
best_bsb += m_unsat_stack.size();
}
break;
}
++i;
++lits;
}
++lits;
m_good_vars.push_back(v);
for (++i; i < c.size(); ++i) {
v = c[i].var();
if (is_true(c[i])) {
for (; (l = *lits) != null_literal; ++lits) {
if (is_true(l)) {
v = l.var();
bool found = false;
unsigned bsb = 0;
bool tt = cur_solution(v);
int_vector const& falsep = m_vars[v].m_watch[!tt];
for (unsigned j = 0; j < falsep.size() && !found; ++j) {
unsigned sz = falsep.size();
for (unsigned j = 0; j < sz; ++j) {
unsigned ci = falsep[j];
if (constraint_slack(ci) < 0) {
if (bsb == best_bsb) {
found = true;
break;
}
else {
++bsb;
}
}
else if (constraint_slack(ci) == 0) {
// >= unsat_stack_fill_pointer is enough
bsb += m_constraints.size();
bsb += m_unsat_stack.size();
if (bsb > best_bsb) {
found = true;
break;
}
}
}

7
src/sat/sat_local_search.h
View file

@ -94,9 +94,12 @@ namespace sat {
struct constraint {
unsigned m_k;
int m_slack;
unsigned m_size;
literal_vector m_literals;
constraint(unsigned k) : m_k(k), m_slack(0) {}
unsigned size() const { return m_literals.size(); }
constraint(unsigned k) : m_k(k), m_slack(0), m_size(0) {}
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; }
literal const& operator[](unsigned idx) const { return m_literals[idx]; }
};