From de028e7a30df593547b47262e98d9673f00adfa9 Mon Sep 17 00:00:00 2001 From: Andreas Froehlich Date: Tue, 22 Apr 2014 00:32:45 +0100 Subject: [PATCH] Almost cleaned up version. --- src/tactic/sls/sls_compilation_settings.h | 156 +-- src/tactic/sls/sls_engine.cpp | 1168 +++------------------ src/tactic/sls/sls_engine.h | 89 +- src/tactic/sls/sls_evaluator.h | 262 +---- src/tactic/sls/sls_tactic.cpp | 6 +- src/tactic/sls/sls_tracker.h | 904 ++-------------- 6 files changed, 315 insertions(+), 2270 deletions(-) diff --git a/src/tactic/sls/sls_compilation_settings.h b/src/tactic/sls/sls_compilation_settings.h index d2b899dd8..9add78daa 100644 --- a/src/tactic/sls/sls_compilation_settings.h +++ b/src/tactic/sls/sls_compilation_settings.h @@ -22,167 +22,13 @@ Notes: #ifndef _SLS_COMPILATION_SETTINGS_H_ #define _SLS_COMPILATION_SETTINGS_H_ -// which unsatisfied assertion is selected? only works with _FOCUS_ > 0 -// 0 = random, 1 = #moves, 2 = assertion with min score, 3 = assertion with max score -#define _BFS_ 0 - -// how many terms are considered for variable selection? -// 0 = all terms (GSAT), 1 = only one top level assertion (WSAT), 2 = only one bottom level atom -#define _FOCUS_ 1 - -// probability of choosing the same assertion again in the next step -#define _PERC_STICKY_ 0 - -// do we use dirty unit propagation to get rid of nested top level assertions? -#define _DIRTY_UP_ 0 - -// 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 - -// should score of discunctions be calculated by multiplication of the inverse score rather than min? -#define _SCORE_OR_MUL_ 0 - -// do we use some kind of variable neighbourhood-search? -// 0 = no, 1 = only consider flipping bits if no better score can be obtained otherwise, 2 = only consider flipping bits until a better score can be obtained -#define _VNS_ 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 - -// what is the probability of doing so (percentage)? -#define _VNS_PERC_ 100 - -// do a decreasing move with percentage ... -#define _INSIST_PERC_ 0 - -// do we reduce the score of unsatisfied literals? -// 0 = no -// 1 = yes, by multiplying it with some factor -// 2 = yes, by squaring it -// 3 = yes, by setting it to zero -// 4 = by progessively increasing weight (_TIMELIMIT_ needs to be set appropriately!) -#define _WEIGHT_DIST_ 1 - -// the factor used for _WEIGHT_DIST_ = 1 -#define _WEIGHT_DIST_FACTOR_ 0.5 - -// shall we toggle the weight after each restart? -#define _WEIGHT_TOGGLE_ 0 - -// do we use intensification steps in local minima? if so, how many? -#define _INTENSIFICATION_ 0 -#define _INTENSIFICATION_TRIES_ 0 - -// what is the percentage of random moves in plateaus (instead of full randomization)? -#define _PERC_PLATEAU_MOVES_ 0 - -// 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 - -// is uct clause selection probabilistic similar to variable selection in sparrow? -// 0 = no, 1 = yes, use uct-value, 2 = yes, use score-value (_UCT_CONSTANT_ = 0.0) with squared score -#define _PROBABILISTIC_UCT_ 0 - -// additive constants for probabilistic uct > 0 -#define _UCT_EPS_ 0.0001 - -// shall we reset _UCT_ touched values after restart? -#define _UCT_RESET_ 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 - -// shall we try multilication and division by 2? -#define _USE_MUL2DIV2_ 0 - -// shall we try multiplication by 3? -#define _USE_MUL3_ 0 - -// shall we try unary minus (= inverting and incrementing) -#define _USE_UNARY_MINUS_ 0 - -// is random selection for assertions uniform? only works with _BFS_ = _UCT_ = 0 -#define _UNIFORM_RANDOM_ 0 +#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 -#define _REAL_PBFS_ 0 - -// how many bits do we neglect in each iteration? -#define _SKIP_BITS_ 0 - -// when randomizing local, what is the probability for changing a single bit? -// 0 = use standard scheme and pick a new value at random (= 50), otherwise the value (as int) gives the percentage -#define _PERC_CHANGE_ 0 - -// do we use random steps for noise? -// 0 = no, 1 = randomize local, 2 = make random move -#define _TYPE_RSTEP_ 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 ((_BFS_ > 0) + (_UCT_ > 0) + _UNIFORM_RANDOM_ + _REAL_RS_ + _REAL_PBFS_ > 1) -InvalidConfiguration; -#endif -#if (_PROBABILISTIC_UCT_ && !_UCT_) -InvalidConfiguration; -#endif -#if (_PERM_RSTEP_ && !_TYPE_RSTEP_) -InvalidConfiguration; -#endif -#if (_PERC_CHANGE_ == 50) -InvalidConfiguration; -#endif -#if (_PERC_STICKY_ && !_FOCUS_) -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 342e649af..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,20 +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; - //printf("armin: %f\n", pow(1.1, inner_id + 1)); - 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() { @@ -74,15 +76,15 @@ void sls_engine::checkpoint() { cooperate("sls"); } -bool sls_engine::full_eval(goal_ref const & g, model & mdl) { +bool sls_engine::full_eval(model & mdl) { bool res = true; - unsigned sz = g->size(); + unsigned sz = m_assertions.size(); for (unsigned i = 0; i < sz && res; i++) { checkpoint(); expr_ref o(m_manager); - if (!mdl.eval(g->form(i), o, true)) + if (!mdl.eval(m_assertions[i], o, true)) exit(ERR_INTERNAL_FATAL); res = m_manager.is_true(o.get()); @@ -93,93 +95,58 @@ bool sls_engine::full_eval(goal_ref const & g, model & mdl) { return res; } -double sls_engine::top_score(goal_ref const & g) { -#if 0 - double min = m_tracker.get_score(g->form(0)); - unsigned sz = g->size(); - for (unsigned i = 1; i < sz; i++) { - double q = m_tracker.get_score(g->form(i)); - if (q < min) min = q; - } - TRACE("sls_top", tout << "Score distribution:"; - for (unsigned i = 0; i < sz; i++) - tout << " " << m_tracker.get_score(g->form(i)); - tout << " MIN: " << min << std::endl;); - return min; -#else +double sls_engine::top_score() { double top_sum = 0.0; - unsigned sz = g->size(); + unsigned sz = m_assertions.size(); for (unsigned i = 0; i < sz; i++) { - expr * e = g->form(i); + expr * e = m_assertions[i]; top_sum += m_tracker.get_score(e); } TRACE("sls_top", tout << "Score distribution:"; for (unsigned i = 0; i < sz; i++) - tout << " " << m_tracker.get_score(g->form(i)); + 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; -#endif } -double sls_engine::rescore(goal_ref const & g) { +double sls_engine::rescore() { m_evaluator.update_all(); m_stats.m_full_evals++; - return top_score(g); + return top_score(); } -double sls_engine::serious_score(goal_ref const & g, func_decl * fd, const mpz & new_value) { +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() / g->size()); -#else - return top_score(g); -#endif + return (m_tracker.get_top_sum() / m_assertions.size()); } -double sls_engine::incremental_score(goal_ref const & g, func_decl * fd, const mpz & new_value) { +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() / g->size()); -#else - return top_score(g); -#endif + return (m_tracker.get_top_sum() / m_assertions.size()); } -double sls_engine::incremental_score_prune(goal_ref const & g, func_decl * fd, const mpz & new_value) { -#if _EARLY_PRUNE_ +double sls_engine::incremental_score_prune(func_decl * fd, const mpz & new_value) { m_stats.m_incr_evals++; if (m_evaluator.update_prune(fd, new_value)) -#if _CACHE_TOP_SCORE_ - return (m_tracker.get_top_sum() / g->size()); -#else - return top_score(g); -#endif - else - return 0.0; -#else - NOT_IMPLEMENTED_YET(); -#endif -} - -double sls_engine::incremental_score_prune_new(goal_ref const & g, func_decl * fd, const mpz & new_value) { - m_stats.m_incr_evals++; - if (m_evaluator.update_prune_new(fd, new_value)) - return (m_tracker.get_top_sum() / g->size()); + return (m_tracker.get_top_sum() / m_assertions.size()); else return 0.0; } // checks whether the score outcome of a given move is better than the previous score -bool sls_engine::what_if(goal_ref const & g, func_decl * fd, const unsigned & fd_inx, const mpz & temp, - double & best_score, unsigned & best_const, mpz & best_value) { +bool sls_engine::what_if( + func_decl * fd, + const unsigned & fd_inx, + const mpz & temp, + double & best_score, + unsigned & best_const, + mpz & best_value) { #ifdef Z3DEBUG mpz old_value; @@ -187,9 +154,9 @@ bool sls_engine::what_if(goal_ref const & g, func_decl * fd, const unsigned & fd #endif #if _EARLY_PRUNE_ - double r = incremental_score_prune(g, fd, temp); + double r = incremental_score_prune(fd, temp); #else - double r = incremental_score(g, fd, temp); + double r = incremental_score(fd, temp); #endif #ifdef Z3DEBUG TRACE("sls_whatif", tout << "WHAT IF " << fd->get_name() << " WERE " << m_mpz_manager.to_string(temp) << @@ -198,7 +165,7 @@ bool sls_engine::what_if(goal_ref const & g, func_decl * fd, const unsigned & fd m_mpz_manager.del(old_value); #endif - //if (r >= best_score) { + // Andreas: For some reason it is important to use > here instead of >=. Probably related to prefering the LSB. if (r > best_score) { m_tracker.reset_equal_scores(); best_score = r; @@ -206,45 +173,6 @@ bool sls_engine::what_if(goal_ref const & g, func_decl * fd, const unsigned & fd m_mpz_manager.set(best_value, temp); return true; } - /*else if (r == best_score) { - if (m_tracker.get_random_uint(16) % m_tracker.inc_equal_scores() == 0) - { - best_score = r; - best_const = fd_inx; - m_mpz_manager.set(best_value, temp); - return true; - } - }*/ - - return false; -} - -bool sls_engine::what_if_new(goal_ref const & g, func_decl * fd, const unsigned & fd_inx, const mpz & temp, - double & best_score, unsigned & best_const, mpz & best_value) { - - double r = incremental_score_prune_new(g, fd, temp); - - if (r >= best_score) { - best_score = r; - best_const = fd_inx; - m_mpz_manager.set(best_value, temp); - return true; - } - - return false; -} - -// same as what_if, but only applied to the score of a specific atom, not the total score -bool sls_engine::what_if_local(expr * e, func_decl * fd, const unsigned & fd_inx, const mpz & temp, - double & best_score, unsigned & best_const, mpz & best_value) { - m_evaluator.update(fd, temp); - double r = m_tracker.get_score(e); - if (r >= best_score) { - best_score = r; - best_const = fd_inx; - m_mpz_manager.set(best_value, temp); - return true; - } return false; } @@ -261,22 +189,6 @@ void sls_engine::mk_add(unsigned bv_sz, const mpz & old_value, mpz & add_value, } -// Andreas: do we really need all those temporary mpzs? -void sls_engine::mk_mul2(unsigned bv_sz, const mpz & old_value, mpz & result) { - mpz temp, mask, mask2; - m_mpz_manager.mul(old_value, m_two, temp); - m_mpz_manager.set(mask, m_powers(bv_sz)); - m_mpz_manager.bitwise_not(bv_sz, mask, mask2); - m_mpz_manager.bitwise_and(temp, mask2, result); - m_mpz_manager.del(temp); - m_mpz_manager.del(mask); - m_mpz_manager.del(mask2); -} - -void sls_engine::mk_div2(unsigned bv_sz, const mpz & old_value, mpz & result) { - m_mpz_manager.div(old_value, m_two, result); -} - void sls_engine::mk_inc(unsigned bv_sz, const mpz & old_value, mpz & incremented) { unsigned shift; m_mpz_manager.add(old_value, m_one, incremented); @@ -334,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; @@ -373,216 +285,40 @@ 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); } -void sls_engine::mk_random_move(goal_ref const & g) { - mk_random_move(m_tracker.get_unsat_constants(g, m_stats.m_moves)); -} - -// will use VNS to ignore some possible moves and increase the flips per second -double sls_engine::find_best_move_vns(goal_ref const & g, ptr_vector & to_evaluate, double score, - unsigned & best_const, mpz & best_value, unsigned & new_bit, move_type & move) { - mpz old_value, temp; - unsigned bv_sz, max_bv_sz = 0; - double new_score = score; - - for (unsigned i = 0; i < to_evaluate.size() && new_score < 1.0; 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); - if (max_bv_sz < bv_sz) max_bv_sz = bv_sz; - m_mpz_manager.set(old_value, m_tracker.get_value(fd)); - - if (m_bv_util.is_bv_sort(srt) && bv_sz > 1) { - if (!m_mpz_manager.is_even(old_value)) { - // for odd values, try +1 - mk_inc(bv_sz, old_value, temp); - if (what_if(g, fd, i, temp, new_score, best_const, best_value)) - move = MV_INC; - } - else { - // for even values, try -1 - mk_dec(bv_sz, old_value, temp); - if (what_if(g, fd, i, temp, new_score, best_const, best_value)) - move = MV_DEC; - } - - // try inverting - mk_inv(bv_sz, old_value, temp); - if (what_if(g, fd, i, temp, new_score, best_const, best_value)) - move = MV_INV; - - // try to flip lsb - mk_flip(srt, old_value, 0, temp); - if (what_if(g, fd, i, temp, new_score, best_const, best_value)) { - new_bit = 0; - move = MV_FLIP; - } - } - - // reset to what it was before - double check = incremental_score(g, fd, old_value); - SASSERT(check == score); - } - - // we can either check the condition once in the beginning or check it repeatedly after every bit -#if _VNS_ == 1 - for (unsigned j = 1; j < max_bv_sz && new_score <= score; j++) -#else - if (new_score <= score) - for (unsigned j = 1; j < max_bv_sz && new_score < 1.0; j++) -#endif - for (unsigned i = 0; i < to_evaluate.size() && new_score < 1.0; 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); - m_mpz_manager.set(old_value, m_tracker.get_value(fd)); - - // What would happen if we flipped bit #j ? - if (j < bv_sz) - { - mk_flip(srt, old_value, j, temp); - - if (what_if(g, fd, i, temp, new_score, best_const, best_value)) { - new_bit = j; - move = MV_FLIP; - } - } - // reset to what it was before - double check = incremental_score(g, fd, old_value); - SASSERT(check == score); - } - m_mpz_manager.del(old_value); - m_mpz_manager.del(temp); - return new_score; -} - -double sls_engine::find_best_move_lsb(goal_ref const & g, ptr_vector & to_evaluate, double score, - unsigned & best_const, mpz & best_value, unsigned & new_bit, move_type & move) { - mpz old_value, temp; - unsigned bv_sz, max_bv_sz = 0; - double new_score = score; - - 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); - if (max_bv_sz < bv_sz) max_bv_sz = bv_sz; - m_mpz_manager.set(old_value, m_tracker.get_value(fd)); - - if (m_bv_util.is_bv_sort(srt) && bv_sz > 1) { - // try inverting - mk_inv(bv_sz, old_value, temp); - if (what_if(g, fd, i, temp, new_score, best_const, best_value)) - move = MV_INV; - - if (!m_mpz_manager.is_even(old_value)) { - // for odd values, try +1 - mk_inc(bv_sz, old_value, temp); - if (what_if(g, fd, i, temp, new_score, best_const, best_value)) - move = MV_INC; - } - else { - // for even values, try -1 - mk_dec(bv_sz, old_value, temp); - if (what_if(g, fd, i, temp, new_score, best_const, best_value)) - move = MV_DEC; - } - - // try to flip lsb - mk_flip(srt, old_value, 0, temp); - if (what_if(g, fd, i, temp, new_score, best_const, best_value)) { - new_bit = 0; - move = MV_FLIP; - } - } - - // reset to what it was before - double check = incremental_score(g, fd, old_value); - SASSERT(check == score); - } - - for (unsigned j = 1; j < max_bv_sz; j++) - { - 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); - m_mpz_manager.set(old_value, m_tracker.get_value(fd)); - - // What would happen if we flipped bit #j ? - if (j < bv_sz) - { - mk_flip(srt, old_value, j, temp); - - if (what_if(g, fd, i, temp, new_score, best_const, best_value)) { - new_bit = j; - move = MV_FLIP; - } - } - // reset to what it was before - double check = incremental_score(g, fd, old_value); - SASSERT(check == score); - } - } - m_mpz_manager.del(old_value); - m_mpz_manager.del(temp); - return new_score; -} - // finds the move that increased score the most. returns best_const = -1, if no increasing move exists. -double sls_engine::find_best_move(goal_ref const & g, ptr_vector & to_evaluate, double score, - unsigned & best_const, mpz & best_value, unsigned & new_bit, move_type & move) { +double sls_engine::find_best_move( + ptr_vector & to_evaluate, + double score, + unsigned & best_const, + mpz & best_value, + unsigned & new_bit, + move_type & move) +{ mpz old_value, temp; -#if _USE_MUL3_ || _USE_UNARY_MINUS_ - mpz temp2; -#endif unsigned bv_sz; -#if _INSIST_PERC_ - double new_score = m_tracker.get_random_uint(16) % 100 < _INSIST_PERC_ ? 0.0 : score; -#else double new_score = score; -#endif m_tracker.reset_equal_scores(); -// for (unsigned i = 0; i < to_evaluate.size() && new_score < 1.0; i++) { for (unsigned i = 0; i < to_evaluate.size(); i++) { -// for (unsigned i = m_tracker.get_random_uint(16) % to_evaluate.size(); i != to_evaluate.size(); i = to_evaluate.size()) { -// for (unsigned i = to_evaluate.size(); i-- > 0; ) { 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); m_mpz_manager.set(old_value, m_tracker.get_value(fd)); // first try to flip every bit -#if _SKIP_BITS_ - for (unsigned j = (i + m_stats.m_moves) % (_SKIP_BITS_ + 1); j < bv_sz && new_score < 1.0; j += (_SKIP_BITS_ + 1)) { -#else -// for (unsigned j = 0; j < bv_sz && new_score < 1.0; j++) { for (unsigned j = 0; j < bv_sz; j++) { -// for (unsigned j = bv_sz; j-- > 0; ) { -#endif // What would happen if we flipped bit #i ? mk_flip(srt, old_value, j, temp); - //if (m_tracker.get_random_uint(1)) - //if ((move != MV_FLIP) || (new_bit > j)) - //{ - //if (what_if_new(g, fd, i, temp, new_score, best_const, best_value)) { - // new_bit = j; - // move = MV_FLIP; - //} - //} - //else - //{ - if (what_if(g, fd, i, temp, new_score, best_const, best_value)) { + if (what_if(fd, i, temp, new_score, best_const, best_value)) { new_bit = j; move = MV_FLIP; } - //} } if (m_bv_util.is_bv_sort(srt) && bv_sz > 1) { @@ -590,76 +326,41 @@ double sls_engine::find_best_move(goal_ref const & g, ptr_vector & to if (!m_mpz_manager.is_even(old_value)) { // for odd values, try +1 mk_inc(bv_sz, old_value, temp); - //if (m_tracker.get_random_uint(1)) - if (what_if(g, fd, i, temp, new_score, best_const, best_value)) + if (what_if(fd, i, temp, new_score, best_const, best_value)) move = MV_INC; } else { // for even values, try -1 mk_dec(bv_sz, old_value, temp); - //if (m_tracker.get_random_uint(1)) - if (what_if(g, fd, i, temp, new_score, best_const, best_value)) + if (what_if(fd, i, temp, new_score, best_const, best_value)) move = MV_DEC; } #endif // try inverting mk_inv(bv_sz, old_value, temp); - //if (m_tracker.get_random_uint(1)) - if (what_if(g, fd, i, temp, new_score, best_const, best_value)) + if (what_if(fd, i, temp, new_score, best_const, best_value)) move = MV_INV; - -#if _USE_UNARY_MINUS_ - mk_inc(bv_sz, temp, temp2); - if (what_if(g, fd, i, temp2, new_score, best_const, best_value)) - move = MV_UMIN; -#endif - -#if _USE_MUL2DIV2_ - // try multiplication by 2 - mk_mul2(bv_sz, old_value, temp); - if (what_if(g, fd, i, temp, new_score, best_const, best_value)) - move = MV_MUL2; - -#if _USE_MUL3_ - // try multiplication by 3 - mk_add(bv_sz, old_value, temp, temp2); - if (what_if(g, fd, i, temp2, new_score, best_const, best_value)) - move = MV_MUL3; -#endif - - // try division by 2 - mk_div2(bv_sz, old_value, temp); - if (what_if(g, fd, i, temp, new_score, best_const, best_value)) - move = MV_DIV2; -#endif } // reset to what it was before - double check = incremental_score(g, fd, old_value); + double check = incremental_score(fd, old_value); // Andreas: does not hold anymore now that we use top level score caching //SASSERT(check == score); } m_mpz_manager.del(old_value); m_mpz_manager.del(temp); -#if _USE_MUL3_ - m_mpz_manager.del(temp2); -#endif - - if ((new_score == score) && 1)// (m_tracker.get_random_uint(1))) - best_const = -1; return new_score; } // finds the move that increased score the most. returns best_const = -1, if no increasing move exists. -double sls_engine::find_best_move_mc(goal_ref const & g, ptr_vector & to_evaluate, double score, +double sls_engine::find_best_move_mc(ptr_vector & to_evaluate, double score, unsigned & best_const, mpz & best_value) { mpz old_value, temp, temp2; unsigned bv_sz; double new_score = score; -// for (unsigned i = 0; i < to_evaluate.size() && new_score < 1.0; i++) { for (unsigned i = 0; i < to_evaluate.size(); i++) { func_decl * fd = to_evaluate[i]; sort * srt = fd->get_range(); @@ -667,22 +368,21 @@ double sls_engine::find_best_move_mc(goal_ref const & g, ptr_vector & m_mpz_manager.set(old_value, m_tracker.get_value(fd)); if (m_bv_util.is_bv_sort(srt) && bv_sz > 2) { -// for (unsigned j = 0; j < bv_sz && new_score < 1.0; j++) { 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) k = m_tracker.get_random_uint(16) % bv_sz; mk_flip(srt, temp, k, temp2); - what_if(g, fd, i, temp2, new_score, best_const, best_value); + what_if(fd, i, temp2, new_score, best_const, best_value); } } } // reset to what it was before - double check = incremental_score(g, fd, old_value); + double check = incremental_score(fd, old_value); } m_mpz_manager.del(old_value); @@ -692,618 +392,89 @@ double sls_engine::find_best_move_mc(goal_ref const & g, ptr_vector & return new_score; } -// same as find_best_move but only considers the score of the current expression instead of the overall score -double sls_engine::find_best_move_local(expr * e, ptr_vector & to_evaluate, - unsigned & best_const, mpz & best_value, unsigned & new_bit, move_type & move) { - mpz old_value, temp; - unsigned bv_sz; - double new_score = m_tracker.get_score(e); - // Andreas: tie breaking not implemented yet - // double tie_score = top_score(g); - 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); - m_mpz_manager.set(old_value, m_tracker.get_value(fd)); - - // first try to flip every bit - for (unsigned j = 0; j < bv_sz; j++) { - // What would happen if we flipped bit #i ? - mk_flip(srt, old_value, j, temp); - - if (what_if_local(e, fd, i, temp, new_score, best_const, best_value)) { - new_bit = j; - move = MV_FLIP; - } - } - - if (m_bv_util.is_bv_sort(srt) && bv_sz > 1) { - if (!m_mpz_manager.is_even(old_value)) { - // for odd values, try +1 - mk_inc(bv_sz, old_value, temp); - if (what_if_local(e, fd, i, temp, new_score, best_const, best_value)) - move = MV_INC; - } - else { - // for even values, try -1 - mk_dec(bv_sz, old_value, temp); - if (what_if_local(e, fd, i, temp, new_score, best_const, best_value)) - move = MV_DEC; - } - - // try inverting - mk_inv(bv_sz, old_value, temp); - if (what_if_local(e, fd, i, temp, new_score, best_const, best_value)) - move = MV_INV; - } - - // reset to what it was before - m_evaluator.update(fd, old_value); - } - - m_mpz_manager.del(old_value); - m_mpz_manager.del(temp); - return new_score; -} - -// first try of intensification ... does not seem to be efficient -bool sls_engine::handle_plateau(goal_ref const & g) -{ - unsigned sz = g->size(); -#if _BFS_ - unsigned pos = m_stats.m_moves % sz; -#else - unsigned pos = m_tracker.get_random_uint(16) % sz; -#endif - expr * e = m_tracker.get_unsat_assertion(g, sz, pos); - if (!e) - return 0; - - expr * q = m_tracker.get_unsat_expression(e); - ptr_vector & to_evaluate = m_tracker.get_constants(q); - for (unsigned i = 0; i < to_evaluate.size(); i++) - { - m_tracker.get_value(to_evaluate[i]); - m_old_values.push_back(&m_tracker.get_value(to_evaluate[i])); - } - unsigned new_const = (unsigned)-1, new_bit = 0; - mpz new_value; - move_type move; - for (unsigned i = 0; i < _INTENSIFICATION_TRIES_; i++) - { - // Andreas: Could be extended to use (best) score but this is computationally more expensive. - find_best_move_local(q, to_evaluate, new_const, new_value, new_bit, move); - - if (new_const == static_cast(-1)) { - // Andreas: Actually this should never happen. - NOT_IMPLEMENTED_YET(); - } - else { - m_stats.m_moves++; - func_decl * fd = to_evaluate[new_const]; - - switch (move) { - case MV_FLIP: m_stats.m_flips++; break; - case MV_INC: m_stats.m_incs++; break; - case MV_DEC: m_stats.m_decs++; break; - case MV_INV: m_stats.m_invs++; break; - case MV_UMIN: m_stats.m_umins++; break; - case MV_MUL2: m_stats.m_mul2s++; break; - case MV_MUL3: m_stats.m_mul3s++; break; - case MV_DIV2: m_stats.m_div2s++; break; - } - - m_evaluator.update(fd, new_value); - } - - if (m_mpz_manager.is_one(m_tracker.get_value(q))) - return 1; - } - - for (unsigned i = 0; i < to_evaluate.size(); i++) - m_tracker.set_value(to_evaluate[i], *m_old_values[i]); - - m_old_values.reset(); - - return 0; -} - -// what_if version needed in the context of 2nd intensification try, combining local and global score -bool sls_engine::what_if(goal_ref const & g, expr * e, func_decl * fd, const mpz & temp, - double & best_score, mpz & best_value, unsigned i) { - - double global_score = incremental_score(g, fd, temp); - double local_score = m_tracker.get_score(e); - double new_score = i * local_score / _INTENSIFICATION_TRIES_ + (_INTENSIFICATION_TRIES_ - i) * global_score / _INTENSIFICATION_TRIES_; - - if (new_score >= best_score) { - best_score = new_score; - m_mpz_manager.set(best_value, temp); - return true; - } - - return false; -} - -// find_best_move version needed in the context of 2nd intensification try -double sls_engine::find_best_move_local(goal_ref const & g, expr * e, func_decl * fd, mpz & best_value, unsigned i) -{ - mpz old_value, temp; - double best_score = 0; - - sort * srt = fd->get_range(); - unsigned bv_sz = (m_manager.is_bool(srt)) ? 1 : m_bv_util.get_bv_size(srt); - m_mpz_manager.set(old_value, m_tracker.get_value(fd)); - - for (unsigned j = 0; j < bv_sz && best_score < 1.0; j++) { - mk_flip(srt, old_value, j, temp); - what_if(g, e, fd, temp, best_score, best_value, i); - } - - m_mpz_manager.del(old_value); - m_mpz_manager.del(temp); - - return best_score; -} - -// second try to use intensification ... also not very effective -bool sls_engine::handle_plateau(goal_ref const & g, double old_score) -{ - unsigned sz = g->size(); -#if _BFS_ - unsigned new_const = m_stats.m_moves % sz; -#else - unsigned new_const = m_tracker.get_random_uint(16) % sz; -#endif - expr * e = m_tracker.get_unsat_assertion(g, sz, new_const); - if (!e) - return 0; - - expr * q = m_tracker.get_unsat_expression(e); - ptr_vector & to_evaluate = m_tracker.get_constants(q); - - new_const = m_tracker.get_random_uint(16) % to_evaluate.size(); - func_decl * fd = to_evaluate[new_const]; - - mpz new_value; - //m_mpz_manager.set(new_value, m_tracker.get_value(fd)); - unsigned new_bit = 0; - double global_score = old_score, local_score = m_tracker.get_score(q), new_score = old_score; - - for (unsigned i = 1; i <= _INTENSIFICATION_TRIES_; i++) - { - new_score = find_best_move_local(g, q, fd, new_value, i); - - m_stats.m_moves++; - m_stats.m_flips++; - - global_score = incremental_score(g, fd, new_value); - local_score = m_tracker.get_score(q); - - SASSERT(new_score == i * local_score / _INTENSIFICATION_TRIES_ + (_INTENSIFICATION_TRIES_ - i) * global_score / _INTENSIFICATION_TRIES_); - - if (m_mpz_manager.is_one(m_tracker.get_value(q))) - return 1; - } - - return 0; -} - // main search loop -lbool sls_engine::search(goal_ref const & g) { +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(g); - unsigned sz = g->size(); - - TRACE("sls", tout << "Starting search, initial score = " << std::setprecision(32) << score << std::endl; - tout << "Score distribution:"; - for (unsigned i = 0; i < g->size(); i++) - tout << " " << std::setprecision(3) << m_tracker.get_score(g->form(i)); - tout << " TOP: " << score << std::endl;); - -#if _PERC_STICKY_ - expr * e = m_tracker.get_unsat_assertion(g, m_stats.m_moves); -#endif - -#if _RESTARTS_ == 1 - while (check_restart(m_stats.m_moves) && m_stats.m_stopwatch.get_current_seconds() < _TIMELIMIT_) { -#elif _RESTARTS_ == 2 - while (check_restart(plateau_cnt) && m_stats.m_stopwatch.get_current_seconds() < _TIMELIMIT_) { -#elif _RESTARTS_ == 3 - while (check_restart((unsigned)m_stats.m_stopwatch.get_current_seconds()) && m_stats.m_stopwatch.get_current_seconds() < _TIMELIMIT_) { -#else - while (m_stats.m_stopwatch.get_current_seconds() < _TIMELIMIT_) { -#endif - //if (m_stats.m_stopwatch.get_current_seconds() > 10.0) - //{printf("Got %f fps and size is %d with avg bw %f\n", m_stats.m_moves / m_stats.m_stopwatch.get_current_seconds(), m_tracker.get_formula_size(), m_tracker.get_avg_bw(g)); exit(0);} + score = rescore(); + unsigned sz = m_assertions.size(); + while (check_restart(m_stats.m_moves)) { checkpoint(); m_stats.m_moves++; + if (m_stats.m_moves % m_restart_base == 0) + m_tracker.ucb_forget(m_assertions); -#if _UCT_FORGET_ - //if (m_stats.m_moves % sz == 0) - if (m_stats.m_moves % _UCT_FORGET_ == 0) - m_tracker.uct_forget(g); -#endif - -#if _REAL_RS_ || _REAL_PBFS_ +#if _REAL_RS_ //m_tracker.debug_real(g, m_stats.m_moves); #endif - -#if _FOCUS_ -#if _PERC_STICKY_ - if (m_tracker.get_random_uint(16) % 100 >= _PERC_STICKY_ || m_mpz_manager.eq(m_tracker.get_value(e), m_one)) - e = m_tracker.get_unsat_assertion(g, m_stats.m_moves); -#else - expr * e = m_tracker.get_unsat_assertion(g, m_stats.m_moves); -#endif - if (!e) - { - res = l_true; - goto bailout; - } - //ptr_vector & to_evaluate = m_tracker.get_unsat_constants_only(e); - ptr_vector & to_evaluate = m_tracker.get_unsat_constants_walksat(e); -#else - ptr_vector & to_evaluate = m_tracker.get_unsat_constants_gsat(g, sz); + + ptr_vector & to_evaluate = m_tracker.get_unsat_constants(m_assertions); if (!to_evaluate.size()) { res = l_true; goto bailout; } -#endif -#if _TYPE_RSTEP_ - if (m_tracker.get_random_uint(16) % 1000 < _PERM_RSTEP_) + if (m_wp && m_tracker.get_random_uint(10) < m_wp) { -#if _TYPE_RSTEP_ == 1 - m_evaluator.randomize_local(to_evaluate); -#elif _TYPE_RSTEP_ == 2 mk_random_move(to_evaluate); -#endif -#if _CACHE_TOP_SCORE_ - score = m_tracker.get_top_sum() / g->size(); -#else - score = top_score(g); -#endif + score = m_tracker.get_top_sum() / sz; + continue; } - continue; -#endif -#if _WEIGHT_DIST_ == 4 - m_tracker.set_weight_dist_factor(m_stats.m_stopwatch.get_current_seconds() / _TIMELIMIT_); -#endif old_score = score; new_const = (unsigned)-1; - move = MV_FLIP; - new_bit = 0; -#if _VNS_ - score = find_best_move_vns(g, to_evaluate, score, new_const, new_value, new_bit, move); -#else - score = find_best_move(g, to_evaluate, score, new_const, new_value, new_bit, move); -#endif + 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)) - if (m_tracker.get_random_uint(16) % 100 < _VNS_PERC_) - 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_tracker.get_random_uint(16) % 100 < _VNS_PERC_) { - 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); - } + 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(m_assertions, e); + if (q) + { + ptr_vector & to_evaluate2 = m_tracker.get_unsat_constants_walksat(e); + 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)) - if (m_tracker.get_random_uint(16) % 100 < _VNS_PERC_) { - 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)) - if (m_tracker.get_random_uint(16) % 100 < _VNS_PERC_) - score = find_best_move_mc(g, to_evaluate, score, new_const, new_value); -#endif -#endif - -#if (_VNS_MC_ == _VNS_REPICK_) && _VNS_MC_ && _VNS_REPICK_ - if (new_const == static_cast(-1)) { - if (m_tracker.get_random_uint(16) % 100 < _VNS_PERC_) - score = find_best_move_mc(g, to_evaluate, score, new_const, new_value); - else { - 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 (new_const == static_cast(-1)) { score = old_score; - plateau_cnt++; -#if _INTENSIFICATION_ - handle_plateau(g, score); - //handle_plateau(g); - //e = m_tracker.get_unsat_assertion(g, m_stats.m_moves); - //to_evaluate = m_tracker.get_unsat_constants_walksat(e); -#else -#if _PERC_PLATEAU_MOVES_ - if (m_tracker.get_random_uint(8) % 100 < _PERC_PLATEAU_MOVES_) - mk_random_move(to_evaluate); + if (m_walksat && m_walksat_repick) + m_evaluator.randomize_local(m_assertions); else -#endif -#if _REPICK_ == 1 - m_evaluator.randomize_local(g, m_stats.m_moves); -#elif _REPICK_ == 2 - { - expr * q = m_tracker.get_new_unsat_assertion(g, e); - if (q) - m_evaluator.randomize_local(q); - else - m_evaluator.randomize_local(e); - } -#else - m_evaluator.randomize_local_n(g, to_evaluate); - //m_evaluator.randomize_local(to_evaluate); -#endif -#endif + m_evaluator.randomize_local(to_evaluate); -#if _CACHE_TOP_SCORE_ - score = m_tracker.get_top_sum() / g->size(); -#else - score = top_score(g); -#endif + score = m_tracker.get_top_sum() / m_assertions.size(); -#if _PAWS_ - for (unsigned i = 0; i < sz; i++) + if (m_paws_sp < 1024) { - expr * q = g->form(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_ || _REAL_PBFS_ || _PAWS_ - score = serious_score(g, fd, new_value); -#else - score = incremental_score(g, fd, new_value); -#endif - } - } - -bailout: - m_mpz_manager.del(new_value); - - return res; -} - -// main search loop -lbool sls_engine::search_old(goal_ref const & g) { - lbool res = l_undef; - double score = 0.0, old_score = 0.0; - unsigned new_const = (unsigned)-1, new_bit = 0; - mpz new_value; - move_type move; - - score = rescore(g); - TRACE("sls", tout << "Starting search, initial score = " << std::setprecision(32) << score << std::endl; - tout << "Score distribution:"; - for (unsigned i = 0; i < g->size(); i++) - tout << " " << std::setprecision(3) << m_tracker.get_score(g->form(i)); - tout << " TOP: " << score << std::endl;); - - unsigned plateau_cnt = 0; - - // Andreas: Why do we only allow so few plateaus? -#if _RESTARTS_ - while (m_stats.m_stopwatch.get_current_seconds() < 200 * (m_stats.m_restarts + 1) * 0.2) { - //while (plateau_cnt < m_plateau_limit && m_stats.m_stopwatch.get_current_seconds() < _TIMELIMIT_) { -#else - while (m_stats.m_stopwatch.get_current_seconds() < _TIMELIMIT_ && (_RESTARTS_ == 0 || m_stats.m_moves < _RESTARTS_)) { -#endif - do { - checkpoint(); - -#if _WEIGHT_DIST_ == 4 - m_tracker.set_weight_dist_factor(m_stats.m_stopwatch.get_current_seconds() / _TIMELIMIT_); -#endif - -#if _TYPE_RSTEP_ - if (m_tracker.get_random_uint(16) % 1000 < _PERM_RSTEP_) - { -#if _TYPE_RSTEP_ == 1 - m_evaluator.randomize_local(g, m_stats.m_moves); -#elif _TYPE_RSTEP_ == 2 - mk_random_move(g); -#endif - score = top_score(g); - - if (score >= 1.0) { - bool all_true = true; - for (unsigned i = 0; i < g->size() && all_true; i++) - if (!m_mpz_manager.is_one(m_tracker.get_value(g->form(i)))) - all_true = false; - if (all_true) { - res = l_true; // sat - goto bailout; - } - else - TRACE("sls", tout << "Imprecise 1.0 score" << std::endl;); - } - } -#endif - old_score = score; - new_const = (unsigned)-1; - - ptr_vector & to_evaluate = m_tracker.get_unsat_constants(g, m_stats.m_moves); - if (!to_evaluate.size()) - { - res = l_true; - goto bailout; - } - TRACE("sls_constants", tout << "Evaluating these constants: " << std::endl; - for (unsigned i = 0; i < to_evaluate.size(); i++) - tout << to_evaluate[i]->get_name() << std::endl;); - -#if _VNS_ - score = find_best_move_vns(g, to_evaluate, score, new_const, new_value, new_bit, move); -#else - score = find_best_move(g, to_evaluate, score, new_const, new_value, new_bit, move); -#endif - if (new_const == static_cast(-1)) { - TRACE("sls", tout << "Local maximum reached; unsatisfied constraints: " << std::endl; - for (unsigned i = 0; i < g->size(); i++) { - if (!m_mpz_manager.is_one(m_tracker.get_value(g->form(i)))) - tout << mk_ismt2_pp(g->form(i), m_manager) << std::endl; - }); - - TRACE("sls_max", m_tracker.show_model(tout); - tout << "Scores: " << std::endl; - for (unsigned i = 0; i < g->size(); i++) - tout << mk_ismt2_pp(g->form(i), m_manager) << " ---> " << - m_tracker.get_score(g->form(i)) << std::endl;); - // Andreas: If new_const == -1, shouldn't score = old_score anyway? - score = old_score; - } - else { - // Andreas: Why does randomizing not count as a move? (Now it does.) - m_stats.m_moves++; - func_decl * fd = to_evaluate[new_const]; - - TRACE("sls", tout << "Setting " << fd->get_name() << " to " << m_mpz_manager.to_string(new_value) << " (Move: "; - switch (move) { - case MV_FLIP: - tout << "Flip"; - if (!m_manager.is_bool(fd->get_range())) tout << " #" << new_bit; - break; - case MV_INC: - tout << "+1"; - break; - case MV_DEC: - tout << "-1"; - break; - case MV_INV: - tout << "NEG"; - break; - }; - tout << ") ; new score = " << std::setprecision(32) << score << std::endl;); - - switch (move) { - case MV_FLIP: m_stats.m_flips++; break; - case MV_INC: m_stats.m_incs++; break; - case MV_DEC: m_stats.m_decs++; break; - case MV_INV: m_stats.m_invs++; break; - case MV_UMIN: m_stats.m_umins++; break; - case MV_MUL2: m_stats.m_mul2s++; break; - case MV_MUL3: m_stats.m_mul3s++; break; - case MV_DIV2: m_stats.m_div2s++; break; - } - -#if _REAL_RS_ || _REAL_PBFS_ || _PAWS_ - score = serious_score(g, fd, new_value); -#else - score = incremental_score(g, fd, new_value); -#endif - - TRACE("sls", tout << "Score distribution:"; - for (unsigned i = 0; i < g->size(); i++) - tout << " " << std::setprecision(3) << m_tracker.get_score(g->form(i)); - tout << " TOP: " << score << std::endl;); - } - - if (score >= 0.99999) { - // if (score >= 1.0) { - // score could theoretically be imprecise. - // Andreas: it seems using top level score caching can make the score unprecise also in the other direction! - bool all_true = true; - for (unsigned i = 0; i < g->size() && all_true; i++) - if (!m_mpz_manager.is_one(m_tracker.get_value(g->form(i)))) - all_true = false; - if (all_true) { - res = l_true; // sat - goto bailout; - } - else - TRACE("sls", tout << "Imprecise 1.0 score" << std::endl;); - } - /* - if (m_stats.m_moves % 100 == 0) - { - verbose_stream() << "(" << std::fixed << std::setprecision(10) << score << ")" << std::endl; - verbose_stream() << "(" << std::fixed << std::setprecision(2) << (m_stats.m_moves / m_stats.m_stopwatch.get_current_seconds()) << ")" << std::endl; - }*/ - } while (score > old_score && res == l_undef); - - // Andreas: Why do you check for old_score? This should always be equal due to the loop invariant. - if (score != old_score) { - report_tactic_progress("This should not happen I guess.", plateau_cnt); - plateau_cnt = 0; - } - else { - m_stats.m_moves++; - plateau_cnt++; - //report_tactic_progress("Plateau.", plateau_cnt); - // Andreas: Right now, a useless assignment is created in case of a restart. But we don't want to use restarts anyway. - //if (plateau_cnt < m_plateau_limit) { - TRACE("sls", tout << "In a plateau (" << plateau_cnt << "/" << m_plateau_limit << "); randomizing locally." << std::endl;); -#if _INTENSIFICATION_ - handle_plateau(g, score); - //handle_plateau(g); -#else - m_evaluator.randomize_local(g, m_stats.m_moves); -#endif - //mk_random_move(g); - score = top_score(g); - - if (score >= 1.0) { - bool all_true = true; - for (unsigned i = 0; i < g->size() && all_true; i++) - if (!m_mpz_manager.is_one(m_tracker.get_value(g->form(i)))) - all_true = false; - if (all_true) { - res = l_true; // sat - goto bailout; - } - else - TRACE("sls", tout << "Imprecise 1.0 score" << std::endl;); - } + score = serious_score(fd, new_value); } } @@ -1321,80 +492,14 @@ void sls_engine::operator()(goal_ref const & g, model_converter_ref & mc) { m_produce_models = g->models_enabled(); - verbose_stream() << "_BFS_ " << _BFS_ << std::endl; - verbose_stream() << "_FOCUS_ " << _FOCUS_ << std::endl; - verbose_stream() << "_PERC_STICKY_ " << _PERC_STICKY_ << 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() << "_SCORE_AND_AVG_ " << _SCORE_AND_AVG_ << std::endl; - verbose_stream() << "_SCORE_OR_MUL_ " << _SCORE_OR_MUL_ << std::endl; - verbose_stream() << "_PAWS_ " << _PAWS_ << std::endl; - verbose_stream() << "_PAWS_INIT_ " << _PAWS_INIT_ << std::endl; - verbose_stream() << "_VNS_ " << _VNS_ << 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() << "_VNS_PERC_ " << _VNS_PERC_ << std::endl; - verbose_stream() << "_INSIST_PERC_ " << _INSIST_PERC_ << 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() << "_INTENSIFICATION_ " << _INTENSIFICATION_ << std::endl; - verbose_stream() << "_INTENSIFICATION_TRIES_ " << _INTENSIFICATION_TRIES_ << std::endl; - verbose_stream() << "_PERC_PLATEAU_MOVES_ " << _PERC_PLATEAU_MOVES_ << 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_RESET_ " << _UCT_RESET_ << 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() << "_PROBABILISTIC_UCT_ " << _PROBABILISTIC_UCT_ << std::endl; - verbose_stream() << "_UCT_EPS_ " << std::fixed << std::setprecision(4) << _UCT_EPS_ << std::endl; + for (unsigned i = 0; i < g->size(); i++) + assert_expr(g->form(i)); + verbose_stream() << "_USE_ADDSUB_ " << _USE_ADDSUB_ << std::endl; - verbose_stream() << "_USE_MUL2DIV2_ " << _USE_MUL2DIV2_ << std::endl; - verbose_stream() << "_USE_MUL3_ " << _USE_MUL3_ << std::endl; - verbose_stream() << "_USE_UNARY_MINUS_ " << _USE_UNARY_MINUS_ << std::endl; - verbose_stream() << "_UNIFORM_RANDOM_ " << _UNIFORM_RANDOM_ << std::endl; verbose_stream() << "_REAL_RS_ " << _REAL_RS_ << std::endl; - verbose_stream() << "_REAL_PBFS_ " << _REAL_PBFS_ << std::endl; - verbose_stream() << "_SKIP_BITS_ " << _SKIP_BITS_ << std::endl; - verbose_stream() << "_PERC_CHANGE_ " << _PERC_CHANGE_ << std::endl; - verbose_stream() << "_TYPE_RSTEP_ " << _TYPE_RSTEP_ << 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; -#if _WEIGHT_DIST_ == 4 - m_tracker.set_weight_dist_factor(m_stats.m_stopwatch.get_current_seconds() / _TIMELIMIT_); -#endif -#if _WEIGHT_TOGGLE_ - m_tracker.set_weight_dist_factor(_WEIGHT_DIST_FACTOR_); -#endif - m_tracker.initialize(g); - lbool res = l_undef; - - m_restart_limit = _RESTART_LIMIT_; - - do { - checkpoint(); - - report_tactic_progress("Searching... restarts left:", m_max_restarts - m_stats.m_restarts); - res = search(g); - - if (res == l_undef) - { -#if _RESTART_INIT_ - m_tracker.randomize(g); -#else - m_tracker.reset(g); -#endif - } - } while (m_stats.m_stopwatch.get_current_seconds() < _TIMELIMIT_ && 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; + lbool res = operator()(); if (res == l_true) { report_tactic_progress("Number of flips:", m_stats.m_moves); @@ -1416,33 +521,66 @@ void sls_engine::operator()(goal_ref const & g, model_converter_ref & mc) { mc = 0; } -unsigned sls_engine::check_restart(unsigned curr_value) +lbool sls_engine::operator()() { + m_tracker.initialize(m_assertions); + lbool res = l_undef; + + do { + checkpoint(); + + report_tactic_progress("Searching... restarts left:", m_max_restarts - m_stats.m_restarts); + res = search(); + + if (res == l_undef) + { + if (m_restart_init) + m_tracker.randomize(m_assertions); + else + m_tracker.reset(m_assertions); + } + } 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; +} + +/* 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) - //if (m_stats.m_restarts % 3 == 2) - 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_limit += (2 << (m_stats.m_restarts / 3)) * _RESTART_LIMIT_; + m_restart_next += (2 << (m_stats.m_restarts >> 1)) * m_restart_base; #else - m_restart_limit += _RESTART_LIMIT_; -#endif -#if _WEIGHT_TOGGLE_ - printf("Setting weight: %f\n", _WEIGHT_DIST_FACTOR_ * (((m_stats.m_restarts & 2) == 0) + 1)); - m_tracker.set_weight_dist_factor(_WEIGHT_DIST_FACTOR_ * (((m_stats.m_restarts & 2) == 0) + 1)); -#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; -} \ No newline at end of file +} diff --git a/src/tactic/sls/sls_engine.h b/src/tactic/sls/sls_engine.h index 902c6b7a0..ff0e55f24 100644 --- a/src/tactic/sls/sls_engine.h +++ b/src/tactic/sls/sls_engine.h @@ -22,6 +22,7 @@ Notes: #include"stopwatch.h" #include"lbool.h" #include"model_converter.h" +#include"goal.h" #include"sls_compilation_settings.h" #include"sls_tracker.h" @@ -35,17 +36,13 @@ public: stopwatch m_stopwatch; unsigned m_full_evals; unsigned m_incr_evals; - unsigned m_moves, m_flips, m_incs, m_decs, m_invs, m_umins, m_mul2s, m_mul3s, m_div2s; + unsigned m_moves, m_flips, m_incs, m_decs, m_invs; stats() : m_restarts(0), m_full_evals(0), m_incr_evals(0), m_moves(0), - m_umins(0), - m_mul2s(0), - m_mul3s(0), - m_div2s(0), m_flips(0), m_incs(0), m_decs(0), @@ -71,14 +68,22 @@ protected: bv_util m_bv_util; sls_tracker m_tracker; 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; - typedef enum { MV_FLIP = 0, MV_INC, MV_DEC, MV_INV, MV_UMIN, MV_MUL2, MV_MUL3, MV_DIV2 } move_type; + typedef enum { MV_FLIP = 0, MV_INC, MV_DEC, MV_INV } move_type; public: sls_engine(ast_manager & m, params_ref const & p); @@ -92,78 +97,46 @@ public: void updt_params(params_ref const & _p); + void assert_expr(expr * e) { m_assertions.push_back(e); } + stats const & get_stats(void) { return m_stats; } void reset_statistics(void) { m_stats.reset(); } - bool full_eval(goal_ref const & g, model & mdl); - + bool full_eval(model & mdl); void mk_add(unsigned bv_sz, const mpz & old_value, mpz & add_value, mpz & result); - void mk_mul2(unsigned bv_sz, const mpz & old_value, mpz & result); - void mk_div2(unsigned bv_sz, const mpz & old_value, mpz & result); void mk_inc(unsigned bv_sz, const mpz & old_value, mpz & incremented); void mk_dec(unsigned bv_sz, const mpz & old_value, mpz & decremented); void mk_inv(unsigned bv_sz, const mpz & old_value, mpz & inverted); - void mk_flip(sort * s, const mpz & old_value, unsigned bit, mpz & flipped); + void mk_flip(sort * s, const mpz & old_value, unsigned bit, mpz & flipped); - double find_best_move(goal_ref const & g, ptr_vector & to_evaluate, double score, - unsigned & best_const, mpz & best_value, unsigned & new_bit, move_type & move); - - double find_best_move_lsb(goal_ref const & g, ptr_vector & to_evaluate, double score, - unsigned & best_const, mpz & best_value, unsigned & new_bit, move_type & move); - - double find_best_move_mc(goal_ref const & g, ptr_vector & to_evaluate, double score, - unsigned & best_const, mpz & best_value); - - double find_best_move_local(expr * e, ptr_vector & to_evaluate, - unsigned & best_const, mpz & best_value, unsigned & new_bit, move_type & move); - - - - bool what_if(goal_ref const & g, expr * e, func_decl * fd, const mpz & temp, - double & best_score, mpz & best_value, unsigned i); - - double find_best_move_local(goal_ref const & g, expr * e, func_decl * fd, mpz & best_value, unsigned i); - - - lbool search(goal_ref const & g); + lbool search(void); + lbool operator()(); void operator()(goal_ref const & g, model_converter_ref & mc); protected: void checkpoint(); - lbool search_old(goal_ref const & g); - double get_restart_armin(unsigned cnt_restarts); - bool what_if(goal_ref const & g, func_decl * fd, const unsigned & fd_inx, const mpz & temp, + bool what_if(func_decl * fd, const unsigned & fd_inx, const mpz & temp, double & best_score, unsigned & best_const, mpz & best_value); - bool what_if_new(goal_ref const & g, func_decl * fd, const unsigned & fd_inx, const mpz & temp, - double & best_score, unsigned & best_const, mpz & best_value); - double incremental_score_prune_new(goal_ref const & g, func_decl * fd, const mpz & new_value); + double top_score(); + double rescore(); + double serious_score(func_decl * fd, const mpz & new_value); + double incremental_score(func_decl * fd, const mpz & new_value); - bool what_if_local(expr * e, func_decl * fd, const unsigned & fd_inx, const mpz & temp, - double & best_score, unsigned & best_const, mpz & best_value); + double incremental_score_prune(func_decl * fd, const mpz & new_value); + double find_best_move(ptr_vector & to_evaluate, double score, + unsigned & best_const, mpz & best_value, unsigned & new_bit, move_type & move); - double top_score(goal_ref const & g); - double rescore(goal_ref const & g); - double serious_score(goal_ref const & g, func_decl * fd, const mpz & new_value); - double incremental_score(goal_ref const & g, func_decl * fd, const mpz & new_value); - -#if _EARLY_PRUNE_ - double incremental_score_prune(goal_ref const & g, func_decl * fd, const mpz & new_value); -#endif - - double find_best_move_vns(goal_ref const & g, ptr_vector & to_evaluate, double score, - unsigned & best_const, mpz & best_value, unsigned & new_bit, move_type & move); + double find_best_move_mc(ptr_vector & to_evaluate, double score, + unsigned & best_const, mpz & best_value); void mk_random_move(ptr_vector & unsat_constants); - void mk_random_move(goal_ref const & g); - - bool handle_plateau(goal_ref const & g); - bool handle_plateau(goal_ref const & g, double old_score); + //inline double get_restart_armin(unsigned cnt_restarts); inline unsigned check_restart(unsigned curr_value); }; -#endif \ No newline at end of file +#endif diff --git a/src/tactic/sls/sls_evaluator.h b/src/tactic/sls/sls_evaluator.h index 78f2cb79a..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)) { @@ -559,8 +542,7 @@ public: (*this)(to_app(cur), new_value); m_tracker.set_value(cur, new_value); -#if _REAL_RS_ || _REAL_PBFS_ - //if (!m_tracker.has_uplinks(cur)) +#if _REAL_RS_ if (m_tracker.is_top_expr(cur)) { if (m_mpz_manager.eq(new_value,m_one)) @@ -570,25 +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.has_uplinks(cur)) - 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.has_uplinks(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)) { @@ -617,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)) { @@ -630,25 +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.has_uplinks(cur)) - 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.has_uplinks(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); @@ -684,11 +638,7 @@ public: m_traversal_stack[cur_depth].push_back(ep); if (cur_depth > max_depth) max_depth = cur_depth; } -#if _REAL_RS_ || _REAL_PBFS_ || _PAWS_ run_serious_update(max_depth); -#else - run_update(max_depth); -#endif } void update(func_decl * fd, const mpz & new_value) { @@ -713,7 +663,6 @@ public: run_serious_update(cur_depth); } -#if _EARLY_PRUNE_ unsigned run_update_bool_prune(unsigned cur_depth) { expr_fast_mark1 visited; @@ -727,19 +676,15 @@ public: expr * cur = cur_depth_exprs[i]; new_score = m_tracker.score(cur); -#if _CACHE_TOP_SCORE_ - //if (!m_tracker.has_uplinks(cur)) 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); if ((new_score > prune_score) && (m_tracker.has_pos_occ(cur))) - //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))) - //if ((new_score < prune_score) && (m_tracker.has_neg_occ(cur))) pot_benefits = 1; if (m_tracker.has_uplinks(cur)) { @@ -754,9 +699,6 @@ public: } } } - else - { - } } cur_depth_exprs.reset(); @@ -770,15 +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.has_uplinks(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++) { @@ -859,161 +797,18 @@ 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.has_uplinks(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.has_uplinks(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 _all_ candidates: - - //// bool did_something = false; - //for (unsigned i = 0; i < unsat_constants.size(); i++) { - // func_decl * fd = unsat_constants[i]; - // mpz temp = m_tracker.get_random(fd->get_range()); - // // if (m_mpz_manager.neq(temp, m_tracker.get_value(fd))) { - // // did_something = true; - // // } - // update(fd, temp); - // m_mpz_manager.del(temp); - //} - // Randomize _one_ candidate: unsigned r = m_tracker.get_random_uint(16) % unsat_constants.size(); func_decl * fd = unsat_constants[r]; -#if _PERC_CHANGE_ - sort * srt = fd->get_range(); - mpz temp; - - if (m_manager.is_bool(srt)) - m_mpz_manager.set(temp, (m_mpz_manager.is_zero(m_tracker.get_value(fd))) ? m_one : m_zero); - else - { - mpz temp2, mask; - unsigned bv_sz = m_bv_util.get_bv_size(srt); - m_mpz_manager.set(temp, m_tracker.get_value(fd)); - - for (unsigned bit = 0; bit < bv_sz; bit++) - if (m_tracker.get_random_uint(16) % 100 < _PERC_CHANGE_) - { - m_mpz_manager.set(mask, m_powers(bit)); - m_mpz_manager.bitwise_xor(temp, mask, temp2); - m_mpz_manager.set(temp, temp2); - } - m_mpz_manager.del(mask); - m_mpz_manager.del(temp2); - } -#else mpz temp = m_tracker.get_random(fd->get_range()); -#endif -#if _REAL_RS_ || _REAL_PBFS_ || _PAWS_ serious_update(fd, temp); -#else - update(fd, temp); -#endif + m_mpz_manager.del(temp); - TRACE("sls", /*tout << "Randomization candidates: "; - for (unsigned i = 0; i < unsat_constants.size(); i++) - tout << unsat_constants[i]->get_name() << ", "; - tout << std::endl;*/ - tout << "Randomization candidate: " << unsat_constants[r]->get_name() << std::endl; + TRACE("sls", tout << "Randomization candidate: " << unsat_constants[r]->get_name() << std::endl; tout << "Locally randomized model: " << std::endl; m_tracker.show_model(tout); ); @@ -1023,36 +818,9 @@ public: randomize_local(m_tracker.get_constants(e)); } - void randomize_local(goal_ref const & g, unsigned int flip) { - randomize_local(m_tracker.get_unsat_constants(g, flip)); + void randomize_local(ptr_vector const & as) { + randomize_local(m_tracker.get_unsat_constants(as)); } - - void randomize_local_n(goal_ref const & g, ptr_vector & unsat_constants) { - unsigned r = m_tracker.get_random_uint(16) % unsat_constants.size(); - func_decl * fd = unsat_constants[r]; - sort * srt = fd->get_range(); - unsigned bv_sz = m_manager.is_bool(srt) ? 1 : m_bv_util.get_bv_size(srt); - mpz max_val = m_tracker.get_random(srt); - update(fd, max_val); - double max_score = m_tracker.get_top_sum() / g->size(); - mpz temp_val; - double temp_score; - for (unsigned i = 1; i < 2; i++) - //for (unsigned i = 1; i < bv_sz; i++) - { - m_mpz_manager.set(temp_val, m_tracker.get_random(srt)); - update(fd, temp_val); - temp_score = m_tracker.get_top_sum() / g->size(); - if (temp_score > max_score) - { - m_mpz_manager.set(max_val, temp_val); - max_score = temp_score; - } - } - update(fd, max_val); - m_mpz_manager.del(temp_val); - m_mpz_manager.del(max_val); - } }; #endif \ No newline at end of file diff --git a/src/tactic/sls/sls_tactic.cpp b/src/tactic/sls/sls_tactic.cpp index 0b6b01e7c..6e1102dd2 100644 --- a/src/tactic/sls/sls_tactic.cpp +++ b/src/tactic/sls/sls_tactic.cpp @@ -1507,16 +1507,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 87c90f1f8..65011dc8d 100644 --- a/src/tactic/sls/sls_tracker.h +++ b/src/tactic/sls/sls_tracker.h @@ -20,7 +20,9 @@ Notes: #ifndef _SLS_TRACKER_H_ #define _SLS_TRACKER_H_ -#include"goal.h" +#include"for_each_expr.h" +#include"ast_smt2_pp.h" +#include"bv_decl_plugin.h" #include"model.h" #include"sls_compilation_settings.h" @@ -37,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; @@ -78,24 +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 -#if _REAL_RS_ || _REAL_PBFS_ + 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; - //obj_map m_weights; -#endif -#if _CACHE_TOP_SCORE_ double m_top_sum; -#endif -#if _WEIGHT_DIST_ == 4 || _WEIGHT_TOGGLE_ - double m_weight_dist_factor; -#endif unsigned m_equal_scores; public: @@ -116,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(); } @@ -141,12 +148,6 @@ public: return sum / count; } -#if _WEIGHT_DIST_ == 4 || _WEIGHT_TOGGLE_ - inline void set_weight_dist_factor(double val) { - m_weight_dist_factor = val; - } -#endif - void reset_equal_scores() { m_equal_scores = 1; } @@ -155,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) { @@ -171,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)); @@ -217,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; @@ -237,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)); @@ -271,7 +264,7 @@ public: return m_uplinks.find(n); } -#if _REAL_RS_ || _REAL_PBFS_ +#if _REAL_RS_ void debug_real(goal_ref const & g, unsigned flip) { unsigned count = 0; @@ -318,21 +311,22 @@ public: } #endif -#if _UCT_ - void uct_forget(goal_ref const & g) { - expr * e; - unsigned touched_old, touched_new; - - for (unsigned i = 0; i < g->size(); i++) + inline void ucb_forget(ptr_vector & as) { + if (m_ucb_forget < 1.0) { - e = g->form(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; + } } } -#endif void initialize(app * n) { // Build score table @@ -409,12 +403,12 @@ public: } }; - void calculate_expr_distances(goal_ref const & g) { + void calculate_expr_distances(ptr_vector const & as) { // precondition: m_scores is set up. - unsigned sz = g->size(); + unsigned sz = as.size(); ptr_vector stack; for (unsigned i = 0; i < sz; i++) - stack.push_back(to_app(g->form(i))); + stack.push_back(to_app(as[i])); while (!stack.empty()) { app * cur = stack.back(); stack.pop_back(); @@ -462,31 +456,24 @@ public: quick_for_each_expr(ffd_proc, visited, e); } - void initialize(goal_ref const & g) { + void initialize(ptr_vector const & as) { init_proc proc(m_manager, *this); expr_mark visited; - unsigned sz = g->size(); + unsigned sz = as.size(); for (unsigned i = 0; i < sz; i++) { - expr * e = g->form(i); + expr * e = as[i]; if (!m_top_expr.contains(e)) m_top_expr.insert(e); else printf("this is already in ...\n"); - // Andreas: Maybe not fully correct. -#if _FOCUS_ == 2 - initialize_recursive(proc, visited, e); -#endif for_each_expr(proc, visited, e); } visited.reset(); for (unsigned i = 0; i < sz; i++) { - expr * e = g->form(i); + expr * e = as[i]; // Andreas: Maybe not fully correct. -#if _FOCUS_ == 2 || _INTENSIFICATION_ - initialize_recursive(e); -#endif ptr_vector t; m_constants_occ.insert_if_not_there(e, t); find_func_decls_proc ffd_proc(m_manager, m_constants_occ.find(e)); @@ -494,11 +481,11 @@ public: quick_for_each_expr(ffd_proc, visited, e); } - calculate_expr_distances(g); + calculate_expr_distances(as); TRACE("sls", tout << "Initial model:" << std::endl; show_model(tout); ); -#if _REAL_RS_ || _REAL_PBFS_ +#if _REAL_RS_ m_list_false = new expr*[sz]; //for (unsigned i = 0; i < sz; i++) //{ @@ -507,50 +494,38 @@ public: //} #endif -#if _PAWS_ for (unsigned i = 0; i < sz; i++) { - expr * e = g->form(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(g->form(i)); + setup_occs(as[i]); #endif -#if _UCT_ - m_touched = _UCT_INIT_ ? g->size() : 1; -#endif + m_touched = m_ucb_init ? as.size() : 1; } -#if _PAWS_ void increase_weight(expr * e) { - //printf("Increasing %d to", m_weights.find(e)); m_weights.find(e)++; - //m_weights.find(e) *= 1.1; - //printf(" %d\n", m_weights.find(e)); } 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 > 1.1 ? old_weight / 1.1 : 1; - //printf("Decreasing %d to %d\n", old_weight, m_weights.find(e)); + m_weights.find(e) = old_weight > m_paws_init ? old_weight - 1 : m_paws_init; } unsigned get_weight(expr * e) - //double get_weight(expr * e) { return m_weights.find(e); } -#endif -#if _REAL_RS_ || _REAL_PBFS_ +#if _REAL_RS_ void make_assertion(expr * e) { if (m_where_false.contains(e)) @@ -683,7 +658,7 @@ public: NOT_IMPLEMENTED_YET(); // This only works for bit-vectors for now. } - void randomize(goal_ref const & g) { + void randomize(ptr_vector const & as) { TRACE("sls", tout << "Abandoned model:" << std::endl; show_model(tout); ); for (entry_point_type::iterator it = m_entry_points.begin(); it != m_entry_points.end(); it++) { @@ -695,15 +670,9 @@ public: } TRACE("sls", tout << "Randomized model:" << std::endl; show_model(tout); ); - -#if _UCT_RESET_ - m_touched = _UCT_INIT_ ? g->size() : 1; - for (unsigned i = 0; i < g->size(); i++) - m_scores.find(g->form(i)).touched = 1; -#endif } - void reset(goal_ref const & g) { + void reset(ptr_vector const & as) { TRACE("sls", tout << "Abandoned model:" << std::endl; show_model(tout); ); for (entry_point_type::iterator it = m_entry_points.begin(); it != m_entry_points.end(); it++) { @@ -711,15 +680,8 @@ public: set_value(it->m_value, temp); m_mpz_manager.del(temp); } - -#if _UCT_RESET_ - m_touched = _UCT_INIT_ ? g->size() : 1; - for (unsigned i = 0; i < g->size(); i++) - m_scores.find(g->form(i)).touched = 1; -#endif } -#if _EARLY_PRUNE_ void setup_occs(expr * n, bool negated = false) { if (m_manager.is_bool(n)) { @@ -752,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; ); @@ -770,57 +731,29 @@ 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++) -#if _DIRTY_UP_ - sum += is_top_expr(args[i]) ? 1.0 : get_score(args[i]); -#else sum += get_score(args[i]); -#endif - 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++) { -#if _DIRTY_UP_ - double cur = is_top_expr(args[i]) ? 1.0 : get_score(args[i]); -#else double cur = get_score(args[i]); -#endif if (cur < min) min = cur; } res = min; -#endif } else if (m_manager.is_or(n)) { SASSERT(!negated); app * a = to_app(n); expr * const * args = a->get_args(); // Andreas: Seems to have no effect. Probably it is still too similar to the original version. -#if _SCORE_OR_MUL_ - double inv = 1.0; - for (unsigned i = 0; i < a->get_num_args(); i++) { -#if _DIRTY_UP_ - double cur = is_top_expr(args[i]) ? 1.0 : get_score(args[i]); -#else - double cur = get_score(args[i]); -#endif - inv *= (1.0 - get_score(args[i])); - } - res = 1.0 - inv; -#else double max = 0.0; for (unsigned i = 0; i < a->get_num_args(); i++) { -#if _DIRTY_UP_ - double cur = is_top_expr(args[i]) ? 1.0 : get_score(args[i]); -#else double cur = get_score(args[i]); -#endif if (cur > max) max = cur; } res = max; -#endif } else if (m_manager.is_ite(n)) { SASSERT(!negated); @@ -855,24 +788,14 @@ public: m_mpz_manager.bitwise_xor(v0, v1, diff); unsigned hamming_distance = 0; unsigned bv_sz = m_bv_util.get_bv_size(arg0); - #if 1 // unweighted hamming distance + // unweighted hamming distance while (!m_mpz_manager.is_zero(diff)) { - //m_mpz_manager.set(diff_m1, diff); - //m_mpz_manager.dec(diff_m1); - //m_mpz_manager.bitwise_and(diff, diff_m1, diff); - //hamming_distance++; if (!m_mpz_manager.is_even(diff)) { hamming_distance++; } m_mpz_manager.machine_div(diff, m_two, diff); } res = 1.0 - (hamming_distance / (double) bv_sz); - #else - rational r(diff); - r /= m_powers(bv_sz); - double dbl = r.get_double(); - res = (dbl < 0.0) ? 1.0 : (dbl > 1.0) ? 0.0 : 1.0 - dbl; - #endif TRACE("sls_score", tout << "V0 = " << m_mpz_manager.to_string(v0) << " ; V1 = " << m_mpz_manager.to_string(v1) << " ; HD = " << hamming_distance << " ; SZ = " << bv_sz << std::endl; ); @@ -891,205 +814,36 @@ public: if (negated) { if (m_mpz_manager.gt(x, y)) - { - /*mpz diff; - m_mpz_manager.sub(x, y, diff); - m_mpz_manager.inc(diff); - rational n(diff); - n /= rational(m_powers(bv_sz)); - double dbl = n.get_double(); - // In extreme cases, n is 0.9999 but to_double returns something > 1.0 - m_mpz_manager.del(diff); - res = 1.0 + 0.5 * dbl;*/ res = 1.0; - } else { - //res = (bv_sz - 1.0) / bv_sz; -/* mpz x_copy, y_copy; - m_mpz_manager.set(x_copy, x); - m_mpz_manager.set(y_copy, y); - unsigned lower_gt = 0; - unsigned curr_gt = 0; - int last_pos = -1; - for (int i = 0; i < bv_sz; i++) - { - if (m_mpz_manager.is_odd(x_copy) && m_mpz_manager.is_even(y_copy)) - { - lower_gt = curr_gt; - curr_gt = 1; - last_pos = i; - } - else if (m_mpz_manager.is_even(x_copy) && m_mpz_manager.is_odd(y_copy)) - { - lower_gt = curr_gt; - curr_gt = 0; - last_pos = i; - } - - m_mpz_manager.machine_div(x_copy, m_two, x_copy); - m_mpz_manager.machine_div(y_copy, m_two, y_copy); - } - - res = (double)(bv_sz - last_pos - 1 + 2 * lower_gt) / (double)(bv_sz + 2); - m_mpz_manager.del(x_copy); - m_mpz_manager.del(y_copy);*/ -#if 1 mpz diff; m_mpz_manager.sub(y, x, diff); m_mpz_manager.inc(diff); rational n(diff); n /= rational(m_powers(bv_sz)); - double dbl = 1.0 - n.get_double(); + double dbl = n.get_double(); // In extreme cases, n is 0.9999 but to_double returns something > 1.0 - res = (dbl > 1.0) ? 1.0 : (dbl < 0.0) ? 0.0 : dbl; - //res = (dbl > 1.0) ? 0.0 : (dbl < 0.0) ? 1.0 : 1.0 - dbl; + res = (dbl > 1.0) ? 0.0 : (dbl < 0.0) ? 1.0 : 1.0 - dbl; m_mpz_manager.del(diff); -#endif } } else { if (m_mpz_manager.le(x, y)) - { - /*mpz diff; - m_mpz_manager.sub(y, x, diff); - m_mpz_manager.inc(diff); - rational n(diff); - n /= rational(m_powers(bv_sz)); - double dbl = n.get_double(); - // In extreme cases, n is 0.9999 but to_double returns something > 1.0 - m_mpz_manager.del(diff); - res = 1.0 + 0.5 * dbl;*/ res = 1.0; - } else { - //res = (bv_sz - 1.0) / bv_sz; -/* mpz x_copy, y_copy; - m_mpz_manager.set(x_copy, x); - m_mpz_manager.set(y_copy, y); - unsigned lower_le = 1; - unsigned curr_le = 1; - int last_pos = -1; - for (int i = 0; i < bv_sz; i++) - { - if (m_mpz_manager.is_odd(x_copy) && m_mpz_manager.is_even(y_copy)) - { - lower_le = curr_le; - curr_le = 0; - last_pos = i; - } - else if (m_mpz_manager.is_even(x_copy) && m_mpz_manager.is_odd(y_copy)) - { - lower_le = curr_le; - curr_le = 1; - last_pos = i; - } - - m_mpz_manager.machine_div(x_copy, m_two, x_copy); - m_mpz_manager.machine_div(y_copy, m_two, y_copy); - } - - res = (double)(bv_sz - last_pos - 1 + 2 * lower_le) / (double)(bv_sz + 2);*/ -#if 1 mpz diff; m_mpz_manager.sub(x, y, diff); rational n(diff); n /= rational(m_powers(bv_sz)); - double dbl = 1.0 - n.get_double(); - res = (dbl > 1.0) ? 1.0 : (dbl < 0.0) ? 0.0 : dbl; + double dbl = n.get_double(); + res = (dbl > 1.0) ? 0.0 : (dbl < 0.0) ? 1.0 : 1.0 - dbl; m_mpz_manager.del(diff); -#endif } } TRACE("sls_score", tout << "x = " << m_mpz_manager.to_string(x) << " ; y = " << m_mpz_manager.to_string(y) << " ; SZ = " << bv_sz << std::endl; ); } -/* else if (m_bv_util.is_bv_sle(n)) { // x <= y - app * a = to_app(n); - SASSERT(a->get_num_args() == 2); - const mpz & x = get_value(a->get_arg(0)); - const mpz & y = get_value(a->get_arg(1)); - int bv_sz = m_bv_util.get_bv_size(a->get_decl()->get_domain()[0]); - - mpz x_unsigned; - mpz y_unsigned; - const mpz & p = m_powers(bv_sz); - const mpz & p_half = m_powers(bv_sz-1); - if (x >= p_half) { m_mpz_manager.sub(x, p, x_unsigned); } - if (y >= p_half) { m_mpz_manager.sub(y, p, y_unsigned); } - - if (negated) { - if (x_unsigned > y_unsigned) - res = 1.0; - else { - mpz x_copy, y_copy; - m_mpz_manager.set(x_copy, x); - m_mpz_manager.set(y_copy, y); - unsigned lower_gt = 0; - unsigned curr_gt = 0; - int last_pos = -1; - for (int i = 0; i < bv_sz; i++) - { - if (m_mpz_manager.is_odd(x_copy) && m_mpz_manager.is_even(y_copy)) - { - lower_gt = curr_gt; - curr_gt = 1; - last_pos = i; - } - else if (m_mpz_manager.is_even(x_copy) && m_mpz_manager.is_odd(y_copy)) - { - lower_gt = curr_gt; - curr_gt = 0; - last_pos = i; - } - - m_mpz_manager.machine_div(x_copy, m_two, x_copy); - m_mpz_manager.machine_div(y_copy, m_two, y_copy); - } - - res = (double)(bv_sz - last_pos - 1 + 2 * lower_gt) / (double)(bv_sz + 2); - m_mpz_manager.del(x_copy); - m_mpz_manager.del(y_copy); - } - } - else { - if (x_unsigned <= y_unsigned) - res = 1.0; - else { - mpz x_copy, y_copy; - m_mpz_manager.set(x_copy, x); - m_mpz_manager.set(y_copy, y); - unsigned lower_le = 1; - unsigned curr_le = 1; - int last_pos = -1; - for (int i = 0; i < bv_sz; i++) - { - if (m_mpz_manager.is_odd(x_copy) && m_mpz_manager.is_even(y_copy)) - { - lower_le = curr_le; - curr_le = 0; - last_pos = i; - } - else if (m_mpz_manager.is_even(x_copy) && m_mpz_manager.is_odd(y_copy)) - { - lower_le = curr_le; - curr_le = 1; - last_pos = i; - } - - m_mpz_manager.machine_div(x_copy, m_two, x_copy); - m_mpz_manager.machine_div(y_copy, m_two, y_copy); - } - - res = (double)(bv_sz - last_pos - 1 + 2 * lower_le) / (double)(bv_sz + 2); - } - } - TRACE("sls_score", tout << "x = " << m_mpz_manager.to_string(x) << " ; y = " << - m_mpz_manager.to_string(y) << " ; SZ = " << bv_sz << std::endl; ); - - m_mpz_manager.del(x_unsigned); - m_mpz_manager.del(y_unsigned); - }*/ - else if (m_bv_util.is_bv_sle(n)) { // x <= y + else if (m_bv_util.is_bv_sle(n)) { // x <= y app * a = to_app(n); SASSERT(a->get_num_args() == 2); mpz x; m_mpz_manager.set(x, get_value(a->get_arg(0))); @@ -1102,61 +856,32 @@ public: if (negated) { if (x > y) - { - /*mpz diff; - m_mpz_manager.sub(x, y, diff); - m_mpz_manager.inc(diff); - rational n(diff); - n /= rational(m_powers(bv_sz)); - double dbl = n.get_double(); - // In extreme cases, n is 0.9999 but to_double returns something > 1.0 - m_mpz_manager.del(diff); - res = 1.0 + 0.5 * dbl;*/ res = 1.0; - } else { - //res = (bv_sz - 1.0) / bv_sz; -#if 1 mpz diff; m_mpz_manager.sub(y, x, diff); m_mpz_manager.inc(diff); rational n(diff); n /= p; - double dbl = 1.0 - n.get_double(); - //res = (dbl > 1.0) ? 0.0 : (dbl < 0.0) ? 1.0 : 1.0 - dbl; - res = (dbl > 1.0) ? 1.0 : (dbl < 0.0) ? 0.0 : dbl; + double dbl = n.get_double(); + res = (dbl > 1.0) ? 0.0 : (dbl < 0.0) ? 1.0 : 1.0 - dbl; m_mpz_manager.del(diff); -#endif } TRACE("sls_score", tout << "x = " << m_mpz_manager.to_string(x) << " ; y = " << m_mpz_manager.to_string(y) << " ; SZ = " << bv_sz << std::endl; ); } else { if (x <= y) - { - /*mpz diff; - m_mpz_manager.sub(y, x, diff); - m_mpz_manager.inc(diff); - rational n(diff); - n /= rational(m_powers(bv_sz)); - double dbl = n.get_double(); - // In extreme cases, n is 0.9999 but to_double returns something > 1.0 - m_mpz_manager.del(diff); - res = 1.0 + 0.5 * dbl;*/ res = 1.0; - } else { - //res = (bv_sz - 1.0) / bv_sz; -#if 1 mpz diff; m_mpz_manager.sub(x, y, diff); SASSERT(!m_mpz_manager.is_neg(diff)); rational n(diff); n /= p; - double dbl = 1.0 - n.get_double(); - res = (dbl > 1.0) ? 1.0 : (dbl < 0.0) ? 0.0 : dbl; + double dbl = n.get_double(); + res = (dbl > 1.0) ? 0.0 : (dbl < 0.0) ? 1.0 : 1.0 - dbl; m_mpz_manager.del(diff); -#endif } TRACE("sls_score", tout << "x = " << m_mpz_manager.to_string(x) << " ; y = " << m_mpz_manager.to_string(y) << " ; SZ = " << bv_sz << std::endl; ); @@ -1171,11 +896,7 @@ public: expr * child = a->get_arg(0); if (m_manager.is_and(child) || m_manager.is_or(child)) // Precondition: Assertion set is in NNF. NOT_IMPLEMENTED_YET(); -#if _DIRTY_UP_ - res = is_top_expr(child) ? 0.0 : score_bool(child, true); -#else res = score_bool(child, true); -#endif } else if (m_manager.is_distinct(n)) { app * a = to_app(n); @@ -1199,25 +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()) -#endif -#if _WEIGHT_DIST_ == 1 -#if _WEIGHT_TOGGLE_ - if (res < 1.0) res *= m_weight_dist_factor; -#else - if (res < 1.0) res *= _WEIGHT_DIST_FACTOR_; -#endif -#elif _WEIGHT_DIST_ == 2 - res *= res; -#elif _WEIGHT_DIST_ == 3 - if (res < 1.0) res = 0.0; -#elif _WEIGHT_DIST_ == 4 - if (res < 1.0) res *= m_weight_dist_factor; -#endif + if (res < 1.0) res *= m_scale_unsat; TRACE("sls_score", tout << "SCORE = " << res << std::endl; ); return res; @@ -1268,33 +975,6 @@ public: NOT_IMPLEMENTED_YET(); } - expr * get_unsat_expression(expr * e) { - if (m_manager.is_bool(e)) { - if (m_manager.is_and(e) || m_manager.is_or(e)) { - app * a = to_app(e); - expr * const * args = a->get_args(); - // Andreas: might be used for guided branching - //for (unsigned i = 0; i < a->get_num_args(); i++) { - //double cur = get_score(args[i]); - //} - // Andreas: A random number is better here since reusing flip will cause patterns. - unsigned int sz = a->get_num_args(); - unsigned int pos = get_random_uint(16) % sz; - for (unsigned int i = pos; i < sz; i++) { - expr * q = args[i]; - if (m_mpz_manager.neq(get_value(q), m_one)) - return get_unsat_expression(q); - } - for (unsigned int i = 0; i < pos; i++) { - expr * q = args[i]; - if (m_mpz_manager.neq(get_value(q), m_one)) - return get_unsat_expression(q); - } - } - } - return e; - } - ptr_vector & get_constants(expr * e) { ptr_vector const & this_decls = m_constants_occ.find(e); unsigned sz = this_decls.size(); @@ -1306,13 +986,17 @@ public: return m_temp_constants; } - ptr_vector & get_unsat_constants_gsat(goal_ref const & g, unsigned sz) { - if (sz == 1) - return get_constants(); + 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(); + } + m_temp_constants.reset(); for (unsigned i = 0; i < sz; i++) { - expr * q = g->form(i); + expr * q = as[i]; if (m_mpz_manager.eq(get_value(q), m_one)) continue; ptr_vector const & this_decls = m_constants_occ.find(q); @@ -1326,35 +1010,6 @@ public: return m_temp_constants; } - expr * get_unsat_assertion(goal_ref const & g, unsigned sz, unsigned int pos) { - for (unsigned i = pos; i < sz; i++) { - expr * q = g->form(i); - if (m_mpz_manager.neq(get_value(q), m_one)) - return q; - } - for (unsigned i = 0; i < pos; i++) { - expr * q = g->form(i); - if (m_mpz_manager.neq(get_value(q), m_one)) - return q; - } - return 0; - } - - ptr_vector & get_unsat_constants_walksat(goal_ref const & g, unsigned sz, unsigned int pos) { - expr * q = get_unsat_assertion(g, sz, pos); - // Andreas: I should probably fix this. If this is the case then the formula is SAT anyway but this is not checked in the first iteration. - if (!q) - return m_temp_constants; - ptr_vector const & this_decls = m_constants_occ.find(q); - unsigned sz2 = this_decls.size(); - for (unsigned j = 0; j < sz2; j++) { - func_decl * fd = this_decls[j]; - if (!m_temp_constants.contains(fd)) - m_temp_constants.push_back(fd); - } - return m_temp_constants; - } - ptr_vector & get_unsat_constants_walksat(expr * e) { if (!e || m_temp_constants.size()) return m_temp_constants; @@ -1368,420 +1023,89 @@ public: return m_temp_constants; } - ptr_vector & go_deeper(expr * e) { - if (m_manager.is_bool(e)) { - if (m_manager.is_and(e)) { - app * a = to_app(e); - expr * const * args = a->get_args(); - // Andreas: might be used for guided branching - //for (unsigned i = 0; i < a->get_num_args(); i++) { - //double cur = get_score(args[i]); - //} - // Andreas: A random number is better here since reusing flip will cause patterns. - unsigned int sz = a->get_num_args(); - unsigned int pos = get_random_uint(16) % sz; - for (unsigned int i = pos; i < sz; i++) { - expr * q = args[i]; - if (m_mpz_manager.neq(get_value(q), m_one)) - return go_deeper(q); - } - for (unsigned int i = 0; i < pos; i++) { - expr * q = args[i]; - if (m_mpz_manager.neq(get_value(q), m_one)) - return go_deeper(q); - } - } - else if (m_manager.is_or(e)) { - app * a = to_app(e); - expr * const * args = a->get_args(); - unsigned int sz = a->get_num_args(); - unsigned int pos = get_random_uint(16) % sz; - for (unsigned int i = pos; i < sz; i++) { - expr * q = args[i]; - if (m_mpz_manager.neq(get_value(q), m_one)) - return go_deeper(q); - } - for (unsigned int i = 0; i < pos; i++) { - expr * q = args[i]; - if (m_mpz_manager.neq(get_value(q), m_one)) - return go_deeper(q); - } - } - } - ptr_vector const & this_decls = m_constants_occ.find(e); - unsigned sz2 = this_decls.size(); - for (unsigned j = 0; j < sz2; j++) { - func_decl * fd = this_decls[j]; - if (!m_temp_constants.contains(fd)) - m_temp_constants.push_back(fd); - } - return m_temp_constants; - } + ptr_vector & get_unsat_constants(ptr_vector const & as) { + if (m_walksat) + { + expr * e = get_unsat_assertion(as); - ptr_vector & get_unsat_constants_crsat(goal_ref const & g, unsigned sz, unsigned int pos) { - expr * q = get_unsat_assertion(g, sz, pos); - if (!q) - return m_temp_constants; - - return go_deeper(q); - } - - void go_deeper_only(expr * e) { - //if (m_manager.is_bool(e)) { - if (m_manager.is_and(e)) { - app * a = to_app(e); - expr * const * args = a->get_args(); - unsigned int sz = a->get_num_args(); - unsigned cnt_unsat = 0, pos = -1; - for (unsigned int i = 0; i < sz; i++) { - expr * q = args[i]; - if (m_mpz_manager.neq(get_value(q), m_one) && (get_random_uint(16) % ++cnt_unsat == 0)) pos = i; - //if (m_mpz_manager.neq(get_value(q), m_one)) go_deeper(q); - } - go_deeper(args[pos]); - } - else if (m_manager.is_or(e)) { - app * a = to_app(e); - expr * const * args = a->get_args(); - unsigned int sz = a->get_num_args(); - for (unsigned int i = 0; i < sz; i++) { - expr * q = args[i]; - go_deeper(q); - } - } - //} - else - { - ptr_vector const & this_decls = m_constants_occ.find(e); - unsigned sz2 = this_decls.size(); - for (unsigned j = 0; j < sz2; j++) { - func_decl * fd = this_decls[j]; - if (!m_temp_constants.contains(fd)) - m_temp_constants.push_back(fd); - } - } - } - - ptr_vector & get_unsat_constants_only(expr * e) { - if (e && !m_temp_constants.size()) - go_deeper_only(e); - - return m_temp_constants; - } - - ptr_vector & get_unsat_constants(goal_ref const & g, unsigned int flip) { - unsigned sz = g->size(); - - if (sz == 1) { - if (m_mpz_manager.eq(get_value(g->form(0)), m_one)) + if (!e) { m_temp_constants.reset(); return m_temp_constants; } - else - return get_constants(); - } - else { - m_temp_constants.reset(); -#if _FOCUS_ == 1 -#if _UCT_ - unsigned pos = -1; - value_score vscore; -#if _PROBABILISTIC_UCT_ - double sum_score = 0.0; - unsigned start_index = get_random_uint(16) % sz; - for (unsigned i = start_index; i < sz; i++) - { - expr * e = g->form(i); - vscore = m_scores.find(e); - -#if _PROBABILISTIC_UCT_ == 2 - double q = vscore.score * vscore.score; -#else - double q = vscore.score + _UCT_CONSTANT_ * sqrt(log(m_touched)/vscore.touched) + _UCT_EPS_; -#endif - if (m_mpz_manager.neq(get_value(g->form(i)), m_one)) { - sum_score += q; - if (rand() <= (q * RAND_MAX / sum_score) + 1) - pos = i; - } - } - for (unsigned i = 0; i < start_index; i++) - { - expr * e = g->form(i); - vscore = m_scores.find(e); -#if _PROBABILISTIC_UCT_ == 2 - double q = vscore.score * vscore.score; -#else - double q = vscore.score + _UCT_CONSTANT_ * sqrt(log(m_touched)/vscore.touched) + _UCT_EPS_; -#endif - if (m_mpz_manager.neq(get_value(g->form(i)), m_one)) { - sum_score += q; - if (rand() <= (q * RAND_MAX / sum_score) + 1) - pos = i; - } - } -#else - double max = -1.0; - for (unsigned i = 0; i < sz; i++) { - expr * e = g->form(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_ == 2 - double q = vscore.score + (_UCT_CONSTANT_ * (flip - vscore.touched)) / sz; -#elif _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; } - } -#endif - if (pos == static_cast(-1)) - return m_temp_constants; - -#if _UCT_ == 1 || _UCT_ == 3 - m_scores.find(g->form(pos)).touched++; - m_touched++; -#elif _UCT_ == 2 - m_scores.find(g->form(pos)).touched = flip; -#endif - expr * e = g->form(pos); -// expr * e = m_list_false[pos]; - -#elif _BFS_ == 3 - unsigned int pos = -1; - double max = -1.0; - for (unsigned i = 0; i < sz; i++) { - expr * e = g->form(i); - double q = get_score(e); - if (q > max && m_mpz_manager.neq(get_value(e), m_one) ) { max = q; pos = i; } - } - if (pos == static_cast(-1)) - return m_temp_constants; - expr * e = g->form(pos); -#elif _BFS_ == 2 - unsigned int pos = -1; - double min = 2.0; - for (unsigned i = 0; i < sz; i++) { - expr * e = g->form(i); - double q = get_score(e); - if (q < min && m_mpz_manager.neq(get_value(e), m_one) ) { min = q; pos = i; } - } - if (pos == static_cast(-1)) - return m_temp_constants; - expr * e = g->form(pos); -#elif _BFS_ == 1 - // I guess it was buggy ... - // unsigned int pos = flip % m_constants.size(); - unsigned int pos = flip % sz; - expr * e = get_unsat_assertion(g, sz, pos); -#elif _UNIFORM_RANDOM_ - 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)) pos = i; - if (pos == static_cast(-1)) - return m_temp_constants; - expr * e = g->form(pos); -#elif _REAL_RS_ - //unsigned pos = m_false_list[get_random_uint(16) % m_cnt_false]; - //expr * e = get_unsat_assertion(g, sz, pos); - //expr * e = m_unsat_expr[get_random_uint(16) % m_unsat_expr.size()]; - sz = m_where_false.size(); - if (sz == 0) - return m_temp_constants; - expr * e = m_list_false[get_random_uint(16) % sz]; -#elif _REAL_PBFS_ - //unsigned pos = m_false_list[flip % m_cnt_false]; - //expr * e = get_unsat_assertion(g, sz, pos); - //expr * e = m_unsat_expr[flip % m_unsat_expr.size()]; - sz = m_where_false.size(); - if (sz == 0) - return m_temp_constants; - else - expr * e = m_list_false[flip % sz]; -#else - // I guess it was buggy ... - // unsigned int pos = get_random_uint(16) % m_constants.size(); - unsigned int pos = get_random_uint(16) % sz; - expr * e = get_unsat_assertion(g, sz, pos); -#endif return get_unsat_constants_walksat(e); -#elif _FOCUS_ == 2 -#if _BFS_ - // I guess it was buggy ... - // unsigned int pos = flip % m_constants.size(); - unsigned int pos = flip % sz; -#else - // I guess it was buggy ... - // unsigned int pos = get_random_uint(16) % m_constants.size(); - unsigned int pos = get_random_uint(16) % sz; -#endif - return get_unsat_constants_crsat(g, sz, pos); -#else - return get_unsat_constants_gsat(g, sz); -#endif } + else + return get_unsat_constants_gsat(as); } - expr * get_unsat_assertion(goal_ref const & g, unsigned int flip) { - unsigned sz = g->size(); - + expr * get_unsat_assertion(ptr_vector const & as) { + unsigned sz = as.size(); if (sz == 1) { - if (m_mpz_manager.eq(get_value(g->form(0)), m_zero)) - return g->form(0); + if (m_mpz_manager.neq(get_value(as[0]), m_one)) + return as[0]; else return 0; } - m_temp_constants.reset(); -#if _FOCUS_ == 1 -#if _UCT_ + unsigned pos = -1; - value_score vscore; -#if _PROBABILISTIC_UCT_ - double sum_score = 0.0; - unsigned start_index = get_random_uint(16) % sz; - - for (unsigned i = start_index; i < sz; i++) + if (m_ucb) { - expr * e = g->form(i); - vscore = m_scores.find(e); -#if _PROBABILISTIC_UCT_ == 2 - double q = vscore.score * vscore.score + _UCT_EPS_; -#else - double q = vscore.score + _UCT_CONSTANT_ * sqrt(log(m_touched)/vscore.touched) + _UCT_EPS_; -#endif - if (m_mpz_manager.neq(get_value(g->form(i)), m_one)) { - sum_score += q; - if (rand() <= (q * RAND_MAX / sum_score) + 1) - pos = i; - } - } - for (unsigned i = 0; i < start_index; i++) - { - expr * e = g->form(i); - vscore = m_scores.find(e); -#if _PROBABILISTIC_UCT_ == 2 - double q = vscore.score * vscore.score + _UCT_EPS_; -#else - double q = vscore.score + _UCT_CONSTANT_ * sqrt(log(m_touched)/vscore.touched) + _UCT_EPS_; -#endif - if (m_mpz_manager.neq(get_value(g->form(i)), m_one)) { - sum_score += q; - if (rand() <= (q * RAND_MAX / sum_score) + 1) - pos = i; - } - } -#else - double max = -1.0; + value_score vscore; + double max = -1.0; for (unsigned i = 0; i < sz; i++) { - expr * e = g->form(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_ == 2 - double q = vscore.score + (_UCT_CONSTANT_ * (flip - vscore.touched)) / sz; -#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; } } -#endif - if (pos == static_cast(-1)) - return 0; + if (pos == static_cast(-1)) + return 0; -#if _UCT_ == 1 || _UCT_ == 3 - m_scores.find(g->form(pos)).touched++; - m_touched++; -#elif _UCT_ == 2 - m_scores.find(g->form(pos)).touched = flip; -#endif + m_scores.find(as[pos]).touched++; + m_touched++; // return m_list_false[pos]; - return g->form(pos); - -#elif _BFS_ == 3 - unsigned int pos = -1; - double max = -1.0; - for (unsigned i = 0; i < sz; i++) { - expr * e = g->form(i); - double q = get_score(e); - if (q > max && m_mpz_manager.neq(get_value(e), m_one) ) { max = q; pos = i; } - if (pos == static_cast(-1)) - return 0; - return g->form(pos); -#elif _BFS_ == 2 - unsigned int pos = -1; - double min = 2.0; - for (unsigned i = 0; i < sz; i++) { - expr * e = g->form(i); - double q = get_score(e); - if (q < min && m_mpz_manager.neq(get_value(e), m_one) ) { min = q; pos = i; } } - if (pos == static_cast(-1)) - return 0; - return g->form(pos); -#elif _BFS_ == 1 - unsigned int pos = flip % sz; - return get_unsat_assertion(g, sz, pos); -#elif _UNIFORM_RANDOM_ - 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)) pos = i; - if (pos == static_cast(-1)) - return 0; - return g->form(pos); -#elif _REAL_RS_ + 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]; +#if _REAL_RS_ //unsigned pos = m_false_list[get_random_uint(16) % m_cnt_false]; - //expr * e = get_unsat_assertion(g, sz, pos); //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]; -#elif _REAL_PBFS_ - //unsigned pos = m_false_list[flip % m_cnt_false]; - //expr * e = get_unsat_assertion(g, sz, pos); - //expr * e = m_unsat_expr[flip % m_unsat_expr.size()]; - sz = m_where_false.size(); - if (sz == 0) - return0; - else - return m_list_false[flip % sz]; -#else - unsigned int pos = get_random_uint(16) % sz; - return get_unsat_assertion(g, sz, pos); -#endif - return g->form(pos); -#elif _FOCUS_ == 2 -#if _BFS_ - unsigned int pos = flip % sz; -#else - unsigned int pos = get_random_uint(16) % sz; -#endif - return get_unsat_constants_crsat(g, sz, pos); #endif } - 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]; } };