diff --git a/src/tactic/sls/sls_compilation_settings.h b/src/tactic/sls/sls_compilation_settings.h new file mode 100644 index 000000000..aea4787b0 --- /dev/null +++ b/src/tactic/sls/sls_compilation_settings.h @@ -0,0 +1,158 @@ +/*++ +Copyright (c) 2014 Microsoft Corporation + +Module Name: + + sls_compilation_constants.h + +Abstract: + + Stochastic Local Search (SLS) compilation constants + +Author: + + Christoph (cwinter) 2014-03-19 + +Notes: + + This file should go away completely once we have evaluated all options. + +--*/ +// 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 + +// do we use restarts? +// 0 = no, 1 = use #moves, 2 = use #plateaus, 3 = use time +#define _RESTARTS_ 3 +// limit of moves/plateaus/seconds until first restart occurs +#define _RESTART_LIMIT_ 10 +// 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 +#define _RESTART_SCHEME_ 1 +// base value c for armin restart scheme using c^inner - only applies for _RESTART_SCHEME_ 3 +#define _RESTART_CONST_ARMIN_ 3.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 + +// 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.25 + +// 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 clause when randomizing in a plateau or use the current 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_ 10.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_ 1 + +// 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 + +// 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 \ No newline at end of file diff --git a/src/tactic/sls/sls_engine.cpp b/src/tactic/sls/sls_engine.cpp new file mode 100644 index 000000000..92471aad8 --- /dev/null +++ b/src/tactic/sls/sls_engine.cpp @@ -0,0 +1,1160 @@ +/*++ +Copyright (c) 2012 Microsoft Corporation + +Module Name: + + sls_engine.cpp + +Abstract: + + A Stochastic Local Search (SLS) engine + +Author: + + Christoph (cwinter) 2014-03-19 + +Notes: + +--*/ +#include + +#include"map.h" +#include"ast_smt2_pp.h" +#include"ast_pp.h" +#include"var_subst.h" +#include"model_pp.h" +#include"tactic.h" +#include"cooperate.h" +#include"luby.h" + +#include"sls_compilation_settings.h" +#include"sls_params.hpp" +#include"sls_engine.h" + + +sls_engine::sls_engine(ast_manager & m, params_ref const & p) : + m_manager(m), + m_powers(m_mpz_manager), + m_zero(m_mpz_manager.mk_z(0)), + m_one(m_mpz_manager.mk_z(1)), + m_two(m_mpz_manager.mk_z(2)), + m_cancel(false), + m_bv_util(m), + m_tracker(m, m_bv_util, m_mpz_manager, m_powers), + m_evaluator(m, m_bv_util, m_tracker, m_mpz_manager, m_powers) +{ + updt_params(p); +} + +sls_engine::~sls_engine() { + m_mpz_manager.del(m_zero); + m_mpz_manager.del(m_one); + 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_tracker.set_random_seed(p.random_seed()); + m_plateau_limit = p.plateau_limit(); +} + +void sls_engine::checkpoint() { + if (m_cancel) + throw tactic_exception(TACTIC_CANCELED_MSG); + cooperate("sls"); +} + +bool sls_engine::full_eval(goal_ref const & g, model & mdl) { + bool res = true; + + unsigned sz = g->size(); + for (unsigned i = 0; i < sz && res; i++) { + checkpoint(); + expr_ref o(m_manager); + + if (!mdl.eval(g->form(i), o, true)) + exit(ERR_INTERNAL_FATAL); + + res = m_manager.is_true(o.get()); + } + + TRACE("sls", tout << "Evaluation: " << res << std::endl;); + + 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 top_sum = 0.0; + unsigned sz = g->size(); + for (unsigned i = 0; i < sz; i++) { + expr * e = g->form(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 << " 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) { + m_evaluator.update_all(); + m_stats.m_full_evals++; + return top_score(g); +} + +double sls_engine::serious_score(goal_ref const & g, 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 +} + +double sls_engine::incremental_score(goal_ref const & g, 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 +} + +double sls_engine::incremental_score_prune(goal_ref const & g, func_decl * fd, const mpz & new_value) { +#if _EARLY_PRUNE_ + m_stats.m_incr_evals++; + if (m_evaluator.update_prune(fd, new_value)) +#if _CACHE_TOP_SCORE_ + return (m_tracker.get_top_sum() / g->size()); +#else + return top_score(g); +#endif + else + return 0.0; +#else + NOT_IMPLEMENTED_YET(); +#endif +} + +// checks whether the score outcome of a given move is better than the previous score +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) { + +#ifdef Z3DEBUG + mpz old_value; + m_mpz_manager.set(old_value, m_tracker.get_value(fd)); +#endif + +#if _EARLY_PRUNE_ + double r = incremental_score_prune(g, fd, temp); +#else + double r = incremental_score(g, fd, temp); +#endif +#ifdef Z3DEBUG + TRACE("sls_whatif", tout << "WHAT IF " << fd->get_name() << " WERE " << m_mpz_manager.to_string(temp) << + " --> " << r << std::endl;); + + m_mpz_manager.del(old_value); +#endif + + // if (r >= best_score) { + 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; +} + +void sls_engine::mk_add(unsigned bv_sz, const mpz & old_value, mpz & add_value, mpz & result) { + mpz temp, mask, mask2; + m_mpz_manager.add(old_value, add_value, 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); + +} + +// 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); + if (m_mpz_manager.is_power_of_two(incremented, shift) && shift == bv_sz) + m_mpz_manager.set(incremented, m_zero); +} + +void sls_engine::mk_dec(unsigned bv_sz, const mpz & old_value, mpz & decremented) { + if (m_mpz_manager.is_zero(old_value)) { + m_mpz_manager.set(decremented, m_powers(bv_sz)); + m_mpz_manager.dec(decremented); + } + else + m_mpz_manager.sub(old_value, m_one, decremented); +} + +void sls_engine::mk_inv(unsigned bv_sz, const mpz & old_value, mpz & inverted) { + m_mpz_manager.bitwise_not(bv_sz, old_value, inverted); +} + +void sls_engine::mk_flip(sort * s, const mpz & old_value, unsigned bit, mpz & flipped) { + m_mpz_manager.set(flipped, m_zero); + + if (m_bv_util.is_bv_sort(s)) { + mpz mask; + m_mpz_manager.set(mask, m_powers(bit)); + m_mpz_manager.bitwise_xor(old_value, mask, flipped); + m_mpz_manager.del(mask); + } + else if (m_manager.is_bool(s)) + m_mpz_manager.set(flipped, (m_mpz_manager.is_zero(old_value)) ? m_one : m_zero); + else + NOT_IMPLEMENTED_YET(); +} + +void sls_engine::mk_random_move(ptr_vector & unsat_constants) +{ + unsigned rnd_mv = 0; + unsigned ucc = unsat_constants.size(); + unsigned rc = (m_tracker.get_random_uint((ucc < 16) ? 4 : (ucc < 256) ? 8 : (ucc < 4096) ? 12 : (ucc < 65536) ? 16 : 32)) % ucc; + func_decl * fd = unsat_constants[rc]; + + mpz new_value; + + sort * srt = fd->get_range(); + if (m_manager.is_bool(srt)) + m_mpz_manager.set(new_value, (m_mpz_manager.is_zero(m_tracker.get_value(fd))) ? m_one : m_zero); + else + { +#if _USE_ADDSUB_ + if (m_mpz_manager.is_one(m_tracker.get_random_bool())) rnd_mv = 2; + if (m_mpz_manager.is_one(m_tracker.get_random_bool())) rnd_mv++; + move_type mt = (move_type)rnd_mv; + + // inversion doesn't make sense, let's do a flip instead. + if (mt == MV_INV) mt = MV_FLIP; +#else + mt = MV_FLIP; +#endif + unsigned bit = 0; + + switch (mt) + { + case MV_FLIP: { + unsigned bv_sz = m_bv_util.get_bv_size(srt); + bit = (m_tracker.get_random_uint((bv_sz < 16) ? 4 : (bv_sz < 256) ? 8 : (bv_sz < 4096) ? 12 : (bv_sz < 65536) ? 16 : 32)) % bv_sz; + mk_flip(fd->get_range(), m_tracker.get_value(fd), bit, new_value); + break; + } + case MV_INC: + mk_inc(m_bv_util.get_bv_size(fd->get_range()), m_tracker.get_value(fd), new_value); + break; + case MV_DEC: + mk_dec(m_bv_util.get_bv_size(fd->get_range()), m_tracker.get_value(fd), new_value); + break; + case MV_INV: + mk_inv(m_bv_util.get_bv_size(fd->get_range()), m_tracker.get_value(fd), new_value); + break; + default: + NOT_IMPLEMENTED_YET(); + } + + TRACE("sls", tout << "Randomization candidates: "; + for (unsigned i = 0; i < unsat_constants.size(); i++) + tout << unsat_constants[i]->get_name() << ", "; + tout << std::endl; + tout << "Random move: "; + switch (mt) { + case MV_FLIP: tout << "Flip #" << bit << " in " << fd->get_name() << std::endl; break; + case MV_INC: tout << "+1 for " << fd->get_name() << std::endl; break; + case MV_DEC: tout << "-1 for " << fd->get_name() << std::endl; break; + case MV_INV: tout << "NEG for " << fd->get_name() << std::endl; break; + } + tout << "Locally randomized model: " << std::endl; m_tracker.show_model(tout);); + } + + m_evaluator.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; +} + +// 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) { + mpz old_value, temp; +#if _USE_MUL3_ || _USE_UNARY_MINUS_ + mpz temp2; +#endif + unsigned bv_sz; + 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); + 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++) { +#endif + // What would happen if we flipped bit #i ? + 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; + } + } + + if (m_bv_util.is_bv_sort(srt) && bv_sz > 1) { +#if _USE_ADDSUB_ + 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; + } +#endif + // 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 _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); + // 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 + 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 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; + unsigned plateau_cnt = 0; + + score = rescore(g); + unsigned sz = g->size(); +#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 + checkpoint(); + m_stats.m_moves++; + +#if _REAL_RS_ || _REAL_PBFS_ + //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_walksat(e); +#else + ptr_vector & to_evaluate = m_tracker.get_unsat_constants_gsat(g, sz); + if (!to_evaluate.size()) + { + res = l_true; + goto bailout; + } +#endif + +#if _TYPE_RSTEP_ + if (m_tracker.get_random_uint(16) % 1000 < _PERM_RSTEP_) + { +#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 + } + 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; + +#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)) { + 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); + else +#endif +#if _REPICK_ + m_evaluator.randomize_local(g, m_stats.m_moves); +#else + m_evaluator.randomize_local(to_evaluate); +#endif +#endif + +#if _CACHE_TOP_SCORE_ + score = m_tracker.get_top_sum() / g->size(); +#else + score = top_score(g); +#endif + } + else { + func_decl * fd = to_evaluate[new_const]; +#if _REAL_RS_ || _REAL_PBFS_ + 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_ + 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;); + } + } + } + +bailout: + m_mpz_manager.del(new_value); + + return res; +} + +void sls_engine::operator()(goal_ref const & g, model_converter_ref & mc) { + if (g->inconsistent()) { + mc = 0; + return; + } + + 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() << "_VNS_ " << _VNS_ << 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() << "_PROBABILISTIC_UCT_ " << _PROBABILISTIC_UCT_ << std::endl; + verbose_stream() << "_UCT_EPS_ " << std::fixed << std::setprecision(4) << _UCT_EPS_ << std::endl; + 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; + + if (res == l_true) { + report_tactic_progress("Number of flips:", m_stats.m_moves); + for (unsigned i = 0; i < g->size(); i++) + if (!m_mpz_manager.is_one(m_tracker.get_value(g->form(i)))) + { + verbose_stream() << "Terminated before all assertions were SAT!" << std::endl; + NOT_IMPLEMENTED_YET(); + } + + if (m_produce_models) { + model_ref mdl = m_tracker.get_model(); + mc = model2model_converter(mdl.get()); + TRACE("sls_model", mc->display(tout);); + } + g->reset(); + } + else + mc = 0; +} + +unsigned sls_engine::check_restart(unsigned curr_value) +{ + if (curr_value > m_restart_limit) + { +#if _RESTART_SCHEME_ == 4 + m_restart_limit += (m_stats.m_restarts & (m_stats.m_restarts + 1)) ? _RESTART_LIMIT_ : (_RESTART_LIMIT_ * m_stats.m_restarts + 1); +#elif _RESTART_SCHEME_ == 3 + m_restart_limit += (unsigned)get_restart_armin(m_stats.m_restarts + 1) * _RESTART_LIMIT_; +#elif _RESTART_SCHEME_ == 2 + m_restart_limit += get_luby(m_stats.m_restarts + 1) * _RESTART_LIMIT_; +#elif _RESTART_SCHEME_ == 1 + if (m_stats.m_restarts & 1) + m_restart_limit += _RESTART_LIMIT_; + else + m_restart_limit += (2 << (m_stats.m_restarts >> 1)) * _RESTART_LIMIT_; +#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 + 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 new file mode 100644 index 000000000..878354c6d --- /dev/null +++ b/src/tactic/sls/sls_engine.h @@ -0,0 +1,159 @@ +/*++ +Copyright (c) 2014 Microsoft Corporation + +Module Name: + + sls_engine.h + +Abstract: + + A Stochastic Local Search (SLS) engine + +Author: + + Christoph (cwinter) 2014-03-19 + +Notes: + +--*/ +#ifndef _SLS_ENGINE_H_ +#define _SLS_ENGINE_H_ + +#include"stopwatch.h" +#include"lbool.h" +#include"model_converter.h" + +#include"sls_compilation_settings.h" +#include"sls_tracker.h" +#include"sls_evaluator.h" + +class sls_engine { +public: + class stats { + public: + unsigned m_restarts; + 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; + + 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), + m_invs(0) { + m_stopwatch.reset(); + m_stopwatch.start(); + } + void reset() { + m_full_evals = m_flips = m_incr_evals = 0; + m_stopwatch.reset(); + m_stopwatch.start(); + } + }; + +protected: + ast_manager & m_manager; + stats m_stats; + unsynch_mpz_manager m_mpz_manager; + powers m_powers; + mpz m_zero, m_one, m_two; + bool m_produce_models; + volatile bool m_cancel; + bv_util m_bv_util; + sls_tracker m_tracker; + sls_evaluator m_evaluator; + + unsigned m_restart_limit; + unsigned m_max_restarts; + unsigned m_plateau_limit; + + 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; + +public: + sls_engine(ast_manager & m, params_ref const & p); + ~sls_engine(); + + ast_manager & m() const { return m_manager; } + + void set_cancel(bool f) { m_cancel = f; } + void cancel() { set_cancel(true); } + void reset_cancel() { set_cancel(false); } + + void updt_params(params_ref const & _p); + + stats const & get_stats(void) { return m_stats; } + void reset_statistics(void) { m_stats.reset(); } + + bool full_eval(goal_ref const & g, 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); + + 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_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); + + 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, + double & best_score, unsigned & best_const, mpz & best_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 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); + + 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 unsigned check_restart(unsigned curr_value); +}; + +#endif \ No newline at end of file diff --git a/src/tactic/sls/sls_evaluator.h b/src/tactic/sls/sls_evaluator.h index 696d7664a..9daf93c32 100644 --- a/src/tactic/sls/sls_evaluator.h +++ b/src/tactic/sls/sls_evaluator.h @@ -20,6 +20,9 @@ Notes: #ifndef _SLS_EVALUATOR_H_ #define _SLS_EVALUATOR_H_ +#include"model_evaluator.h" + +#include"sls_compilation_settings.h" #include"sls_powers.h" #include"sls_tracker.h" diff --git a/src/tactic/sls/sls_tactic.cpp b/src/tactic/sls/sls_tactic.cpp index ada0ec359..0f157d3a6 100644 --- a/src/tactic/sls/sls_tactic.cpp +++ b/src/tactic/sls/sls_tactic.cpp @@ -16,1364 +16,31 @@ Author: Notes: --*/ -#include -#include"map.h" #include"nnf.h" -#include"cooperate.h" -#include"ast_smt2_pp.h" -#include"ast_pp.h" -#include"var_subst.h" -#include"model_pp.h" -#include"model_evaluator.h" #include"solve_eqs_tactic.h" -#include"elim_uncnstr_tactic.h" #include"bv_size_reduction_tactic.h" #include"max_bv_sharing_tactic.h" #include"simplify_tactic.h" -#include"stopwatch.h" #include"propagate_values_tactic.h" -#include"sls_tactic.h" +#include"ctx_simplify_tactic.h" +#include"elim_uncnstr_tactic.h" #include"nnf_tactic.h" -#include"luby.h" -#include "ctx_simplify_tactic.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 - -// do we use restarts? -// 0 = no, 1 = use #moves, 2 = use #plateaus, 3 = use time -#define _RESTARTS_ 3 -// limit of moves/plateaus/seconds until first restart occurs -#define _RESTART_LIMIT_ 10 -// 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 -#define _RESTART_SCHEME_ 1 -// base value c for armin restart scheme using c^inner - only applies for _RESTART_SCHEME_ 3 -#define _RESTART_CONST_ARMIN_ 3.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 - -// 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.25 - -// 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 clause when randomizing in a plateau or use the current 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_ 10.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_ 1 - -// 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 - -// 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 +#include"stopwatch.h" +#include"sls_tactic.h" #include"sls_params.hpp" -#include"sls_evaluator.h" -#include"sls_tracker.h" +#include"sls_engine.h" -class sls_tactic : public tactic { - class stats { - public: - unsigned m_restarts; - 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; - - 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), - m_invs(0) { - m_stopwatch.reset(); - m_stopwatch.start(); - } - void reset() { - m_full_evals = m_flips = m_incr_evals = 0; - m_stopwatch.reset(); - m_stopwatch.start(); - } - }; - - struct imp { - ast_manager & m_manager; - stats & m_stats; - unsynch_mpz_manager m_mpz_manager; - powers m_powers; - mpz m_zero, m_one, m_two; - bool m_produce_models; - volatile bool m_cancel; - bv_util m_bv_util; - sls_tracker m_tracker; - sls_evaluator m_evaluator; - - unsigned m_restart_limit; - unsigned m_max_restarts; - unsigned m_plateau_limit; - - 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; - - imp(ast_manager & m, params_ref const & p, stats & s) : - m_manager(m), - m_stats(s), - m_powers(m_mpz_manager), - m_zero(m_mpz_manager.mk_z(0)), - m_one(m_mpz_manager.mk_z(1)), - m_two(m_mpz_manager.mk_z(2)), - m_cancel(false), - m_bv_util(m), - m_tracker(m, m_bv_util, m_mpz_manager, m_powers), - m_evaluator(m, m_bv_util, m_tracker, m_mpz_manager, m_powers) - { - updt_params(p); - } - - ~imp() { - m_mpz_manager.del(m_zero); - m_mpz_manager.del(m_one); - m_mpz_manager.del(m_two); - } - - double 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(_RESTART_CONST_ARMIN_, inner_id + 1); - } - - inline unsigned check_restart(unsigned curr_value) - { - if (curr_value > m_restart_limit) - { -#if _RESTART_SCHEME_ == 4 - m_restart_limit += (m_stats.m_restarts & (m_stats.m_restarts + 1)) ? _RESTART_LIMIT_ : (_RESTART_LIMIT_ * m_stats.m_restarts + 1); -#elif _RESTART_SCHEME_ == 3 - m_restart_limit += (unsigned)get_restart_armin(m_stats.m_restarts + 1) * _RESTART_LIMIT_; -#elif _RESTART_SCHEME_ == 2 - m_restart_limit += get_luby(m_stats.m_restarts + 1) * _RESTART_LIMIT_; -#elif _RESTART_SCHEME_ == 1 - if (m_stats.m_restarts & 1) - m_restart_limit += _RESTART_LIMIT_; - else - m_restart_limit += (2 << (m_stats.m_restarts >> 1)) * _RESTART_LIMIT_; -#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 - return 0; - } - return 1; - } - - ast_manager & m() const { return m_manager; } - - void set_cancel(bool f) { m_cancel = f; } - void cancel() { set_cancel(true); } - void reset_cancel() { set_cancel(false); } - - static void collect_param_descrs(param_descrs & r) { - sls_params::collect_param_descrs(r); - } - - void updt_params(params_ref const & _p) { - sls_params p(_p); - m_produce_models = _p.get_bool("model", false); - m_max_restarts = p.restarts(); - m_tracker.set_random_seed(p.random_seed()); - m_plateau_limit = p.plateau_limit(); - } - - void checkpoint() { - if (m_cancel) - throw tactic_exception(TACTIC_CANCELED_MSG); - cooperate("sls"); - } - - bool full_eval(goal_ref const & g, model & mdl) { - bool res = true; - - unsigned sz = g->size(); - for (unsigned i = 0; i < sz && res; i++) { - checkpoint(); - expr_ref o(m_manager); - - if (!mdl.eval(g->form(i), o, true)) - exit(ERR_INTERNAL_FATAL); - - res = m_manager.is_true(o.get()); - } - - TRACE("sls", tout << "Evaluation: " << res << std::endl;); - - return res; - } - - double 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 top_sum = 0.0; - unsigned sz = g->size(); - for (unsigned i = 0; i < sz; i++) { - expr * e = g->form(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 << " 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 rescore(goal_ref const & g) { - m_evaluator.update_all(); - m_stats.m_full_evals++; - return top_score(g); - } - - double serious_score(goal_ref const & g, 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 - } - - double incremental_score(goal_ref const & g, 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 - } - -#if _EARLY_PRUNE_ - double incremental_score_prune(goal_ref const & g, 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; - } -#endif - - // checks whether the score outcome of a given move is better than the previous score - bool 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) { - - #ifdef Z3DEBUG - mpz old_value; - m_mpz_manager.set(old_value, m_tracker.get_value(fd)); - #endif - -#if _EARLY_PRUNE_ - double r = incremental_score_prune(g, fd, temp); -#else - double r = incremental_score(g, fd, temp); -#endif - #ifdef Z3DEBUG - TRACE("sls_whatif", tout << "WHAT IF " << fd->get_name() << " WERE " << m_mpz_manager.to_string(temp) << - " --> " << r << std::endl; ); - - m_mpz_manager.del(old_value); - #endif - -// if (r >= best_score) { - 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 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; - } - - void mk_add(unsigned bv_sz, const mpz & old_value, mpz & add_value, mpz & result) { - mpz temp, mask, mask2; - m_mpz_manager.add(old_value, add_value, 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); - - } - - // Andreas: do we really need all those temporary mpzs? - void 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 mk_div2(unsigned bv_sz, const mpz & old_value, mpz & result) { - m_mpz_manager.div(old_value, m_two, result); - } - - void mk_inc(unsigned bv_sz, const mpz & old_value, mpz & incremented) { - unsigned shift; - m_mpz_manager.add(old_value, m_one, incremented); - if (m_mpz_manager.is_power_of_two(incremented, shift) && shift == bv_sz) - m_mpz_manager.set(incremented, m_zero); - } - - void mk_dec(unsigned bv_sz, const mpz & old_value, mpz & decremented) { - if (m_mpz_manager.is_zero(old_value)) { - m_mpz_manager.set(decremented, m_powers(bv_sz)); - m_mpz_manager.dec(decremented); - } - else - m_mpz_manager.sub(old_value, m_one, decremented); - } - - void mk_inv(unsigned bv_sz, const mpz & old_value, mpz & inverted) { - m_mpz_manager.bitwise_not(bv_sz, old_value, inverted); - } - - void mk_flip(sort * s, const mpz & old_value, unsigned bit, mpz & flipped) { - m_mpz_manager.set(flipped, m_zero); - - if (m_bv_util.is_bv_sort(s)) { - mpz mask; - m_mpz_manager.set(mask, m_powers(bit)); - m_mpz_manager.bitwise_xor(old_value, mask, flipped); - m_mpz_manager.del(mask); - } - else if (m_manager.is_bool(s)) - m_mpz_manager.set(flipped, (m_mpz_manager.is_zero(old_value)) ? m_one : m_zero); - else - NOT_IMPLEMENTED_YET(); - } - - void mk_random_move(ptr_vector & unsat_constants) - { - unsigned rnd_mv = 0; - - unsigned ucc = unsat_constants.size(); - unsigned rc = (m_tracker.get_random_uint((ucc < 16) ? 4 : (ucc < 256) ? 8 : (ucc < 4096) ? 12 : (ucc < 65536) ? 16 : 32)) % ucc; - func_decl * fd = unsat_constants[rc]; - - mpz new_value; - - sort * srt = fd->get_range(); - if (m_manager.is_bool(srt)) - m_mpz_manager.set(new_value, (m_mpz_manager.is_zero(m_tracker.get_value(fd))) ? m_one : m_zero); - else - { -#if _USE_ADDSUB_ - if (m_mpz_manager.is_one(m_tracker.get_random_bool())) rnd_mv=2; - if (m_mpz_manager.is_one(m_tracker.get_random_bool())) rnd_mv++; - move_type mt = (move_type) rnd_mv; - - // inversion doesn't make sense, let's do a flip instead. - if (mt == MV_INV) mt = MV_FLIP; -#else - mt = MV_FLIP; -#endif - unsigned bit = 0; - - switch (mt) - { - case MV_FLIP: { - unsigned bv_sz = m_bv_util.get_bv_size(srt); - bit = (m_tracker.get_random_uint((bv_sz < 16) ? 4 : (bv_sz < 256) ? 8 : (bv_sz < 4096) ? 12 : (bv_sz < 65536) ? 16 : 32)) % bv_sz; - mk_flip(fd->get_range(), m_tracker.get_value(fd), bit, new_value); - break; - } - case MV_INC: - mk_inc(m_bv_util.get_bv_size(fd->get_range()), m_tracker.get_value(fd), new_value); - break; - case MV_DEC: - mk_dec(m_bv_util.get_bv_size(fd->get_range()), m_tracker.get_value(fd), new_value); - break; - case MV_INV: - mk_inv(m_bv_util.get_bv_size(fd->get_range()), m_tracker.get_value(fd), new_value); - break; - default: - NOT_IMPLEMENTED_YET(); - } - - TRACE("sls", tout << "Randomization candidates: "; - for (unsigned i = 0; i < unsat_constants.size(); i++) - tout << unsat_constants[i]->get_name() << ", "; - tout << std::endl; - tout << "Random move: "; - switch (mt) { - case MV_FLIP: tout << "Flip #" << bit << " in " << fd->get_name() << std::endl; break; - case MV_INC: tout << "+1 for " << fd->get_name() << std::endl; break; - case MV_DEC: tout << "-1 for " << fd->get_name() << std::endl; break; - case MV_INV: tout << "NEG for " << fd->get_name() << std::endl; break; - } - tout << "Locally randomized model: " << std::endl; m_tracker.show_model(tout); ); - } - - m_evaluator.update(fd, new_value); - m_mpz_manager.del(new_value); - } - - void 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 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; - } - - // finds the move that increased score the most. returns best_const = -1, if no increasing move exists. - 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) { - mpz old_value, temp; -#if _USE_MUL3_ || _USE_UNARY_MINUS_ - mpz temp2; -#endif - unsigned bv_sz; - 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); - 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++) { -#endif - // What would happen if we flipped bit #i ? - 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; - } - } - - if (m_bv_util.is_bv_sort(srt) && bv_sz > 1) { -#if _USE_ADDSUB_ - 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; - } -#endif - // 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 _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); - // 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 - return new_score; - } - - // same as find_best_move but only considers the score of the current expression instead of the overall score - double 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 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 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 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 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 search(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; - unsigned plateau_cnt = 0; - - score = rescore(g); - unsigned sz = g->size(); -#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 - checkpoint(); - m_stats.m_moves++; - -#if _REAL_RS_ || _REAL_PBFS_ - //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_walksat(e); -#else - ptr_vector & to_evaluate = m_tracker.get_unsat_constants_gsat(g, sz); - if (!to_evaluate.size()) - { - res = l_true; - goto bailout; - } -#endif - -#if _TYPE_RSTEP_ - if (m_tracker.get_random_uint(16) % 1000 < _PERM_RSTEP_) - { -#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 - } - 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; - -#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)) { - 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); - else -#endif -#if _REPICK_ - m_evaluator.randomize_local(g, m_stats.m_moves); -#else - m_evaluator.randomize_local(to_evaluate); -#endif -#endif - -#if _CACHE_TOP_SCORE_ - score = m_tracker.get_top_sum() / g->size(); -#else - score = top_score(g); -#endif - } else { - func_decl * fd = to_evaluate[new_const]; -#if _REAL_RS_ || _REAL_PBFS_ - 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 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_ - 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;); - } - } - } - - bailout: - m_mpz_manager.del(new_value); - - return res; - } - - void operator()(goal_ref const & g, model_converter_ref & mc) { - if (g->inconsistent()) { - mc = 0; - return; - } - - 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() << "_VNS_ " << _VNS_ << 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() << "_PROBABILISTIC_UCT_ " << _PROBABILISTIC_UCT_ << std::endl; - verbose_stream() << "_UCT_EPS_ " << std::fixed << std::setprecision(4) << _UCT_EPS_ << std::endl; - 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; - - if (res == l_true) { - report_tactic_progress("Number of flips:", m_stats.m_moves); - for (unsigned i = 0; i < g->size(); i++) - if (!m_mpz_manager.is_one(m_tracker.get_value(g->form(i)))) - { - verbose_stream() << "Terminated before all assertions were SAT!" << std::endl; - NOT_IMPLEMENTED_YET(); - } - - if (m_produce_models) { - model_ref mdl = m_tracker.get_model(); - mc = model2model_converter(mdl.get()); - TRACE("sls_model", mc->display(tout); ); - } - g->reset(); - } - else - mc = 0; - } - }; - +class sls_tactic : public tactic { ast_manager & m; params_ref m_params; - imp * m_imp; - stats m_stats; + sls_engine * m_engine; public: sls_tactic(ast_manager & _m, params_ref const & p): m(_m), m_params(p) { - m_imp = alloc(imp, m, p, m_stats); + m_engine = alloc(sls_engine, m, p); } virtual tactic * translate(ast_manager & m) { @@ -1381,16 +48,16 @@ public: } virtual ~sls_tactic() { - dealloc(m_imp); + dealloc(m_engine); } virtual void updt_params(params_ref const & p) { m_params = p; - m_imp->updt_params(p); + m_engine->updt_params(p); } virtual void collect_param_descrs(param_descrs & r) { - imp::collect_param_descrs(r); + sls_params::collect_param_descrs(r); } virtual void operator()(goal_ref const & g, @@ -1398,14 +65,13 @@ public: model_converter_ref & mc, proof_converter_ref & pc, expr_dependency_ref & core) { - SASSERT(g->is_well_sorted()); - m_imp->m_produce_models = g->models_enabled(); + SASSERT(g->is_well_sorted()); mc = 0; pc = 0; core = 0; result.reset(); TRACE("sls", g->display(tout);); tactic_report report("sls", *g); - m_imp->operator()(g, mc); + m_engine->operator()(g, mc); g->inc_depth(); result.push_back(g.get()); @@ -1414,40 +80,41 @@ public: } virtual void cleanup() { - imp * d = m_imp; + sls_engine * d = m_engine; #pragma omp critical (tactic_cancel) { - d = m_imp; + d = m_engine; } dealloc(d); - d = alloc(imp, m, m_params, m_stats); + d = alloc(sls_engine, m, m_params); #pragma omp critical (tactic_cancel) { - m_imp = d; + m_engine = d; } } virtual void collect_statistics(statistics & st) const { - double seconds = m_stats.m_stopwatch.get_current_seconds(); - st.update("sls restarts", m_stats.m_restarts); - st.update("sls full evals", m_stats.m_full_evals); - st.update("sls incr evals", m_stats.m_incr_evals); - st.update("sls incr evals/sec", m_stats.m_incr_evals/ seconds); - st.update("sls FLIP moves", m_stats.m_flips); - st.update("sls INC moves", m_stats.m_incs); - st.update("sls DEC moves", m_stats.m_decs); - st.update("sls INV moves", m_stats.m_invs); - st.update("sls moves", m_stats.m_moves); - st.update("sls moves/sec", m_stats.m_moves / seconds); + sls_engine::stats const & stats = m_engine->get_stats(); + double seconds = stats.m_stopwatch.get_current_seconds(); + st.update("sls restarts", stats.m_restarts); + st.update("sls full evals", stats.m_full_evals); + st.update("sls incr evals", stats.m_incr_evals); + st.update("sls incr evals/sec", stats.m_incr_evals / seconds); + st.update("sls FLIP moves", stats.m_flips); + st.update("sls INC moves", stats.m_incs); + st.update("sls DEC moves", stats.m_decs); + st.update("sls INV moves", stats.m_invs); + st.update("sls moves", stats.m_moves); + st.update("sls moves/sec", stats.m_moves / seconds); } virtual void reset_statistics() { - m_stats.reset(); + m_engine->reset_statistics(); } virtual void set_cancel(bool f) { - if (m_imp) - m_imp->set_cancel(f); + if (m_engine) + m_engine->set_cancel(f); } }; diff --git a/src/tactic/sls/sls_tracker.h b/src/tactic/sls/sls_tracker.h index 0aca1f59c..3675265ee 100644 --- a/src/tactic/sls/sls_tracker.h +++ b/src/tactic/sls/sls_tracker.h @@ -20,6 +20,12 @@ Notes: #ifndef _SLS_TRACKER_H_ #define _SLS_TRACKER_H_ +#include"goal.h" +#include"model.h" + +#include"sls_compilation_settings.h" +#include"sls_powers.h" + class sls_tracker { ast_manager & m_manager; unsynch_mpz_manager & m_mpz_manager; @@ -1186,7 +1192,7 @@ public: // expr * e = m_list_false[i]; vscore = m_scores.find(e); #if _UCT_ == 1 - double q = vscore.score + _UCT_CONSTANT_ * sqrt(log(m_touched)/vscore.touched); + 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; #endif @@ -1334,7 +1340,7 @@ public: // expr * e = m_list_false[i]; vscore = m_scores.find(e); #if _UCT_ == 1 - double q = vscore.score + _UCT_CONSTANT_ * sqrt(log(m_touched)/vscore.touched); + 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; #endif