mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-15 21:38:44 +00:00
Code Activity

Almost cleaned up version.

Browse source
This commit is contained in:
Andreas Froehlich 2014-04-22 00:32:45 +01:00
parent 5ab65d52a6
commit c1741d7941
6 changed files with 177 additions and 490 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -22,83 +22,13 @@ Notes:
#ifndef _SLS_COMPILATION_SETTINGS_H_
#define _SLS_COMPILATION_SETTINGS_H_
// how many terms are considered for variable selection?
// 0 = all terms (GSAT), 1 = only one top level assertion (WSAT)
#define _FOCUS_ 1
// shall we use additive weighting scheme?
#define _PAWS_ 5
#define _PAWS_INIT_ 40
// do we use restarts?
// 0 = no, 1 = use #moves, 2 = use #plateaus, 3 = use time
#define _RESTARTS_ 1
// limit of moves/plateaus/seconds until first restart occurs
#define _RESTART_LIMIT_ 100
//// 0 = initialize with all zero, 1 initialize with random value
#define _RESTART_INIT_ 0
// 0 = even intervals, 1 = pseudo luby, 2 = real luby, 3 = armin, 4 = rapid, 5 = minisat
#define _RESTART_SCHEME_ 1
// base value c for armin restart scheme using c^inner - only applies for _RESTART_SCHEME_ 3
#define _RESTART_CONST_ARMIN_ 2.0
// timelimit
#define _TIMELIMIT_ 3600
// should score of conjunctions be calculated by average rather than max?
#define _SCORE_AND_AVG_ 0
// shall we check 2-bit flips in plateaus using Monte Carlo?
#define _VNS_MC_ 0
// how many 2-bit flips shall we try per bit?
#define _VNS_MC_TRIES_ 1
// shall we check another assertion if no improving step was found in the first one?
#define _VNS_REPICK_ 0
// do we reduce the score of unsatisfied literals?
// 0 = no, 1 = yes, by multiplying it with some factor
#define _WEIGHT_DIST_ 1
// the factor used for _WEIGHT_DIST_ = 1
#define _WEIGHT_DIST_FACTOR_ 0.5
// shall we repick assertion when randomizing in a plateau or use the current one?
// 0 = use old one, 1 = repick according to usual scheme, 2 = repick randomly and force different one
#define _REPICK_ 1
// do we use some UCT-like scheme for assertion-selection? overrides _BFS_
#define _UCT_ 1
// how much diversification is used in the UCT-scheme?
#define _UCT_CONSTANT_ 20.0
// how shall we initialize the _UCT_ total touched counter?
// 0 = initialize with one, 1 = initialize with number of assertions
#define _UCT_INIT_ 0
// do we gradually reduce the touched values of _UCT_?
#define _UCT_FORGET_ 0
#define _UCT_FORGET_FACTOR_ 0.9
// shall we use addition/subtraction?
#define _USE_ADDSUB_ 1
#define _USE_ADDSUB_ 0
// should we use unsat-structures as done in SLS 4 SAT instead for random or bfs selection?
#define _REAL_RS_ 0
// with what probability _PERM_STEP_/1000 will the random step happen?
#define _PERM_RSTEP_ 0
// shall we use early pruning for incremental update?
#define _EARLY_PRUNE_ 1
// shall we use caching for top_score?
#define _CACHE_TOP_SCORE_ 1
#if ((_UCT_ > 0) + _REAL_RS_ > 1)
InvalidConfiguration;
#endif
#endif

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

@ -44,6 +44,7 @@ sls_engine::sls_engine(ast_manager & m, params_ref const & p) :
m_evaluator(m, m_bv_util, m_tracker, m_mpz_manager, m_powers)
{
updt_params(p);
m_tracker.updt_params(p);
}
sls_engine::~sls_engine() {
@ -52,19 +53,21 @@ sls_engine::~sls_engine() {
m_mpz_manager.del(m_two);
}
double sls_engine::get_restart_armin(unsigned cnt_restarts)
{
unsigned outer_id = (unsigned)(0.5 + sqrt(0.25 + 2 * cnt_restarts));
unsigned inner_id = cnt_restarts - (outer_id - 1) * outer_id / 2;
return pow((double) _RESTART_CONST_ARMIN_, (int) inner_id + 1);
}
void sls_engine::updt_params(params_ref const & _p) {
sls_params p(_p);
m_produce_models = _p.get_bool("model", false);
m_max_restarts = p.restarts();
m_max_restarts = p.max_restarts();
m_tracker.set_random_seed(p.random_seed());
m_plateau_limit = p.plateau_limit();
m_walksat = p.walksat();
m_walksat_repick = p.walksat_repick();
m_paws_sp = p.paws_sp();
m_wp = p.wp();
m_vns_mc = p.vns_mc();
m_vns_repick = p.vns_repick();
m_restart_base = p.restart_base();
m_restart_next = m_restart_base;
m_restart_init = p.restart_init();
}
void sls_engine::checkpoint() {
@ -105,9 +108,7 @@ double sls_engine::top_score() {
tout << " " << m_tracker.get_score(m_assertions[i]);
tout << " AVG: " << top_sum / (double)sz << std::endl;);
#if _CACHE_TOP_SCORE_
m_tracker.set_top_sum(top_sum);
#endif
return top_sum / (double)sz;
}
@ -121,37 +122,21 @@ double sls_engine::rescore() {
double sls_engine::serious_score(func_decl * fd, const mpz & new_value) {
m_evaluator.serious_update(fd, new_value);
m_stats.m_incr_evals++;
#if _CACHE_TOP_SCORE_
return (m_tracker.get_top_sum() / m_assertions.size());
#else
return top_score();
#endif
}
double sls_engine::incremental_score(func_decl * fd, const mpz & new_value) {
m_evaluator.update(fd, new_value);
m_stats.m_incr_evals++;
#if _CACHE_TOP_SCORE_
return (m_tracker.get_top_sum() / m_assertions.size());
#else
return top_score();
#endif
}
double sls_engine::incremental_score_prune(func_decl * fd, const mpz & new_value) {
#if _EARLY_PRUNE_
m_stats.m_incr_evals++;
if (m_evaluator.update_prune(fd, new_value))
#if _CACHE_TOP_SCORE_
return (m_tracker.get_top_sum() / m_assertions.size());
#else
return top_score();
#endif
else
return 0.0;
#else
NOT_IMPLEMENTED_YET();
#endif
}
// checks whether the score outcome of a given move is better than the previous score
@ -261,7 +246,7 @@ void sls_engine::mk_random_move(ptr_vector<func_decl> & unsat_constants)
// inversion doesn't make sense, let's do a flip instead.
if (mt == MV_INV) mt = MV_FLIP;
#else
mt = MV_FLIP;
move_type mt = MV_FLIP;
#endif
unsigned bit = 0;
@ -300,7 +285,7 @@ void sls_engine::mk_random_move(ptr_vector<func_decl> & unsat_constants)
tout << "Locally randomized model: " << std::endl; m_tracker.show_model(tout););
}
m_evaluator.update(fd, new_value);
m_evaluator.serious_update(fd, new_value);
m_mpz_manager.del(new_value);
}
@ -385,7 +370,7 @@ double sls_engine::find_best_move_mc(ptr_vector<func_decl> & to_evaluate, double
if (m_bv_util.is_bv_sort(srt) && bv_sz > 2) {
for (unsigned j = 0; j < bv_sz; j++) {
mk_flip(srt, old_value, j, temp);
for (unsigned l = 0; l < _VNS_MC_TRIES_ && l < bv_sz / 2; l++)
for (unsigned l = 0; l < m_vns_mc && l < bv_sz / 2; l++)
{
unsigned k = m_tracker.get_random_uint(16) % bv_sz;
while (k == j)
@ -411,144 +396,85 @@ double sls_engine::find_best_move_mc(ptr_vector<func_decl> & to_evaluate, double
lbool sls_engine::search() {
lbool res = l_undef;
double score = 0.0, old_score = 0.0;
unsigned new_const = (unsigned)-1, new_bit = 0;
unsigned new_const = (unsigned)-1, new_bit;
mpz new_value;
move_type move;
unsigned plateau_cnt = 0;
score = rescore();
unsigned sz = m_assertions.size();
#if _RESTARTS_
while (check_restart(m_stats.m_moves) && m_stats.m_stopwatch.get_current_seconds() < _TIMELIMIT_) {
#else
while (m_stats.m_stopwatch.get_current_seconds() < _TIMELIMIT_) {
#endif
while (check_restart(m_stats.m_moves)) {
checkpoint();
m_stats.m_moves++;
#if _UCT_FORGET_
if (m_stats.m_moves % _UCT_FORGET_ == 0)
m_tracker.uct_forget(g);
#endif
if (m_stats.m_moves % m_restart_base == 0)
m_tracker.ucb_forget(m_assertions);
#if _REAL_RS_
//m_tracker.debug_real(g, m_stats.m_moves);
#endif
#if _FOCUS_
expr * e = m_tracker.get_unsat_assertion(m_assertions);
if (!e)
{
res = l_true;
goto bailout;
}
ptr_vector<func_decl> & to_evaluate = m_tracker.get_unsat_constants_walksat(e);
#else
ptr_vector<func_decl> & to_evaluate = m_tracker.get_unsat_constants_gsat(m_assertions, sz);
ptr_vector<func_decl> & to_evaluate = m_tracker.get_unsat_constants(m_assertions);
if (!to_evaluate.size())
{
res = l_true;
goto bailout;
}
#endif
if (m_tracker.get_random_uint(16) % 1000 < _PERM_RSTEP_)
if (m_wp && m_tracker.get_random_uint(10) < m_wp)
{
mk_random_move(to_evaluate);
#if _CACHE_TOP_SCORE_
score = m_tracker.get_top_sum() / sz;
#else
score = top_score(g);
#endif
continue;
}
old_score = score;
new_const = (unsigned)-1;
move = MV_FLIP;
new_bit = 0;
score = find_best_move(to_evaluate, score, new_const, new_value, new_bit, move);
#if _VNS_MC_ > _VNS_REPICK_
#if _VNS_MC_
if (new_const == static_cast<unsigned>(-1))
score = find_best_move_mc(g, to_evaluate, score, new_const, new_value);
#endif
#if _VNS_REPICK_
if (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);
/*if (m_vns_repick && (new_const == static_cast<unsigned>(-1)))
{
expr * q = m_tracker.get_new_unsat_assertion(g, e);
expr * q = m_tracker.get_new_unsat_assertion(m_assertions, e);
if (q)
{
ptr_vector<func_decl> & to_evaluate2 = m_tracker.get_unsat_constants_walksat(e);
score = find_best_move(g, to_evaluate2, score, new_const, new_value, new_bit, move);
score = find_best_move(to_evaluate2, score, new_const, new_value, new_bit, move);
}
}
#endif
#endif
#if _VNS_MC_ < _VNS_REPICK_
#if _VNS_REPICK_
if (new_const == static_cast<unsigned>(-1))
{
expr * q = m_tracker.get_new_unsat_assertion(g, e);
if (q)
{
ptr_vector<func_decl> & to_evaluate2 = m_tracker.get_unsat_constants_walksat(e);
score = find_best_move(g, to_evaluate2, score, new_const, new_value, new_bit, move);
}
}
#endif
#if _VNS_MC_
if (new_const == static_cast<unsigned>(-1))
score = find_best_move_mc(g, to_evaluate, score, new_const, new_value);
#endif
#endif
}*/
if (new_const == static_cast<unsigned>(-1)) {
score = old_score;
plateau_cnt++;
#if _REPICK_
if (m_walksat && m_walksat_repick)
m_evaluator.randomize_local(m_assertions);
#else
else
m_evaluator.randomize_local(to_evaluate);
#endif
#if _CACHE_TOP_SCORE_
score = m_tracker.get_top_sum() / m_assertions.size();
#else
score = top_score(g);
#endif
#if _PAWS_
for (unsigned i = 0; i < sz; i++)
if (m_paws_sp < 1024)
{
expr * q = m_assertions[i];
if (m_tracker.get_random_uint(16) % 100 < _PAWS_)
for (unsigned i = 0; i < sz; i++)
{
if (m_mpz_manager.eq(m_tracker.get_value(q),m_one))
m_tracker.decrease_weight(q);
}
else
{
if (m_mpz_manager.eq(m_tracker.get_value(q),m_zero))
m_tracker.increase_weight(q);
expr * q = m_assertions[i];
if (m_tracker.get_random_uint(10) < m_paws_sp)
{
if (m_mpz_manager.eq(m_tracker.get_value(q),m_one))
m_tracker.decrease_weight(q);
}
else
{
if (m_mpz_manager.eq(m_tracker.get_value(q),m_zero))
m_tracker.increase_weight(q);
}
}
}
#endif
}
else {
func_decl * fd = to_evaluate[new_const];
#if _REAL_RS_ || _PAWS_
score = serious_score(fd, new_value);
#else
score = incremental_score(fd, new_value);
#endif
}
}
@ -569,30 +495,9 @@ 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() << "_FOCUS_ " << _FOCUS_ << std::endl;
verbose_stream() << "_RESTARTS_ " << _RESTARTS_ << std::endl;
verbose_stream() << "_RESTART_LIMIT_ " << _RESTART_LIMIT_ << std::endl;
verbose_stream() << "_RESTART_INIT_ " << _RESTART_INIT_ << std::endl;
verbose_stream() << "_RESTART_SCHEME_ " << _RESTART_SCHEME_ << std::endl;
verbose_stream() << "_TIMELIMIT_ " << _TIMELIMIT_ << std::endl;
verbose_stream() << "_PAWS_ " << _PAWS_ << std::endl;
verbose_stream() << "_PAWS_INIT_ " << _PAWS_INIT_ << std::endl;
verbose_stream() << "_VNS_MC_ " << _VNS_MC_ << std::endl;
verbose_stream() << "_VNS_MC_TRIES_ " << _VNS_MC_TRIES_ << std::endl;
verbose_stream() << "_VNS_REPICK_ " << _VNS_REPICK_ << std::endl;
verbose_stream() << "_WEIGHT_DIST_ " << _WEIGHT_DIST_ << std::endl;
verbose_stream() << "_WEIGHT_DIST_FACTOR_ " << std::fixed << std::setprecision(2) << _WEIGHT_DIST_FACTOR_ << std::endl;
verbose_stream() << "_REPICK_ " << _REPICK_ << std::endl;
verbose_stream() << "_UCT_ " << _UCT_ << std::endl;
verbose_stream() << "_UCT_CONSTANT_ " << std::fixed << std::setprecision(2) << _UCT_CONSTANT_ << std::endl;
verbose_stream() << "_UCT_INIT_ " << _UCT_INIT_ << std::endl;
verbose_stream() << "_UCT_FORGET_ " << _UCT_FORGET_ << std::endl;
verbose_stream() << "_UCT_FORGET_FACTOR_ " << std::fixed << std::setprecision(2) << _UCT_FORGET_FACTOR_ << std::endl;
verbose_stream() << "_USE_ADDSUB_ " << _USE_ADDSUB_ << std::endl;
verbose_stream() << "_REAL_RS_ " << _REAL_RS_ << std::endl;
verbose_stream() << "_PERM_RSTEP_ " << _PERM_RSTEP_ << std::endl;
verbose_stream() << "_EARLY_PRUNE_ " << _EARLY_PRUNE_ << std::endl;
verbose_stream() << "_CACHE_TOP_SCORE_ " << _CACHE_TOP_SCORE_ << std::endl;
lbool res = operator()();
@ -620,8 +525,6 @@ lbool sls_engine::operator()() {
m_tracker.initialize(m_assertions);
lbool res = l_undef;
m_restart_limit = _RESTART_LIMIT_;
do {
checkpoint();
@ -630,39 +533,53 @@ lbool sls_engine::operator()() {
if (res == l_undef)
{
#if _RESTART_INIT_
m_tracker.randomize();
#else
m_tracker.reset(m_assertions);
#endif
if (m_restart_init)
m_tracker.randomize(m_assertions);
else
m_tracker.reset(m_assertions);
}
} while (m_stats.m_stopwatch.get_current_seconds() < _TIMELIMIT_ && res != l_true && m_stats.m_restarts++ < m_max_restarts);
} while (res != l_true && m_stats.m_restarts++ < m_max_restarts);
verbose_stream() << "(restarts: " << m_stats.m_restarts << " flips: " << m_stats.m_moves << " time: " << std::fixed << std::setprecision(2) << m_stats.m_stopwatch.get_current_seconds() << " fps: " << (m_stats.m_moves / m_stats.m_stopwatch.get_current_seconds()) << ")" << std::endl;
return res;
}
unsigned sls_engine::check_restart(unsigned curr_value)
/* Andreas: Needed for Armin's restart scheme if we don't want to use loops.
inline double sls_engine::get_restart_armin(unsigned cnt_restarts)
{
if (curr_value > m_restart_limit)
unsigned outer_id = (unsigned)(0.5 + sqrt(0.25 + 2 * cnt_restarts));
unsigned inner_id = cnt_restarts - (outer_id - 1) * outer_id / 2;
return pow((double) _RESTART_CONST_ARMIN_, (int) inner_id + 1);
}
*/
inline unsigned sls_engine::check_restart(unsigned curr_value)
{
if (curr_value > m_restart_next)
{
/* Andreas: My own scheme (= 1) seems to work best. Other schemes are disabled so that we save 1 parameter.
I leave the other versions as comments in case you want to try it again somewhen.
#if _RESTART_SCHEME_ == 5
m_restart_limit += (unsigned)(_RESTART_LIMIT_ * pow(_RESTART_CONST_ARMIN_, m_stats.m_restarts));
m_restart_next += (unsigned)(m_restart_base * pow(_RESTART_CONST_ARMIN_, m_stats.m_restarts));
#elif _RESTART_SCHEME_ == 4
m_restart_limit += (m_stats.m_restarts & (m_stats.m_restarts + 1)) ? _RESTART_LIMIT_ : (_RESTART_LIMIT_ * m_stats.m_restarts + 1);
m_restart_next += (m_stats.m_restarts & (m_stats.m_restarts + 1)) ? m_restart_base : (m_restart_base * m_stats.m_restarts + 1);
#elif _RESTART_SCHEME_ == 3
m_restart_limit += (unsigned)get_restart_armin(m_stats.m_restarts + 1) * _RESTART_LIMIT_;
m_restart_next += (unsigned)get_restart_armin(m_stats.m_restarts + 1) * m_restart_base;
#elif _RESTART_SCHEME_ == 2
m_restart_limit += get_luby(m_stats.m_restarts + 1) * _RESTART_LIMIT_;
m_restart_next += get_luby(m_stats.m_restarts + 1) * m_restart_base;
#elif _RESTART_SCHEME_ == 1
if (m_stats.m_restarts & 1)
m_restart_limit += _RESTART_LIMIT_;
m_restart_next += m_restart_base;
else
m_restart_limit += (2 << (m_stats.m_restarts >> 1)) * _RESTART_LIMIT_;
m_restart_next += (2 << (m_stats.m_restarts >> 1)) * m_restart_base;
#else
m_restart_limit += _RESTART_LIMIT_;
#endif
m_restart_limit += m_restart_base;
#endif */
if (m_stats.m_restarts & 1)
m_restart_next += m_restart_base;
else
m_restart_next += (2 << (m_stats.m_restarts >> 1)) * m_restart_base;
return 0;
}
return 1;

13
src/tactic/sls/sls_engine.h
View file

@ -70,9 +70,16 @@ protected:
sls_evaluator m_evaluator;
ptr_vector<expr> m_assertions;
unsigned m_restart_limit;
unsigned m_max_restarts;
unsigned m_plateau_limit;
unsigned m_walksat;
unsigned m_walksat_repick;
unsigned m_wp;
unsigned m_vns_mc;
unsigned m_vns_repick;
unsigned m_paws_sp;
unsigned m_restart_base;
unsigned m_restart_next;
unsigned m_restart_init;
ptr_vector<mpz> m_old_values;
@ -110,7 +117,6 @@ public:
protected:
void checkpoint();
double get_restart_armin(unsigned cnt_restarts);
bool what_if(func_decl * fd, const unsigned & fd_inx, const mpz & temp,
double & best_score, unsigned & best_const, mpz & best_value);
@ -129,6 +135,7 @@ protected:
void mk_random_move(ptr_vector<func_decl> & unsat_constants);
//inline double get_restart_armin(unsigned cnt_restarts);
inline unsigned check_restart(unsigned curr_value);
};

175
src/tactic/sls/sls_evaluator.h
View file

@ -81,11 +81,7 @@ public:
case OP_AND: {
m_mpz_manager.set(result, m_one);
for (unsigned i = 0; i < n_args; i++)
#if _DIRTY_UP_
if (m_mpz_manager.neq(m_tracker.get_value(args[i]), result) && !m_tracker.is_top_expr(args[i])) {
#else
if (m_mpz_manager.neq(m_tracker.get_value(args[i]), result)) {
#endif
m_mpz_manager.set(result, m_zero);
break;
}
@ -93,11 +89,7 @@ public:
}
case OP_OR: {
for (unsigned i = 0; i < n_args; i++)
#if _DIRTY_UP_
if (m_mpz_manager.neq(m_tracker.get_value(args[i]), result) || m_tracker.is_top_expr(args[i])) {
#else
if (m_mpz_manager.neq(m_tracker.get_value(args[i]), result)) {
#endif
m_mpz_manager.set(result, m_one);
break;
}
@ -105,16 +97,9 @@ public:
}
case OP_NOT: {
SASSERT(n_args == 1);
#if _DIRTY_UP_
if (m_tracker.is_top_expr(args[0]))
m_mpz_manager.set(result, m_zero);
else
m_mpz_manager.set(result, (m_mpz_manager.is_zero(m_tracker.get_value(args[0]))) ? m_one : m_zero);
#else
const mpz & child = m_tracker.get_value(args[0]);
SASSERT(m_mpz_manager.is_one(child) || m_mpz_manager.is_zero(child));
m_mpz_manager.set(result, (m_mpz_manager.is_zero(child)) ? m_one : m_zero);
#endif
break;
}
case OP_EQ: {
@ -545,9 +530,7 @@ public:
expr_fast_mark1 visited;
mpz new_value;
#if _EARLY_PRUNE_ || _CACHE_TOP_SCORE_
double new_score;
#endif
SASSERT(cur_depth < m_traversal_stack.size());
while (cur_depth != static_cast<unsigned>(-1)) {
@ -569,23 +552,12 @@ public:
}
#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);
#if _EARLY_PRUNE_
new_score = m_tracker.score(cur);
#if _CACHE_TOP_SCORE_
if (m_tracker.is_top_expr(cur))
m_tracker.adapt_top_sum(cur, new_score, m_tracker.get_score(cur));
#endif
m_tracker.set_score(cur, new_score);
m_tracker.set_score_prune(cur, new_score);
#else
#if _CACHE_TOP_SCORE_
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);
#else
m_tracker.set_score(cur, m_tracker.score(cur));
#endif
#endif
if (m_tracker.has_uplinks(cur)) {
@ -614,9 +586,7 @@ public:
expr_fast_mark1 visited;
mpz new_value;
#if _EARLY_PRUNE_ || _CACHE_TOP_SCORE_
double new_score;
#endif
SASSERT(cur_depth < m_traversal_stack.size());
while (cur_depth != static_cast<unsigned>(-1)) {
@ -627,23 +597,12 @@ public:
(*this)(to_app(cur), new_value);
m_tracker.set_value(cur, new_value);
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);
#if _EARLY_PRUNE_
new_score = m_tracker.score(cur);
#if _CACHE_TOP_SCORE_
if (m_tracker.is_top_expr(cur))
m_tracker.adapt_top_sum(cur, new_score, m_tracker.get_score(cur));
#endif
m_tracker.set_score(cur, new_score);
m_tracker.set_score_prune(cur, new_score);
#else
#if _CACHE_TOP_SCORE_
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);
#else
m_tracker.set_score(cur, m_tracker.score(cur));
#endif
#endif
if (m_tracker.has_uplinks(cur)) {
ptr_vector<expr> & ups = m_tracker.get_uplinks(cur);
@ -679,11 +638,7 @@ public:
m_traversal_stack[cur_depth].push_back(ep);
if (cur_depth > max_depth) max_depth = cur_depth;
}
#if _REAL_RS_ || _PAWS_
run_serious_update(max_depth);
#else
run_update(max_depth);
#endif
}
void update(func_decl * fd, const mpz & new_value) {
@ -708,7 +663,6 @@ public:
run_serious_update(cur_depth);
}
#if _EARLY_PRUNE_
unsigned run_update_bool_prune(unsigned cur_depth) {
expr_fast_mark1 visited;
@ -722,10 +676,9 @@ public:
expr * cur = cur_depth_exprs[i];
new_score = m_tracker.score(cur);
#if _CACHE_TOP_SCORE_
if (m_tracker.is_top_expr(cur))
m_tracker.adapt_top_sum(cur, new_score, m_tracker.get_score(cur));
#endif
prune_score = m_tracker.get_score_prune(cur);
m_tracker.set_score(cur, new_score);
@ -746,9 +699,6 @@ public:
}
}
}
else
{
}
}
cur_depth_exprs.reset();
@ -762,14 +712,11 @@ public:
for (unsigned i = 0; i < cur_size; i++) {
expr * cur = cur_depth_exprs[i];
#if _CACHE_TOP_SCORE_
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);
#else
m_tracker.set_score(cur, m_tracker.score(cur));
#endif
if (m_tracker.has_uplinks(cur)) {
ptr_vector<expr> & ups = m_tracker.get_uplinks(cur);
for (unsigned j = 0; j < ups.size(); j++) {
@ -850,103 +797,6 @@ public:
}
return run_update_bool_prune(cur_depth);
}
#endif
unsigned run_update_bool_prune_new(unsigned cur_depth) {
expr_fast_mark1 visited;
double prune_score, new_score;
unsigned pot_benefits = 0;
SASSERT(cur_depth < m_traversal_stack_bool.size());
ptr_vector<expr> & cur_depth_exprs = m_traversal_stack_bool[cur_depth];
for (unsigned i = 0; i < cur_depth_exprs.size(); i++) {
expr * cur = cur_depth_exprs[i];
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));
prune_score = m_tracker.get_score_prune(cur);
m_tracker.set_score(cur, new_score);
if ((new_score >= prune_score) && (m_tracker.has_pos_occ(cur)))
pot_benefits = 1;
if ((new_score < prune_score) && (m_tracker.has_neg_occ(cur)))
pot_benefits = 1;
if (m_tracker.has_uplinks(cur)) {
ptr_vector<expr> & ups = m_tracker.get_uplinks(cur);
for (unsigned j = 0; j < ups.size(); j++) {
expr * next = ups[j];
unsigned next_d = m_tracker.get_distance(next);
SASSERT(next_d < cur_depth);
if (!visited.is_marked(next)) {
m_traversal_stack_bool[next_d].push_back(next);
visited.mark(next);
}
}
}
else
{
}
}
cur_depth_exprs.reset();
cur_depth--;
while (cur_depth != static_cast<unsigned>(-1)) {
ptr_vector<expr> & cur_depth_exprs = m_traversal_stack_bool[cur_depth];
if (pot_benefits)
{
unsigned cur_size = cur_depth_exprs.size();
for (unsigned i = 0; i < cur_size; i++) {
expr * cur = cur_depth_exprs[i];
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);
if (m_tracker.has_uplinks(cur)) {
ptr_vector<expr> & ups = m_tracker.get_uplinks(cur);
for (unsigned j = 0; j < ups.size(); j++) {
expr * next = ups[j];
unsigned next_d = m_tracker.get_distance(next);
SASSERT(next_d < cur_depth);
if (!visited.is_marked(next)) {
m_traversal_stack_bool[next_d].push_back(next);
visited.mark(next);
}
}
}
}
}
cur_depth_exprs.reset();
cur_depth--;
}
return pot_benefits;
}
unsigned update_prune_new(func_decl * fd, const mpz & new_value) {
m_tracker.set_value(fd, new_value);
expr * ep = m_tracker.get_entry_point(fd);
unsigned cur_depth = m_tracker.get_distance(ep);
if (m_traversal_stack_bool.size() <= cur_depth)
m_traversal_stack_bool.resize(cur_depth+1);
if (m_traversal_stack.size() <= cur_depth)
m_traversal_stack.resize(cur_depth+1);
if (m_manager.is_bool(ep))
m_traversal_stack_bool[cur_depth].push_back(ep);
else
{
m_traversal_stack[cur_depth].push_back(ep);
run_update_prune(cur_depth);
}
return run_update_bool_prune_new(cur_depth);
}
void randomize_local(ptr_vector<func_decl> & unsat_constants) {
// Randomize _one_ candidate:
@ -954,11 +804,8 @@ public:
func_decl * fd = unsat_constants[r];
mpz temp = m_tracker.get_random(fd->get_range());
#if _REAL_RS_ || _PAWS_
serious_update(fd, temp);
#else
update(fd, temp);
#endif
m_mpz_manager.del(temp);
TRACE("sls", tout << "Randomization candidate: " << unsat_constants[r]->get_name() << std::endl;

6
src/tactic/sls/sls_tactic.cpp
View file

@ -159,16 +159,12 @@ tactic * mk_preamble(ast_manager & m, params_ref const & p) {
using_params(mk_simplify_tactic(m), simp2_p)),
using_params(mk_simplify_tactic(m), hoist_p),
mk_max_bv_sharing_tactic(m),
// Andreas: It would be cool to get rid of shared top level assertions but which simplification is doing this?
//mk_ctx_simplify_tactic(m, ctx_p),
// Andreas: This one at least eliminates top level duplicates ... but has very bad effects on performance!
//mk_simplify_tactic(m),
mk_nnf_tactic(m, p));
}
tactic * mk_qfbv_sls_tactic(ast_manager & m, params_ref const & p) {
tactic * t = and_then(mk_preamble(m, p), mk_sls_tactic(m));
// tactic * t = and_then(mk_simplify_tactic(m), mk_nnf_tactic(m, p), mk_sls_tactic(m));
//tactic * t = and_then(mk_simplify_tactic(m), mk_nnf_tactic(m, p), mk_sls_tactic(m));
t->updt_params(p);
return t;
}

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

@ -39,11 +39,7 @@ class sls_tracker {
mpz m_zero, m_one, m_two;
struct value_score {
#if _EARLY_PRUNE_
value_score() : m(0), value(unsynch_mpz_manager::mk_z(0)), score(0.0), distance(0), touched(1), score_prune(0.0), has_pos_occ(0), has_neg_occ(0) { };
#else
value_score() : m(0), value(unsynch_mpz_manager::mk_z(0)), score(0.0), distance(0), touched(1) { };
#endif
~value_score() { if (m) m->del(value); }
unsynch_mpz_manager * m;
mpz value;
@ -80,20 +76,22 @@ private:
ptr_vector<func_decl> m_constants;
ptr_vector<func_decl> m_temp_constants;
occ_type m_constants_occ;
#if _UCT_
unsigned m_walksat;
unsigned m_ucb;
double m_ucb_constant;
unsigned m_ucb_init;
double m_ucb_forget;
unsigned m_touched;
#endif
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
#if _PAWS_
obj_map<expr, unsigned> m_weights;
#endif
#if _CACHE_TOP_SCORE_
double m_top_sum;
#endif
unsigned m_equal_scores;
public:
@ -114,6 +112,17 @@ public:
m_mpz_manager.del(m_two);
}
void updt_params(params_ref const & _p) {
sls_params p(_p);
m_walksat = p.walksat();
m_ucb = p.walksat_ucb();
m_ucb_constant = p.walksat_ucb_constant();
m_ucb_init = p.walksat_ucb_init();
m_ucb_forget = p.walksat_ucb_forget();
m_scale_unsat = p.scale_unsat();
m_paws_init = p.paws_init();
}
unsigned get_formula_size() {
return m_scores.size();
}
@ -147,13 +156,8 @@ public:
return ++m_equal_scores;
}
#if _CACHE_TOP_SCORE_
inline void adapt_top_sum(expr * e, double add, double sub) {
#if _PAWS_
m_top_sum += m_weights.find(e) * (add - sub);
#else
m_top_sum += add - sub;
#endif
}
inline void set_top_sum(double new_score) {
@ -163,7 +167,6 @@ public:
inline double get_top_sum() {
return m_top_sum;
}
#endif
inline void set_value(expr * n, const mpz & r) {
SASSERT(m_scores.contains(n));
@ -209,7 +212,6 @@ public:
return get_score(ep);
}
#if _EARLY_PRUNE_
inline void set_score_prune(expr * n, double score) {
SASSERT(m_scores.contains(n));
m_scores.find(n).score_prune = score;
@ -229,7 +231,6 @@ public:
SASSERT(m_scores.contains(n));
return m_scores.find(n).has_neg_occ;
}
#endif
inline unsigned get_distance(expr * n) {
SASSERT(m_scores.contains(n));
@ -310,17 +311,20 @@ public:
}
#endif
void uct_forget(ptr_vector<expr> & as) {
expr * e;
unsigned touched_old, touched_new;
for (unsigned i = 0; i < as.size(); i++)
inline void ucb_forget(ptr_vector<expr> & as) {
if (m_ucb_forget < 1.0)
{
e = as[i];
touched_old = m_scores.find(e).touched;
touched_new = (unsigned)((touched_old - 1) * _UCT_FORGET_FACTOR_ + 1);
m_scores.find(e).touched = touched_new;
m_touched += touched_new - touched_old;
expr * e;
unsigned touched_old, touched_new;
for (unsigned i = 0; i < as.size(); i++)
{
e = as[i];
touched_old = m_scores.find(e).touched;
touched_new = (unsigned)((touched_old - 1) * m_ucb_forget + 1);
m_scores.find(e).touched = touched_new;
m_touched += touched_new - touched_old;
}
}
}
@ -490,26 +494,21 @@ public:
//}
#endif
#if _PAWS_
for (unsigned i = 0; i < sz; i++)
{
expr * e = as[i];
if (!m_weights.contains(e))
m_weights.insert(e, _PAWS_INIT_);
m_weights.insert(e, m_paws_init);
}
#endif
#if _EARLY_PRUNE_
for (unsigned i = 0; i < sz; i++)
setup_occs(as[i]);
#endif
#if _UCT_
m_touched = _UCT_INIT_ ? as.size() : 1;
#endif
m_touched = m_ucb_init ? as.size() : 1;
}
#if _PAWS_
void increase_weight(expr * e)
{
m_weights.find(e)++;
@ -518,14 +517,13 @@ public:
void decrease_weight(expr * e)
{
unsigned old_weight = m_weights.find(e);
m_weights.find(e) = old_weight > _PAWS_INIT_ ? old_weight - 1 : _PAWS_INIT_;
m_weights.find(e) = old_weight > m_paws_init ? old_weight - 1 : m_paws_init;
}
unsigned get_weight(expr * e)
{
return m_weights.find(e);
}
#endif
#if _REAL_RS_
void make_assertion(expr * e)
@ -684,7 +682,6 @@ public:
}
}
#if _EARLY_PRUNE_
void setup_occs(expr * n, bool negated = false) {
if (m_manager.is_bool(n))
{
@ -717,7 +714,6 @@ public:
else
NOT_IMPLEMENTED_YET();
}
#endif
double score_bool(expr * n, bool negated = false) {
TRACE("sls_score", tout << ((negated)?"NEG ":"") << "BOOL: " << mk_ismt2_pp(n, m_manager) << std::endl; );
@ -735,20 +731,17 @@ public:
SASSERT(!negated);
app * a = to_app(n);
expr * const * args = a->get_args();
// Andreas: Seems to have no effect. Probably it does not even occur.
#if _SCORE_AND_AVG_
/* Andreas: Seems to have no effect. But maybe you want to try it again at some point.
double sum = 0.0;
for (unsigned i = 0; i < a->get_num_args(); i++)
sum += get_score(args[i]);
res = sum / (double) a->get_num_args();
#else
res = sum / (double) a->get_num_args(); */
double min = 1.0;
for (unsigned i = 0; i < a->get_num_args(); i++) {
double cur = get_score(args[i]);
if (cur < min) min = cur;
}
res = min;
#endif
}
else if (m_manager.is_or(n)) {
SASSERT(!negated);
@ -927,13 +920,11 @@ public:
SASSERT(res >= 0.0 && res <= 1.0);
#if _WEIGHT_DIST_
app * a = to_app(n);
family_id afid = a->get_family_id();
if (afid == m_bv_util.get_family_id())
if (res < 1.0) res *= _WEIGHT_DIST_FACTOR_;
#endif
if (res < 1.0) res *= m_scale_unsat;
TRACE("sls_score", tout << "SCORE = " << res << std::endl; );
return res;
@ -995,8 +986,8 @@ public:
return m_temp_constants;
}
ptr_vector<func_decl> & get_unsat_constants_gsat(ptr_vector<expr> const & as, unsigned sz) {
ptr_vector<func_decl> & get_unsat_constants_gsat(ptr_vector<expr> const & as) {
unsigned sz = as.size();
if (sz == 1) {
if (m_mpz_manager.neq(get_value(as[0]), m_one))
return get_constants();
@ -1033,89 +1024,88 @@ public:
}
ptr_vector<func_decl> & get_unsat_constants(ptr_vector<expr> const & as) {
#if _FOCUS_
expr * e = get_unsat_assertion(as);
if (!e)
if (m_walksat)
{
m_temp_constants.reset();
return m_temp_constants;
}
expr * e = get_unsat_assertion(as);
return get_unsat_constants_walksat(e);
#else
return m_tracker.get_unsat_constants_gsat(as, sz);
#endif
if (!e)
{
m_temp_constants.reset();
return m_temp_constants;
}
return get_unsat_constants_walksat(e);
}
else
return get_unsat_constants_gsat(as);
}
expr * get_unsat_assertion(ptr_vector<expr> const & as) {
unsigned sz = as.size();
if (sz == 1) {
if (m_mpz_manager.neq(get_value(as[0]), m_one))
return as[0];
else
return 0;
}
m_temp_constants.reset();
#if _UCT_
unsigned pos = -1;
value_score vscore;
double max = -1.0;
if (m_ucb)
{
value_score vscore;
double max = -1.0;
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);
#if _UCT_ == 1
double q = vscore.score + _UCT_CONSTANT_ * sqrt(log((double)m_touched) / vscore.touched);
#elif _UCT_ == 3
double q = vscore.score + m_ucb_constant * sqrt(log((double)m_touched) / vscore.touched);
#if _UCT_ == 3
double q = vscore.score + _UCT_CONSTANT_ * sqrt(log(m_touched)/vscore.touched) + (get_random_uint(16) * 0.1 / (2<<16));
#endif
if (q > max && m_mpz_manager.neq(get_value(e), m_one) ) { max = q; pos = i; }
if (q > max && m_mpz_manager.neq(get_value(e), m_one) ) { max = q; pos = i; }
}
if (pos == static_cast<unsigned>(-1))
return 0;
if (pos == static_cast<unsigned>(-1))
return 0;
#if _UCT_
m_scores.find(as[pos]).touched++;
m_touched++;
#endif
m_scores.find(as[pos]).touched++;
m_touched++;
// return m_list_false[pos];
}
else
{
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;
if (pos == static_cast<unsigned>(-1))
return 0;
}
return as[pos];
#elif _REAL_RS_
#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];
#else
unsigned cnt_unsat = 0, pos = -1;
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;
if (pos == static_cast<unsigned>(-1))
return 0;
#endif
return as[pos];
}
expr * get_new_unsat_assertion(goal_ref const & g, expr * e) {
unsigned sz = g->size();
expr * get_new_unsat_assertion(ptr_vector<expr> const & as, expr * e) {
unsigned sz = as.size();
if (sz == 1)
return 0;
m_temp_constants.reset();
unsigned cnt_unsat = 0, pos = -1;
for (unsigned i = 0; i < sz; i++)
if (m_mpz_manager.neq(get_value(g->form(i)), m_one) && (get_random_uint(16) % ++cnt_unsat == 0) && (g->form(i) != e)) pos = 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 (pos == static_cast<unsigned>(-1))
return 0;
return g->form(pos);
return as[pos];
}
};