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

fiddle with phase

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2017-03-02 13:28:17 -08:00
parent c6f943e4d6
commit 9777f43e75
4 changed files with 21 additions and 25 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

7
src/sat/sat_local_search.cpp
View file

@ -670,10 +670,11 @@ namespace sat {
} }
} }
void local_search::set_phase(bool_var v, bool f) { void local_search::set_phase(bool_var v, lbool f) {
unsigned& bias = m_vars[v].m_bias; unsigned& bias = m_vars[v].m_bias;
if (f && bias < 100) bias++; if (f == l_true && bias < 100) bias++;
if (!f && bias > 0) bias--; if (f == l_false && bias > 0) bias--;
// f == l_undef ?
} }
} }

2
src/sat/sat_local_search.h
View file

@ -225,7 +225,7 @@ namespace sat {
unsigned num_vars() const { return m_vars.size() - 1; } // var index from 1 to num_vars unsigned num_vars() const { return m_vars.size() - 1; } // var index from 1 to num_vars
void set_phase(bool_var v, bool f); void set_phase(bool_var v, lbool f);
bool get_phase(bool_var v) const { return is_true(v); } bool get_phase(bool_var v) const { return is_true(v); }

35
src/sat/sat_parallel.cpp
View file

@ -210,20 +210,21 @@ namespace sat {
void parallel::_set_phase(solver& s) { void parallel::_set_phase(solver& s) {
if (!m_phase.empty()) { if (!m_phase.empty()) {
m_phase.reserve(s.num_vars(), 0); m_phase.reserve(s.num_vars(), l_undef);
for (unsigned i = 0; i < s.num_vars(); ++i) { for (unsigned i = 0; i < s.num_vars(); ++i) {
if (s.value(i) != l_undef) { if (s.value(i) != l_undef) {
m_phase[i] += (s.value(i) == l_true) ? 1 : -1; m_phase[i] = s.value(i);
continue; continue;
} }
switch (s.m_phase[i]) { switch (s.m_phase[i]) {
case POS_PHASE: case POS_PHASE:
m_phase[i]++; m_phase[i] = l_true;
break; break;
case NEG_PHASE: case NEG_PHASE:
m_phase[i]--; m_phase[i] = l_false;
break; break;
default: default:
m_phase[i] = l_undef;
break; break;
} }
} }
@ -246,39 +247,33 @@ namespace sat {
void parallel::_get_phase(solver& s) { void parallel::_get_phase(solver& s) {
if (!m_phase.empty()) { if (!m_phase.empty()) {
m_phase.reserve(s.num_vars(), 0); m_phase.reserve(s.num_vars(), l_undef);
for (unsigned i = 0; i < s.num_vars(); ++i) { for (unsigned i = 0; i < s.num_vars(); ++i) {
if (m_phase[i] < 0) { switch (m_phase[i]) {
s.m_phase[i] = NEG_PHASE; case l_false: s.m_phase[i] = NEG_PHASE; break;
} case l_true: s.m_phase[i] = POS_PHASE; break;
else if (m_phase[i] > 0) { default: break;
s.m_phase[i] = POS_PHASE;
} }
} }
} }
} }
void parallel::get_phase(local_search& s) { void parallel::get_phase(local_search& s) {
#pragma omp critical (par_solver) #pragma omp critical (par_solver)
{ {
for (unsigned i = 0; i < m_phase.size(); ++i) { for (unsigned i = 0; i < m_phase.size(); ++i) {
if (m_phase[i] < 0) { s.set_phase(i, m_phase[i]);
s.set_phase(i, false);
}
else if (m_phase[i] > 0) {
s.set_phase(i, true);
}
} }
m_phase.reserve(s.num_vars(), 0); m_phase.reserve(s.num_vars(), l_undef);
} }
} }
void parallel::set_phase(local_search& s) { void parallel::set_phase(local_search& s) {
#pragma omp critical (par_solver) #pragma omp critical (par_solver)
{ {
m_phase.reserve(s.num_vars(), 0); m_phase.reserve(s.num_vars(), l_undef);
for (unsigned i = 0; i < s.num_vars(); ++i) { for (unsigned i = 0; i < s.num_vars(); ++i) {
m_phase[i] += (s.get_phase(i) ? 1 : -1); m_phase[i] = s.get_phase(i) ? l_true : l_false;
} }
} }
} }

2
src/sat/sat_parallel.h
View file

@ -60,7 +60,7 @@ namespace sat {
index_set m_unit_set; index_set m_unit_set;
literal_vector m_lits; literal_vector m_lits;
vector_pool m_pool; vector_pool m_pool;
int_vector m_phase; svector<lbool> m_phase;
scoped_limits m_scoped_rlimit; scoped_limits m_scoped_rlimit;
vector<reslimit> m_limits; vector<reslimit> m_limits;