mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-12 12:08:18 +00:00
Code Activity

Fixed bug with VNS repick.

Browse source
This commit is contained in:
Andreas Froehlich 2014-04-22 01:07:30 +01:00 committed by Christoph M. Wintersteiger
parent 8a30a2caa9
commit 39ea6234a4
3 changed files with 22 additions and 9 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
src/tactic/sls/sls_compilation_settings.h
View file

@ -23,7 +23,7 @@ Notes:
#define _SLS_COMPILATION_SETTINGS_H_ #define _SLS_COMPILATION_SETTINGS_H_
// shall we use addition/subtraction? // shall we use addition/subtraction?
#define _USE_ADDSUB_ 0 #define _USE_ADDSUB_ 1
// should we use unsat-structures as done in SLS 4 SAT instead for random or bfs selection? // should we use unsat-structures as done in SLS 4 SAT instead for random or bfs selection?
#define _REAL_RS_ 0 #define _REAL_RS_ 0

22
src/tactic/sls/sls_engine.cpp
View file

@ -68,6 +68,12 @@ void sls_engine::updt_params(params_ref const & _p) {
m_restart_base = p.restart_base(); m_restart_base = p.restart_base();
m_restart_next = m_restart_base; m_restart_next = m_restart_base;
m_restart_init = p.restart_init(); m_restart_init = p.restart_init();
// Andreas: Would cause trouble because repick requires an assertion being picked before which is not the case in GSAT.
if (m_walksat_repick && !m_walksat)
NOT_IMPLEMENTED_YET();
if (m_vns_repick && !m_walksat)
NOT_IMPLEMENTED_YET();
} }
void sls_engine::checkpoint() { void sls_engine::checkpoint() {
@ -435,19 +441,25 @@ lbool sls_engine::search() {
if (m_vns_mc && (new_const == static_cast<unsigned>(-1))) if (m_vns_mc && (new_const == static_cast<unsigned>(-1)))
score = find_best_move_mc(to_evaluate, score, new_const, new_value); score = find_best_move_mc(to_evaluate, score, new_const, new_value);
/*if (m_vns_repick && (new_const == static_cast<unsigned>(-1))) if (m_vns_repick && (new_const == static_cast<unsigned>(-1)))
{ {
expr * q = m_tracker.get_new_unsat_assertion(m_assertions, e); expr * q = m_tracker.get_new_unsat_assertion(m_assertions);
if (q) if (q)
{ {
ptr_vector<func_decl> & to_evaluate2 = m_tracker.get_unsat_constants_walksat(e); ptr_vector<func_decl> & to_evaluate2 = m_tracker.get_unsat_constants_walksat(q);
score = find_best_move(to_evaluate2, score, new_const, new_value, new_bit, move); score = find_best_move(to_evaluate2, score, new_const, new_value, new_bit, move);
if (new_const != static_cast<unsigned>(-1)) {
func_decl * fd = to_evaluate2[new_const];
score = serious_score(fd, new_value);
continue;
}
} }
}*/ }
if (new_const == static_cast<unsigned>(-1)) { if (new_const == static_cast<unsigned>(-1)) {
score = old_score; score = old_score;
if (m_walksat && m_walksat_repick) if (m_walksat_repick)
m_evaluator.randomize_local(m_assertions); m_evaluator.randomize_local(m_assertions);
else else
m_evaluator.randomize_local(to_evaluate); m_evaluator.randomize_local(to_evaluate);

7
src/tactic/sls/sls_tracker.h
View file

@ -76,7 +76,7 @@ private:
ptr_vector<func_decl> m_constants; ptr_vector<func_decl> m_constants;
ptr_vector<func_decl> m_temp_constants; ptr_vector<func_decl> m_temp_constants;
occ_type m_constants_occ; occ_type m_constants_occ;
unsigned m_last_pos;
unsigned m_walksat; unsigned m_walksat;
unsigned m_ucb; unsigned m_ucb;
double m_ucb_constant; double m_ucb_constant;
@ -1082,6 +1082,7 @@ public:
return 0; return 0;
} }
m_last_pos = pos;
return as[pos]; return as[pos];
#if _REAL_RS_ #if _REAL_RS_
//unsigned pos = m_false_list[get_random_uint(16) % m_cnt_false]; //unsigned pos = m_false_list[get_random_uint(16) % m_cnt_false];
@ -1093,7 +1094,7 @@ public:
#endif #endif
} }
expr * get_new_unsat_assertion(ptr_vector<expr> const & as, expr * e) { expr * get_new_unsat_assertion(ptr_vector<expr> const & as) {
unsigned sz = as.size(); unsigned sz = as.size();
if (sz == 1) if (sz == 1)
return 0; return 0;
@ -1101,7 +1102,7 @@ public:
unsigned cnt_unsat = 0, pos = -1; unsigned cnt_unsat = 0, pos = -1;
for (unsigned i = 0; i < sz; i++) for (unsigned i = 0; i < sz; i++)
if (m_mpz_manager.neq(get_value(as[i]), m_one) && (get_random_uint(16) % ++cnt_unsat == 0) && (as[i] != e)) pos = i; if ((i != m_last_pos) && m_mpz_manager.neq(get_value(as[i]), m_one) && (get_random_uint(16) % ++cnt_unsat == 0)) pos = i;
if (pos == static_cast<unsigned>(-1)) if (pos == static_cast<unsigned>(-1))
return 0; return 0;