mirror of
https://github.com/Z3Prover/z3
synced 2025-04-07 18:05:21 +00:00
Cleaned up final SLS version. Enjoy!
This commit is contained in:
parent
c4fb21cca1
commit
b3924d85ed
|
@ -1,28 +0,0 @@
|
|||
/*++
|
||||
Copyright (c) 2014 Microsoft Corporation
|
||||
|
||||
Module Name:
|
||||
|
||||
sls_compilation_constants.h
|
||||
|
||||
Abstract:
|
||||
|
||||
Stochastic Local Search (SLS) compilation constants
|
||||
|
||||
Author:
|
||||
|
||||
Christoph (cwinter) 2014-03-19
|
||||
|
||||
Notes:
|
||||
|
||||
This file should go away completely once we have evaluated all options.
|
||||
|
||||
--*/
|
||||
|
||||
#ifndef _SLS_COMPILATION_SETTINGS_H_
|
||||
#define _SLS_COMPILATION_SETTINGS_H_
|
||||
|
||||
// should we use unsat-structures as done in SLS 4 SAT?
|
||||
#define _REAL_RS_ 0
|
||||
|
||||
#endif
|
|
@ -71,6 +71,8 @@ void sls_engine::updt_params(params_ref const & _p) {
|
|||
m_restart_init = p.restart_init();
|
||||
|
||||
m_early_prune = p.early_prune();
|
||||
m_random_offset = p.random_offset();
|
||||
m_rescore = p.rescore();
|
||||
|
||||
// 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)
|
||||
|
@ -174,6 +176,9 @@ bool sls_engine::what_if(
|
|||
m_mpz_manager.del(old_value);
|
||||
#endif
|
||||
|
||||
// Andreas: Had this idea on my last day. Maybe we could add a noise here similar to the one that worked so well for ucb assertion selection.
|
||||
// r += 0.0001 * m_tracker.get_random_uint(8);
|
||||
|
||||
// Andreas: For some reason it is important to use > here instead of >=. Probably related to prefering the LSB.
|
||||
if (r > best_score) {
|
||||
best_score = r;
|
||||
|
@ -248,9 +253,15 @@ void sls_engine::mk_random_move(ptr_vector<func_decl> & unsat_constants)
|
|||
{
|
||||
if (m_mpz_manager.is_one(m_tracker.get_random_bool())) rnd_mv = 2;
|
||||
if (m_mpz_manager.is_one(m_tracker.get_random_bool())) rnd_mv++;
|
||||
|
||||
// Andreas: The other option would be to scale the probability for flips according to the bit-width.
|
||||
/* unsigned bv_sz2 = m_bv_util.get_bv_size(srt);
|
||||
rnd_mv = m_tracker.get_random_uint(16) % (bv_sz2 + 3);
|
||||
if (rnd_mv > 3) rnd_mv = 0; */
|
||||
|
||||
move_type mt = (move_type)rnd_mv;
|
||||
|
||||
// inversion doesn't make sense, let's do a flip instead.
|
||||
// Andreas: Christoph claimed inversion doesn't make sense, let's do a flip instead. Is this really true?
|
||||
if (mt == MV_INV) mt = MV_FLIP;
|
||||
unsigned bit = 0;
|
||||
|
||||
|
@ -306,10 +317,13 @@ double sls_engine::find_best_move(
|
|||
unsigned bv_sz;
|
||||
double new_score = score;
|
||||
|
||||
//unsigned offset = m_tracker.get_random_uint(16) % to_evaluate.size();
|
||||
//for (unsigned j = 0; j < to_evaluate.size(); j++) {
|
||||
//unsigned i = (j + offset) % to_evaluate.size();
|
||||
for (unsigned i = 0; i < to_evaluate.size(); i++) {
|
||||
// Andreas: Introducting a bit of randomization by using a random offset and a random direction to go through the candidate list.
|
||||
unsigned sz = to_evaluate.size();
|
||||
unsigned offset = (m_random_offset) ? m_tracker.get_random_uint(16) % sz : 0;
|
||||
for (unsigned j = 0; j < sz; j++) {
|
||||
unsigned i = j + offset;
|
||||
if (i >= sz) i -= sz;
|
||||
//for (unsigned i = 0; i < to_evaluate.size(); i++) {
|
||||
func_decl * fd = to_evaluate[i];
|
||||
sort * srt = fd->get_range();
|
||||
bv_sz = (m_manager.is_bool(srt)) ? 1 : m_bv_util.get_bv_size(srt);
|
||||
|
@ -361,7 +375,13 @@ double sls_engine::find_best_move_mc(ptr_vector<func_decl> & to_evaluate, double
|
|||
unsigned bv_sz;
|
||||
double new_score = score;
|
||||
|
||||
for (unsigned i = 0; i < to_evaluate.size(); i++) {
|
||||
// Andreas: Introducting a bit of randomization by using a random offset and a random direction to go through the candidate list.
|
||||
unsigned sz = to_evaluate.size();
|
||||
unsigned offset = (m_random_offset) ? m_tracker.get_random_uint(16) % sz : 0;
|
||||
for (unsigned j = 0; j < sz; j++) {
|
||||
unsigned i = j + offset;
|
||||
if (i >= sz) i -= sz;
|
||||
//for (unsigned i = 0; i < to_evaluate.size(); i++) {
|
||||
func_decl * fd = to_evaluate[i];
|
||||
sort * srt = fd->get_range();
|
||||
bv_sz = (m_manager.is_bool(srt)) ? 1 : m_bv_util.get_bv_size(srt);
|
||||
|
@ -405,15 +425,16 @@ lbool sls_engine::search() {
|
|||
while (check_restart(m_stats.m_moves)) {
|
||||
checkpoint();
|
||||
m_stats.m_moves++;
|
||||
|
||||
// Andreas: Every base restart interval ...
|
||||
if (m_stats.m_moves % m_restart_base == 0)
|
||||
{
|
||||
// ... potentially smooth the touched counters ...
|
||||
m_tracker.ucb_forget(m_assertions);
|
||||
//score = rescore();
|
||||
// ... or normalize the top-level score.
|
||||
if (m_rescore) score = rescore();
|
||||
}
|
||||
|
||||
#if _REAL_RS_
|
||||
//m_tracker.debug_real(g, m_stats.m_moves);
|
||||
#endif
|
||||
// get candidate variables
|
||||
ptr_vector<func_decl> & to_evaluate = m_tracker.get_unsat_constants(m_assertions);
|
||||
if (!to_evaluate.size())
|
||||
|
@ -513,8 +534,6 @@ void sls_engine::operator()(goal_ref const & g, model_converter_ref & mc) {
|
|||
for (unsigned i = 0; i < g->size(); i++)
|
||||
assert_expr(g->form(i));
|
||||
|
||||
verbose_stream() << "_REAL_RS_ " << _REAL_RS_ << std::endl;
|
||||
|
||||
lbool res = operator()();
|
||||
|
||||
if (res == l_true) {
|
||||
|
|
|
@ -82,6 +82,8 @@ protected:
|
|||
unsigned m_restart_next;
|
||||
unsigned m_restart_init;
|
||||
unsigned m_early_prune;
|
||||
unsigned m_random_offset;
|
||||
unsigned m_rescore;
|
||||
|
||||
typedef enum { MV_FLIP = 0, MV_INC, MV_DEC, MV_INV } move_type;
|
||||
|
||||
|
|
|
@ -22,7 +22,6 @@ Notes:
|
|||
|
||||
#include"model_evaluator.h"
|
||||
|
||||
#include"sls_compilation_settings.h"
|
||||
#include"sls_powers.h"
|
||||
#include"sls_tracker.h"
|
||||
|
||||
|
@ -540,19 +539,16 @@ public:
|
|||
(*this)(to_app(cur), new_value);
|
||||
m_tracker.set_value(cur, new_value);
|
||||
|
||||
#if _REAL_RS_
|
||||
new_score = m_tracker.score(cur);
|
||||
if (m_tracker.is_top_expr(cur))
|
||||
{
|
||||
m_tracker.adapt_top_sum(cur, new_score, m_tracker.get_score(cur));
|
||||
if (m_mpz_manager.eq(new_value,m_one))
|
||||
m_tracker.make_assertion(cur);
|
||||
else
|
||||
m_tracker.break_assertion(cur);
|
||||
}
|
||||
#endif
|
||||
|
||||
new_score = m_tracker.score(cur);
|
||||
if (m_tracker.is_top_expr(cur))
|
||||
m_tracker.adapt_top_sum(cur, new_score, m_tracker.get_score(cur));
|
||||
m_tracker.set_score(cur, new_score);
|
||||
m_tracker.set_score_prune(cur, new_score);
|
||||
|
||||
|
|
|
@ -8,15 +8,19 @@ def_module_params('sls',
|
|||
('walksat_ucb_constant', DOUBLE, 20.0, 'the ucb constant c in the term score + c * f(touched)'),
|
||||
('walksat_ucb_init', BOOL, 0, 'initialize total ucb touched to formula size'),
|
||||
('walksat_ucb_forget', DOUBLE, 1.0, 'scale touched by this factor every base restart interval'),
|
||||
('walksat_ucb_noise', DOUBLE, 0.0002, 'add noise 0 <= 256 * ucb_noise to ucb score for assertion selection'),
|
||||
('walksat_repick', BOOL, 1, 'repick assertion if randomizing in local minima'),
|
||||
('scale_unsat', DOUBLE, 0.5, 'scale score of unsat expressions by this factor'),
|
||||
('paws_init', UINT, 40, 'initial/minimum assertion weights'),
|
||||
('paws_sp', UINT, 52, 'smooth assertion weights with probability paws_sp / 1024'),
|
||||
('wp', UINT, 0, 'random walk with probability wp / 1024'),
|
||||
('wp', UINT, 100, 'random walk with probability wp / 1024'),
|
||||
('vns_mc', UINT, 0, 'in local minima, try Monte Carlo sampling vns_mc many 2-bit-flips per bit'),
|
||||
('vns_repick', BOOL, 0, 'in local minima, try picking a different assertion (only for walksat)'),
|
||||
('restart_base', UINT, 100, 'base restart interval given by moves per run'),
|
||||
('restart_init', BOOL, 0, 'initialize to 0 or random value (= 1) after restart'),
|
||||
('early_prune', BOOL, 1, 'use early pruning for score prediction'),
|
||||
('random_offset', BOOL, 1, 'use random offset vor candidate evaluation'),
|
||||
('rescore', BOOL, 1, 'rescore/normalize top-level score every base restart interval'),
|
||||
('track_unsat', BOOL, 0, 'keep a list of unsat assertions as done in SAT - currently disabled internally'),
|
||||
('random_seed', UINT, 0, 'random seed')
|
||||
))
|
||||
|
|
|
@ -80,14 +80,13 @@ private:
|
|||
double m_ucb_constant;
|
||||
unsigned m_ucb_init;
|
||||
double m_ucb_forget;
|
||||
double m_ucb_noise;
|
||||
unsigned m_touched;
|
||||
double m_scale_unsat;
|
||||
unsigned m_paws_init;
|
||||
#if _REAL_RS_
|
||||
ptr_vector<expr> m_unsat_expr;
|
||||
obj_map<expr, unsigned> m_where_false;
|
||||
expr** m_list_false;
|
||||
#endif
|
||||
unsigned m_track_unsat;
|
||||
obj_map<expr, unsigned> m_weights;
|
||||
double m_top_sum;
|
||||
|
||||
|
@ -116,8 +115,12 @@ public:
|
|||
m_ucb_constant = p.walksat_ucb_constant();
|
||||
m_ucb_init = p.walksat_ucb_init();
|
||||
m_ucb_forget = p.walksat_ucb_forget();
|
||||
m_ucb_noise = p.walksat_ucb_noise();
|
||||
m_scale_unsat = p.scale_unsat();
|
||||
m_paws_init = p.paws_init();
|
||||
// Andreas: track_unsat is currently disabled because I cannot guarantee that it is not buggy.
|
||||
// If you want to use it, you will also need to change comments in the assertion selection.
|
||||
m_track_unsat = 0;//p.track_unsat();
|
||||
}
|
||||
|
||||
/* Andreas: Tried to give some measure for the formula size by the following two methods but both are not used currently.
|
||||
|
@ -254,53 +257,6 @@ public:
|
|||
return m_uplinks.find(n);
|
||||
}
|
||||
|
||||
#if _REAL_RS_
|
||||
void debug_real(goal_ref const & g, unsigned flip)
|
||||
{
|
||||
unsigned count = 0;
|
||||
for (unsigned i = 0; i < g->size(); i++)
|
||||
{
|
||||
expr * e = g->form(i);
|
||||
if (m_mpz_manager.eq(get_value(e),m_one) && m_where_false.contains(e))
|
||||
{
|
||||
printf("iteration %d: ", flip);
|
||||
printf("form %d is sat but in unsat list at position %d of %d\n", i, m_where_false.find(e), m_where_false.size());
|
||||
exit(4);
|
||||
}
|
||||
|
||||
if (m_mpz_manager.eq(get_value(e),m_zero) && !m_where_false.contains(e))
|
||||
{
|
||||
printf("iteration %d: ", flip);
|
||||
printf("form %d is unsat but not in unsat list\n", i);
|
||||
exit(4);
|
||||
}
|
||||
|
||||
if (m_mpz_manager.eq(get_value(e),m_zero) && m_where_false.contains(e))
|
||||
{
|
||||
unsigned pos = m_where_false.find(e);
|
||||
expr * q = m_list_false[pos];
|
||||
if (q != e)
|
||||
{
|
||||
printf("iteration %d: ", flip);
|
||||
printf("form %d is supposed to be at pos %d in unsat list but something else was there\n", i, pos);
|
||||
exit(4);
|
||||
}
|
||||
}
|
||||
|
||||
if (m_mpz_manager.eq(get_value(e),m_zero))
|
||||
count++;
|
||||
}
|
||||
|
||||
// should be true now that duplicate assertions are removed
|
||||
if (count != m_where_false.size())
|
||||
{
|
||||
printf("iteration %d: ", flip);
|
||||
printf("%d are unsat but list is of size %d\n", count, m_where_false.size());
|
||||
exit(4);
|
||||
}
|
||||
}
|
||||
#endif
|
||||
|
||||
inline void ucb_forget(ptr_vector<expr> & as) {
|
||||
if (m_ucb_forget < 1.0)
|
||||
{
|
||||
|
@ -474,14 +430,15 @@ public:
|
|||
|
||||
TRACE("sls", tout << "Initial model:" << std::endl; show_model(tout); );
|
||||
|
||||
#if _REAL_RS_
|
||||
m_list_false = new expr*[sz];
|
||||
//for (unsigned i = 0; i < sz; i++)
|
||||
//{
|
||||
// if (m_mpz_manager.eq(get_value(g->form(i)),m_zero))
|
||||
// break_assertion(g->form(i));
|
||||
//}
|
||||
#endif
|
||||
if (m_track_unsat)
|
||||
{
|
||||
m_list_false = new expr*[sz];
|
||||
for (unsigned i = 0; i < sz; i++)
|
||||
{
|
||||
if (m_mpz_manager.eq(get_value(as[i]), m_zero))
|
||||
break_assertion(as[i]);
|
||||
}
|
||||
}
|
||||
|
||||
for (unsigned i = 0; i < sz; i++)
|
||||
{
|
||||
|
@ -515,44 +472,36 @@ public:
|
|||
return m_weights.find(e);
|
||||
}
|
||||
|
||||
#if _REAL_RS_
|
||||
void make_assertion(expr * e)
|
||||
{
|
||||
if (m_where_false.contains(e))
|
||||
if (m_track_unsat)
|
||||
{
|
||||
unsigned pos = m_where_false.find(e);
|
||||
m_where_false.erase(e);
|
||||
if (pos != m_where_false.size())
|
||||
if (m_where_false.contains(e))
|
||||
{
|
||||
expr * q = m_list_false[m_where_false.size()];
|
||||
m_list_false[pos] = q;
|
||||
m_where_false.find(q) = pos;
|
||||
//printf("Moving %d from %d to %d\n", q, m_where_false.size(), pos);
|
||||
unsigned pos = m_where_false.find(e);
|
||||
m_where_false.erase(e);
|
||||
if (pos != m_where_false.size())
|
||||
{
|
||||
expr * q = m_list_false[m_where_false.size()];
|
||||
m_list_false[pos] = q;
|
||||
m_where_false.find(q) = pos;
|
||||
}
|
||||
}
|
||||
//else
|
||||
//printf("Erasing %d from %d to %d\n", e, pos);
|
||||
// m_list_false[m_where_false.size()] = 0;
|
||||
// printf("Going in %d\n", m_where_false.size());
|
||||
}
|
||||
//if (m_unsat_expr.contains(e))
|
||||
//m_unsat_expr.erase(e);
|
||||
}
|
||||
|
||||
void break_assertion(expr * e)
|
||||
{
|
||||
//printf("I'm broken... that's still fine.\n");
|
||||
if (!m_where_false.contains(e))
|
||||
if (m_track_unsat)
|
||||
{
|
||||
//printf("This however is not so cool...\n");
|
||||
unsigned pos = m_where_false.size();
|
||||
m_list_false[pos] = e;
|
||||
m_where_false.insert(e, pos);
|
||||
// printf("Going in %d\n", m_where_false.size());
|
||||
if (!m_where_false.contains(e))
|
||||
{
|
||||
unsigned pos = m_where_false.size();
|
||||
m_list_false[pos] = e;
|
||||
m_where_false.insert(e, pos);
|
||||
}
|
||||
}
|
||||
//if (!m_unsat_expr.contains(e))
|
||||
//m_unsat_expr.push_back(e);
|
||||
}
|
||||
#endif
|
||||
|
||||
void show_model(std::ostream & out) {
|
||||
unsigned sz = get_num_constants();
|
||||
|
@ -1043,24 +992,38 @@ public:
|
|||
{
|
||||
value_score vscore;
|
||||
double max = -1.0;
|
||||
// Andreas: Commented things here might be used for track_unsat data structures as done in SLS for SAT. But seems to have no benefit.
|
||||
/* for (unsigned i = 0; i < m_where_false.size(); i++) {
|
||||
expr * e = m_list_false[i]; */
|
||||
for (unsigned i = 0; i < sz; i++) {
|
||||
expr * e = as[i];
|
||||
// for (unsigned i = 0; i < m_where_false.size(); i++) {
|
||||
// expr * e = m_list_false[i];
|
||||
vscore = m_scores.find(e);
|
||||
//double q = vscore.score + m_ucb_constant * sqrt(log((double)m_touched) / vscore.touched);
|
||||
double q = vscore.score + m_ucb_constant * sqrt(log((double)m_touched) / vscore.touched) + (get_random_uint(8) * 0.0000002);
|
||||
if (q > max && m_mpz_manager.neq(get_value(e), m_one) ) { max = q; pos = i; }
|
||||
if (m_mpz_manager.neq(get_value(e), m_one))
|
||||
{
|
||||
vscore = m_scores.find(e);
|
||||
// Andreas: Select the assertion with the greatest ucb score. Potentially add some noise.
|
||||
// double q = vscore.score + m_ucb_constant * sqrt(log((double)m_touched) / vscore.touched);
|
||||
double q = vscore.score + m_ucb_constant * sqrt(log((double)m_touched) / vscore.touched) + m_ucb_noise * get_random_uint(8);
|
||||
if (q > max) { max = q; pos = i; }
|
||||
}
|
||||
}
|
||||
if (pos == static_cast<unsigned>(-1))
|
||||
return 0;
|
||||
|
||||
m_scores.find(as[pos]).touched++;
|
||||
m_touched++;
|
||||
// return m_list_false[pos];
|
||||
m_scores.find(as[pos]).touched++;
|
||||
// Andreas: Also part of track_unsat data structures. Additionally disable the previous line!
|
||||
/* m_last_pos = pos;
|
||||
m_scores.find(m_list_false[pos]).touched++;
|
||||
return m_list_false[pos]; */
|
||||
}
|
||||
else
|
||||
{
|
||||
// Andreas: The track_unsat data structures for random assertion selection.
|
||||
/* sz = m_where_false.size();
|
||||
if (sz == 0)
|
||||
return 0;
|
||||
return m_list_false[get_random_uint(16) % sz]; */
|
||||
|
||||
unsigned cnt_unsat = 0;
|
||||
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)) pos = i;
|
||||
|
@ -1070,14 +1033,6 @@ public:
|
|||
|
||||
m_last_pos = pos;
|
||||
return as[pos];
|
||||
#if _REAL_RS_
|
||||
//unsigned pos = m_false_list[get_random_uint(16) % m_cnt_false];
|
||||
//expr * e = m_unsat_expr[get_random_uint(16) % m_unsat_expr.size()];
|
||||
sz = m_where_false.size();
|
||||
if (sz == 0)
|
||||
return 0;
|
||||
return m_list_false[get_random_uint(16) % sz];
|
||||
#endif
|
||||
}
|
||||
|
||||
expr * get_new_unsat_assertion(ptr_vector<expr> const & as) {
|
||||
|
|
Loading…
Reference in a new issue