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

current updates

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2017-03-03 17:37:55 -08:00
parent d819784500
commit b5ace71bb8
1 changed files with 24 additions and 20 deletions
Download patch file Download diff file Expand all files Collapse all files

42
src/sat/sat_local_search.cpp
View file

@ -329,24 +329,30 @@ namespace sat {
return check(0, 0); return check(0, 0);
} }
#define PROGRESS(tries, total_steps) \
if (tries % 10 == 0 || m_unsat_stack.empty()) { \
IF_VERBOSE(1, verbose_stream() << "(sat-local-search" \
<< " :tries " << tries \
<< " :steps " << total_steps \
<< " :unsat " << m_unsat_stack.size() \
<< " :time " << timer.get_seconds() << ")\n";); \
}
void local_search::walksat() { void local_search::walksat() {
reinit(); reinit();
timer timer; timer timer;
timer.start(); timer.start();
unsigned step = 0, total_steps = 0, max_steps = (1 << 20); unsigned step = 0, total_steps = 0, max_steps = (1 << 17), tries = 0;
for (unsigned tries = 1; !m_unsat_stack.empty() && m_limit.inc(); ++tries) { PROGRESS(tries, total_steps);
for (tries = 1; !m_unsat_stack.empty() && m_limit.inc(); ++tries) {
for (step = 0; step < max_steps && !m_unsat_stack.empty(); ++step) { for (step = 0; step < max_steps && !m_unsat_stack.empty(); ++step) {
pick_flip_walksat(); pick_flip_walksat();
} }
total_steps += step; total_steps += step;
if (tries % 10 == 0) { PROGRESS(tries, total_steps);
IF_VERBOSE(1, verbose_stream() << "(sat-local-search"
<< " :tries " << tries
<< " :steps " << total_steps
<< " :unsat " << m_unsat_stack.size()
<< " :time " << timer.get_seconds() << ")\n";);
}
} }
PROGRESS(tries, total_steps);
} }
void local_search::gsat() { void local_search::gsat() {
@ -355,10 +361,10 @@ namespace sat {
bool_var flipvar; bool_var flipvar;
timer timer; timer timer;
timer.start(); timer.start();
unsigned tries, step = 0; unsigned tries, step = 0, total_steps = 0;
for (tries = 1; m_limit.inc() && !m_unsat_stack.empty(); ++tries) { for (tries = 1; m_limit.inc() && !m_unsat_stack.empty(); ++tries) {
reinit(); reinit();
for (step = 1; step <= max_steps; ++step) { for (step = 1; step <= max_steps; ) {
// feasible // feasible
if (m_unsat_stack.empty()) { if (m_unsat_stack.empty()) {
calculate_and_update_ob(); calculate_and_update_ob();
@ -368,20 +374,17 @@ namespace sat {
} }
flipvar = pick_var_gsat(); flipvar = pick_var_gsat();
flip_gsat(flipvar); flip_gsat(flipvar);
m_vars[flipvar].m_time_stamp = step; m_vars[flipvar].m_time_stamp = step++;
} }
IF_VERBOSE(1, if (tries % 10 == 0) total_steps += step;
verbose_stream() << "(sat-local-search" PROGRESS(tries, total_steps);
<< " :tries " << tries
<< " :steps " << (tries - 1) * max_steps + step
<< " :unsat " << m_unsat_stack.size()
<< " :time " << timer.get_seconds() << ")\n";);
// tell the SAT solvers about the phase of variables. // tell the SAT solvers about the phase of variables.
if (m_par && tries % 10 == 0) { if (m_par && tries % 10 == 0) {
m_par->get_phase(*this); m_par->get_phase(*this);
} }
} }
PROGRESS(tries, total_steps);
} }
lbool local_search::check(unsigned sz, literal const* assumptions, parallel* p) { lbool local_search::check(unsigned sz, literal const* assumptions, parallel* p) {
@ -442,7 +445,8 @@ namespace sat {
bool_var v; bool_var v;
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 < 5) { if (m_rand() % 100 < 98) {
// take this branch with 98% probability.
// display(std::cout, c); // display(std::cout, c);
unsigned best_bsb = 0; unsigned best_bsb = 0;
// find the first one, to fast break the rest // find the first one, to fast break the rest