diff --git a/src/tactic/sls/sls_compilation_settings.h b/src/tactic/sls/sls_compilation_settings.h index 73ba1ffab..9add78daa 100644 --- a/src/tactic/sls/sls_compilation_settings.h +++ b/src/tactic/sls/sls_compilation_settings.h @@ -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 \ No newline at end of file diff --git a/src/tactic/sls/sls_engine.cpp b/src/tactic/sls/sls_engine.cpp index 938b6e0df..c240a0c51 100644 --- a/src/tactic/sls/sls_engine.cpp +++ b/src/tactic/sls/sls_engine.cpp @@ -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 & 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 & 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 & 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 & 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 & to_evaluate = m_tracker.get_unsat_constants_walksat(e); -#else - ptr_vector & to_evaluate = m_tracker.get_unsat_constants_gsat(m_assertions, sz); + + ptr_vector & 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(-1)) - score = find_best_move_mc(g, to_evaluate, score, new_const, new_value); -#endif -#if _VNS_REPICK_ - if (new_const == static_cast(-1)) + if (m_vns_mc && (new_const == static_cast(-1))) + score = find_best_move_mc(to_evaluate, score, new_const, new_value); + + /*if (m_vns_repick && (new_const == static_cast(-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 & 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(-1)) - { - expr * q = m_tracker.get_new_unsat_assertion(g, e); - if (q) - { - ptr_vector & 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(-1)) - score = find_best_move_mc(g, to_evaluate, score, new_const, new_value); -#endif -#endif + }*/ if (new_const == static_cast(-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; diff --git a/src/tactic/sls/sls_engine.h b/src/tactic/sls/sls_engine.h index 4e5af8c93..ff0e55f24 100644 --- a/src/tactic/sls/sls_engine.h +++ b/src/tactic/sls/sls_engine.h @@ -70,9 +70,16 @@ protected: sls_evaluator m_evaluator; ptr_vector 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 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 & unsat_constants); + //inline double get_restart_armin(unsigned cnt_restarts); inline unsigned check_restart(unsigned curr_value); }; diff --git a/src/tactic/sls/sls_evaluator.h b/src/tactic/sls/sls_evaluator.h index da2a4b29f..37bfa5a2d 100644 --- a/src/tactic/sls/sls_evaluator.h +++ b/src/tactic/sls/sls_evaluator.h @@ -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(-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(-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 & 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 & 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 & 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 & 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(-1)) { - ptr_vector & 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 & 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 & 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; diff --git a/src/tactic/sls/sls_tactic.cpp b/src/tactic/sls/sls_tactic.cpp index 7a9252fe2..2a40e908d 100644 --- a/src/tactic/sls/sls_tactic.cpp +++ b/src/tactic/sls/sls_tactic.cpp @@ -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; } diff --git a/src/tactic/sls/sls_tracker.h b/src/tactic/sls/sls_tracker.h index 235ab9471..65011dc8d 100644 --- a/src/tactic/sls/sls_tracker.h +++ b/src/tactic/sls/sls_tracker.h @@ -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 m_constants; ptr_vector 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 m_unsat_expr; obj_map m_where_false; expr** m_list_false; #endif -#if _PAWS_ obj_map 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 & as) { - expr * e; - unsigned touched_old, touched_new; - - for (unsigned i = 0; i < as.size(); i++) + inline void ucb_forget(ptr_vector & 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 & get_unsat_constants_gsat(ptr_vector const & as, unsigned sz) { - + ptr_vector & get_unsat_constants_gsat(ptr_vector 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 & get_unsat_constants(ptr_vector 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 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(-1)) - return 0; + if (pos == static_cast(-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(-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(-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 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(-1)) return 0; - return g->form(pos); + return as[pos]; } };