From ef1d8f2acc9aca562a83e55f89e8820b48c525d5 Mon Sep 17 00:00:00 2001 From: Andreas Froehlich Date: Sun, 20 Apr 2014 16:38:49 +0100 Subject: [PATCH 1/7] Current version before integration ... --- src/tactic/sls/sls_compilation_settings.h | 36 +- src/tactic/sls/sls_engine.cpp | 348 ++++++++++++++++++-- src/tactic/sls/sls_engine.h | 12 +- src/tactic/sls/sls_evaluator.h | 146 ++++++++- src/tactic/sls/sls_tactic.cpp | 4 +- src/tactic/sls/sls_tracker.h | 379 +++++++++++++++++++++- src/tactic/smtlogics/qfbv_tactic.cpp | 28 ++ 7 files changed, 885 insertions(+), 68 deletions(-) diff --git a/src/tactic/sls/sls_compilation_settings.h b/src/tactic/sls/sls_compilation_settings.h index 4d8c83599..d2b899dd8 100644 --- a/src/tactic/sls/sls_compilation_settings.h +++ b/src/tactic/sls/sls_compilation_settings.h @@ -36,17 +36,21 @@ Notes: // 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_ 3 +#define _RESTARTS_ 1 // limit of moves/plateaus/seconds until first restart occurs -#define _RESTART_LIMIT_ 10 +#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_ 3.0 +#define _RESTART_CONST_ARMIN_ 2.0 // timelimit #define _TIMELIMIT_ 3600 @@ -61,6 +65,21 @@ Notes: // 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 @@ -70,7 +89,7 @@ Notes: #define _WEIGHT_DIST_ 1 // the factor used for _WEIGHT_DIST_ = 1 -#define _WEIGHT_DIST_FACTOR_ 0.25 +#define _WEIGHT_DIST_FACTOR_ 0.5 // shall we toggle the weight after each restart? #define _WEIGHT_TOGGLE_ 0 @@ -82,14 +101,15 @@ Notes: // 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? +// 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_ 10.0 +#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 @@ -103,11 +123,11 @@ Notes: // how shall we initialize the _UCT_ total touched counter? // 0 = initialize with one, 1 = initialize with number of assertions -#define _UCT_INIT_ 1 +#define _UCT_INIT_ 0 // do we gradually reduce the touched values of _UCT_? #define _UCT_FORGET_ 0 -#define _UCT_FORGET_FACTOR_ 0.5 +#define _UCT_FORGET_FACTOR_ 0.9 // shall we use addition/subtraction? #define _USE_ADDSUB_ 1 diff --git a/src/tactic/sls/sls_engine.cpp b/src/tactic/sls/sls_engine.cpp index 92471aad8..342e649af 100644 --- a/src/tactic/sls/sls_engine.cpp +++ b/src/tactic/sls/sls_engine.cpp @@ -169,6 +169,14 @@ double sls_engine::incremental_score_prune(goal_ref const & g, func_decl * fd, c #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()); + 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) { @@ -190,8 +198,33 @@ 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) { + //if (r >= best_score) { if (r > best_score) { + m_tracker.reset_equal_scores(); + best_score = r; + best_const = fd_inx; + 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); @@ -426,39 +459,25 @@ double sls_engine::find_best_move_vns(goal_ref const & g, ptr_vector 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_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; -#if _USE_MUL3_ || _USE_UNARY_MINUS_ - mpz temp2; -#endif - unsigned bv_sz; + unsigned bv_sz, max_bv_sz = 0; 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(); 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)); - // 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_ + // 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); @@ -471,9 +490,121 @@ double sls_engine::find_best_move(goal_ref const & g, ptr_vector & to 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) { + 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)) { + 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 (m_tracker.get_random_uint(1)) + 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 (m_tracker.get_random_uint(1)) + 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 (m_tracker.get_random_uint(1)) if (what_if(g, fd, i, temp, new_score, best_const, best_value)) move = MV_INV; @@ -514,6 +645,50 @@ double sls_engine::find_best_move(goal_ref const & g, ptr_vector & to #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, + 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(); + 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)); + + 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++) + { + 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); + } + } + } + + // reset to what it was before + double check = incremental_score(g, fd, old_value); + } + + m_mpz_manager.del(old_value); + m_mpz_manager.del(temp); + m_mpz_manager.del(temp2); + return new_score; } @@ -725,6 +900,13 @@ lbool sls_engine::search(goal_ref const & g) { 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 @@ -738,9 +920,18 @@ lbool sls_engine::search(goal_ref const & g) { #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);} + checkpoint(); m_stats.m_moves++; +#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_ //m_tracker.debug_real(g, m_stats.m_moves); #endif @@ -757,6 +948,7 @@ lbool sls_engine::search(goal_ref const & g) { 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); @@ -789,6 +981,8 @@ lbool sls_engine::search(goal_ref const & g) { #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); @@ -796,6 +990,60 @@ lbool sls_engine::search(goal_ref const & g) { score = find_best_move(g, to_evaluate, score, new_const, new_value, new_bit, move); #endif +#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); + } + } +#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++; @@ -810,10 +1058,19 @@ lbool sls_engine::search(goal_ref const & g) { mk_random_move(to_evaluate); else #endif -#if _REPICK_ +#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(to_evaluate); + m_evaluator.randomize_local_n(g, to_evaluate); + //m_evaluator.randomize_local(to_evaluate); #endif #endif @@ -822,10 +1079,28 @@ lbool sls_engine::search(goal_ref const & g) { #else score = top_score(g); #endif + +#if _PAWS_ + for (unsigned i = 0; i < sz; i++) + { + expr * q = g->form(i); + if (m_tracker.get_random_uint(16) % 100 < _PAWS_) + { + 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_ +#if _REAL_RS_ || _REAL_PBFS_ || _PAWS_ score = serious_score(g, fd, new_value); #else score = incremental_score(g, fd, new_value); @@ -961,7 +1236,7 @@ lbool sls_engine::search_old(goal_ref const & g) { case MV_DIV2: m_stats.m_div2s++; break; } -#if _REAL_RS_ || _REAL_PBFS_ +#if _REAL_RS_ || _REAL_PBFS_ || _PAWS_ score = serious_score(g, fd, new_value); #else score = incremental_score(g, fd, new_value); @@ -1056,7 +1331,14 @@ void sls_engine::operator()(goal_ref const & g, model_converter_ref & mc) { 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; @@ -1067,6 +1349,8 @@ void sls_engine::operator()(goal_ref const & g, model_converter_ref & mc) { 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; verbose_stream() << "_USE_ADDSUB_ " << _USE_ADDSUB_ << std::endl; @@ -1136,7 +1420,9 @@ unsigned sls_engine::check_restart(unsigned curr_value) { if (curr_value > m_restart_limit) { -#if _RESTART_SCHEME_ == 4 +#if _RESTART_SCHEME_ == 5 + m_restart_limit += (unsigned)(_RESTART_LIMIT_ * 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); #elif _RESTART_SCHEME_ == 3 m_restart_limit += (unsigned)get_restart_armin(m_stats.m_restarts + 1) * _RESTART_LIMIT_; @@ -1144,9 +1430,11 @@ unsigned sls_engine::check_restart(unsigned curr_value) m_restart_limit += get_luby(m_stats.m_restarts + 1) * _RESTART_LIMIT_; #elif _RESTART_SCHEME_ == 1 if (m_stats.m_restarts & 1) + //if (m_stats.m_restarts % 3 == 2) m_restart_limit += _RESTART_LIMIT_; else m_restart_limit += (2 << (m_stats.m_restarts >> 1)) * _RESTART_LIMIT_; + //m_restart_limit += (2 << (m_stats.m_restarts / 3)) * _RESTART_LIMIT_; #else m_restart_limit += _RESTART_LIMIT_; #endif diff --git a/src/tactic/sls/sls_engine.h b/src/tactic/sls/sls_engine.h index 878354c6d..902c6b7a0 100644 --- a/src/tactic/sls/sls_engine.h +++ b/src/tactic/sls/sls_engine.h @@ -108,7 +108,13 @@ public: 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); @@ -132,6 +138,10 @@ protected: 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_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); + 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); diff --git a/src/tactic/sls/sls_evaluator.h b/src/tactic/sls/sls_evaluator.h index 8d2a7ba1d..78f2cb79a 100644 --- a/src/tactic/sls/sls_evaluator.h +++ b/src/tactic/sls/sls_evaluator.h @@ -575,7 +575,7 @@ public: #if _CACHE_TOP_SCORE_ //if (!m_tracker.has_uplinks(cur)) if (m_tracker.is_top_expr(cur)) - m_tracker.adapt_top_sum(new_score, m_tracker.get_score(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); @@ -584,12 +584,13 @@ public: new_score = m_tracker.score(cur); //if (!m_tracker.has_uplinks(cur)) if (m_tracker.is_top_expr(cur)) - m_tracker.adapt_top_sum(new_score, m_tracker.get_score(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); for (unsigned j = 0; j < ups.size(); j++) { @@ -634,7 +635,7 @@ public: #if _CACHE_TOP_SCORE_ //if (!m_tracker.has_uplinks(cur)) if (m_tracker.is_top_expr(cur)) - m_tracker.adapt_top_sum(new_score, m_tracker.get_score(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); @@ -643,7 +644,7 @@ public: new_score = m_tracker.score(cur); //if (!m_tracker.has_uplinks(cur)) if (m_tracker.is_top_expr(cur)) - m_tracker.adapt_top_sum(new_score, m_tracker.get_score(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)); @@ -683,7 +684,7 @@ public: m_traversal_stack[cur_depth].push_back(ep); if (cur_depth > max_depth) max_depth = cur_depth; } -#if _REAL_RS_ || _REAL_PBFS_ +#if _REAL_RS_ || _REAL_PBFS_ || _PAWS_ run_serious_update(max_depth); #else run_update(max_depth); @@ -729,14 +730,16 @@ public: #if _CACHE_TOP_SCORE_ //if (!m_tracker.has_uplinks(cur)) if (m_tracker.is_top_expr(cur)) - m_tracker.adapt_top_sum(new_score, m_tracker.get_score(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)) { @@ -771,7 +774,7 @@ public: new_score = m_tracker.score(cur); //if (!m_tracker.has_uplinks(cur)) if (m_tracker.is_top_expr(cur)) - m_tracker.adapt_top_sum(new_score, m_tracker.get_score(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)); @@ -858,6 +861,104 @@ public: } #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: @@ -901,7 +1002,7 @@ public: mpz temp = m_tracker.get_random(fd->get_range()); #endif -#if _REAL_RS_ || _REAL_PBFS_ +#if _REAL_RS_ || _REAL_PBFS_ || _PAWS_ serious_update(fd, temp); #else update(fd, temp); @@ -922,9 +1023,36 @@ public: randomize_local(m_tracker.get_constants(e)); } - void randomize_local(goal_ref const & g, unsigned int flip) { + void randomize_local(goal_ref const & g, unsigned int flip) { randomize_local(m_tracker.get_unsat_constants(g, flip)); } + + 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 a9b110224..7a9252fe2 100644 --- a/src/tactic/sls/sls_tactic.cpp +++ b/src/tactic/sls/sls_tactic.cpp @@ -161,14 +161,14 @@ tactic * mk_preamble(ast_manager & m, params_ref const & 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 ... + // Andreas: This one at least eliminates top level duplicates ... but has very bad effects on performance! //mk_simplify_tactic(m), - // Andreas: How does a NNF actually look like? Can it contain ITE operators? 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)); t->updt_params(p); return t; } diff --git a/src/tactic/sls/sls_tracker.h b/src/tactic/sls/sls_tracker.h index 6ac054246..87c90f1f8 100644 --- a/src/tactic/sls/sls_tracker.h +++ b/src/tactic/sls/sls_tracker.h @@ -86,12 +86,17 @@ private: 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: sls_tracker(ast_manager & m, bv_util & bvu, unsynch_mpz_manager & mm, powers & p) : @@ -111,15 +116,52 @@ public: m_mpz_manager.del(m_two); } + unsigned get_formula_size() { + return m_scores.size(); + } + + double get_avg_bw(goal_ref const & g) { + double sum = 0.0; + unsigned count = 0; + + for (unsigned i = 0; i < g->size(); i++) + { + m_temp_constants.reset(); + ptr_vector const & this_decls = m_constants_occ.find(g->form(i)); + unsigned sz = this_decls.size(); + for (unsigned i = 0; i < sz; i++) { + func_decl * fd = this_decls[i]; + m_temp_constants.push_back(fd); + sort * srt = fd->get_range(); + sum += (m_manager.is_bool(srt)) ? 1 : m_bv_util.get_bv_size(srt); + count++; + } + } + + 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; + } + + unsigned inc_equal_scores() { + return ++m_equal_scores; + } + #if _CACHE_TOP_SCORE_ - inline void adapt_top_sum(double add, double sub) { + 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) { @@ -276,6 +318,7 @@ public: } #endif +#if _UCT_ void uct_forget(goal_ref const & g) { expr * e; unsigned touched_old, touched_new; @@ -289,6 +332,7 @@ public: m_touched += touched_new - touched_old; } } +#endif void initialize(app * n) { // Build score table @@ -463,6 +507,15 @@ public: //} #endif +#if _PAWS_ + for (unsigned i = 0; i < sz; i++) + { + expr * e = g->form(i); + if (!m_weights.contains(e)) + m_weights.insert(e, _PAWS_INIT_); + } +#endif + #if _EARLY_PRUNE_ for (unsigned i = 0; i < sz; i++) setup_occs(g->form(i)); @@ -473,6 +526,30 @@ public: #endif } +#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)); + } + + unsigned get_weight(expr * e) + //double get_weight(expr * e) + { + return m_weights.find(e); + } +#endif + #if _REAL_RS_ || _REAL_PBFS_ void make_assertion(expr * e) { @@ -763,6 +840,7 @@ public: const mpz & v1 = get_value(arg1); if (negated) { + //res = (m_mpz_manager.eq(v0, v1)) ? 0.5 * (m_bv_util.get_bv_size(arg0) - 1.0) / m_bv_util.get_bv_size(arg0) : 1.0; res = (m_mpz_manager.eq(v0, v1)) ? 0.0 : 1.0; TRACE("sls_score", tout << "V0 = " << m_mpz_manager.to_string(v0) << " ; V1 = " << m_mpz_manager.to_string(v1) << std::endl; ); @@ -809,40 +887,209 @@ public: SASSERT(a->get_num_args() == 2); const mpz & x = get_value(a->get_arg(0)); const mpz & y = get_value(a->get_arg(1)); - unsigned bv_sz = m_bv_util.get_bv_size(a->get_decl()->get_domain()[0]); + int bv_sz = m_bv_util.get_bv_size(a->get_decl()->get_domain()[0]); 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(); + // 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; + 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 - res = (dbl > 1.0) ? 0.0 : (dbl < 0.0) ? 1.0 : 1.0 - dbl; m_mpz_manager.del(diff); - } - } - else { - if (m_mpz_manager.le(x, y)) + 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 = n.get_double(); + double dbl = 1.0 - n.get_double(); res = (dbl > 1.0) ? 1.0 : (dbl < 0.0) ? 0.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 +/* 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 app * a = to_app(n); SASSERT(a->get_num_args() == 2); mpz x; m_mpz_manager.set(x, get_value(a->get_arg(0))); @@ -855,31 +1102,61 @@ public: if (negated) { if (x > y) - res = 1.0; + { + /*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 = n.get_double(); - res = (dbl > 1.0) ? 0.0 : (dbl < 0.0) ? 1.0 : 1.0 - dbl; + 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; 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) - res = 1.0; + { + /*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 = n.get_double(); + double dbl = 1.0 - n.get_double(); res = (dbl > 1.0) ? 1.0 : (dbl < 0.0) ? 0.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; ); @@ -1149,12 +1426,58 @@ public: 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)) + { + m_temp_constants.reset(); return m_temp_constants; + } else return get_constants(); } @@ -1303,12 +1626,15 @@ public: } } - expr * get_unsat_assertion(goal_ref const & g, unsigned int flip) { unsigned sz = g->size(); - if (sz == 1) - return g->form(0); + if (sz == 1) { + if (m_mpz_manager.eq(get_value(g->form(0)), m_zero)) + return g->form(0); + else + return 0; + } m_temp_constants.reset(); #if _FOCUS_ == 1 @@ -1357,7 +1683,7 @@ public: // 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); + 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 @@ -1440,6 +1766,23 @@ public: return get_unsat_constants_crsat(g, sz, pos); #endif } + + expr * get_new_unsat_assertion(goal_ref const & g, expr * e) { + unsigned sz = g->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 (pos == static_cast(-1)) + return 0; + return g->form(pos); + } }; #endif \ No newline at end of file diff --git a/src/tactic/smtlogics/qfbv_tactic.cpp b/src/tactic/smtlogics/qfbv_tactic.cpp index ac53ca0c8..a7870176d 100644 --- a/src/tactic/smtlogics/qfbv_tactic.cpp +++ b/src/tactic/smtlogics/qfbv_tactic.cpp @@ -28,6 +28,8 @@ Notes: #include"bv_size_reduction_tactic.h" #include"aig_tactic.h" #include"sat_tactic.h" +//#include"nnf_tactic.h" +//#include"sls_tactic.h" #define MEMLIMIT 300 @@ -93,6 +95,32 @@ tactic * mk_qfbv_tactic(ast_manager & m, params_ref const & p) { mk_sat_tactic(m)); #endif + /* use full sls + tactic * st = using_params(and_then(preamble_st, + cond(mk_is_qfbv_probe(), + cond(mk_is_qfbv_eq_probe(), + and_then(mk_bv1_blaster_tactic(m), + using_params(mk_smt_tactic(), solver_p)), + and_then(mk_nnf_tactic(m, p), mk_sls_tactic(m))), + mk_smt_tactic())), + main_p);*/ + + /* use pure dpll + tactic * st = using_params(and_then(mk_simplify_tactic(m), + cond(mk_is_qfbv_probe(), + and_then(mk_bit_blaster_tactic(m), + when(mk_lt(mk_memory_probe(), mk_const_probe(MEMLIMIT)), + and_then(using_params(and_then(mk_simplify_tactic(m), + mk_solve_eqs_tactic(m)), + local_ctx_p), + if_no_proofs(cond(mk_produce_unsat_cores_probe(), + mk_aig_tactic(), + using_params(mk_aig_tactic(), + big_aig_p))))), + new_sat), + mk_smt_tactic())), + main_p);*/ + tactic * st = using_params(and_then(preamble_st, // If the user sets HI_DIV0=false, then the formula may contain uninterpreted function // symbols. In this case, we should not use From c1741d794155eea8041ef78075aff29b6bbce900 Mon Sep 17 00:00:00 2001 From: Andreas Froehlich Date: Tue, 22 Apr 2014 00:32:45 +0100 Subject: [PATCH 2/7] Almost cleaned up version. --- src/tactic/sls/sls_compilation_settings.h | 72 +------ src/tactic/sls/sls_engine.cpp | 231 +++++++--------------- src/tactic/sls/sls_engine.h | 13 +- src/tactic/sls/sls_evaluator.h | 175 ++-------------- src/tactic/sls/sls_tactic.cpp | 6 +- src/tactic/sls/sls_tracker.h | 170 ++++++++-------- 6 files changed, 177 insertions(+), 490 deletions(-) diff --git a/src/tactic/sls/sls_compilation_settings.h b/src/tactic/sls/sls_compilation_settings.h index 73ba1ffab..9add78daa 100644 --- a/src/tactic/sls/sls_compilation_settings.h +++ b/src/tactic/sls/sls_compilation_settings.h @@ -22,83 +22,13 @@ Notes: #ifndef _SLS_COMPILATION_SETTINGS_H_ #define _SLS_COMPILATION_SETTINGS_H_ -// how many terms are considered for variable selection? -// 0 = all terms (GSAT), 1 = only one top level assertion (WSAT) -#define _FOCUS_ 1 - -// shall we use additive weighting scheme? -#define _PAWS_ 5 -#define _PAWS_INIT_ 40 - -// do we use restarts? -// 0 = no, 1 = use #moves, 2 = use #plateaus, 3 = use time -#define _RESTARTS_ 1 -// limit of moves/plateaus/seconds until first restart occurs -#define _RESTART_LIMIT_ 100 -//// 0 = initialize with all zero, 1 initialize with random value -#define _RESTART_INIT_ 0 -// 0 = even intervals, 1 = pseudo luby, 2 = real luby, 3 = armin, 4 = rapid, 5 = minisat -#define _RESTART_SCHEME_ 1 -// base value c for armin restart scheme using c^inner - only applies for _RESTART_SCHEME_ 3 -#define _RESTART_CONST_ARMIN_ 2.0 - -// timelimit -#define _TIMELIMIT_ 3600 - -// should score of conjunctions be calculated by average rather than max? -#define _SCORE_AND_AVG_ 0 - -// shall we check 2-bit flips in plateaus using Monte Carlo? -#define _VNS_MC_ 0 - -// how many 2-bit flips shall we try per bit? -#define _VNS_MC_TRIES_ 1 - -// shall we check another assertion if no improving step was found in the first one? -#define _VNS_REPICK_ 0 - -// do we reduce the score of unsatisfied literals? -// 0 = no, 1 = yes, by multiplying it with some factor -#define _WEIGHT_DIST_ 1 - -// the factor used for _WEIGHT_DIST_ = 1 -#define _WEIGHT_DIST_FACTOR_ 0.5 - -// shall we repick assertion when randomizing in a plateau or use the current one? -// 0 = use old one, 1 = repick according to usual scheme, 2 = repick randomly and force different one -#define _REPICK_ 1 - -// do we use some UCT-like scheme for assertion-selection? overrides _BFS_ -#define _UCT_ 1 - -// how much diversification is used in the UCT-scheme? -#define _UCT_CONSTANT_ 20.0 - -// how shall we initialize the _UCT_ total touched counter? -// 0 = initialize with one, 1 = initialize with number of assertions -#define _UCT_INIT_ 0 - -// do we gradually reduce the touched values of _UCT_? -#define _UCT_FORGET_ 0 -#define _UCT_FORGET_FACTOR_ 0.9 - // shall we use addition/subtraction? -#define _USE_ADDSUB_ 1 +#define _USE_ADDSUB_ 0 // should we use unsat-structures as done in SLS 4 SAT instead for random or bfs selection? #define _REAL_RS_ 0 -// with what probability _PERM_STEP_/1000 will the random step happen? -#define _PERM_RSTEP_ 0 - // shall we use early pruning for incremental update? #define _EARLY_PRUNE_ 1 -// shall we use caching for top_score? -#define _CACHE_TOP_SCORE_ 1 - -#if ((_UCT_ > 0) + _REAL_RS_ > 1) -InvalidConfiguration; -#endif - #endif \ No newline at end of file diff --git a/src/tactic/sls/sls_engine.cpp b/src/tactic/sls/sls_engine.cpp index 938b6e0df..c240a0c51 100644 --- a/src/tactic/sls/sls_engine.cpp +++ b/src/tactic/sls/sls_engine.cpp @@ -44,6 +44,7 @@ sls_engine::sls_engine(ast_manager & m, params_ref const & p) : m_evaluator(m, m_bv_util, m_tracker, m_mpz_manager, m_powers) { updt_params(p); + m_tracker.updt_params(p); } sls_engine::~sls_engine() { @@ -52,19 +53,21 @@ sls_engine::~sls_engine() { m_mpz_manager.del(m_two); } -double sls_engine::get_restart_armin(unsigned cnt_restarts) -{ - unsigned outer_id = (unsigned)(0.5 + sqrt(0.25 + 2 * cnt_restarts)); - unsigned inner_id = cnt_restarts - (outer_id - 1) * outer_id / 2; - return pow((double) _RESTART_CONST_ARMIN_, (int) inner_id + 1); -} - void sls_engine::updt_params(params_ref const & _p) { sls_params p(_p); m_produce_models = _p.get_bool("model", false); - m_max_restarts = p.restarts(); + m_max_restarts = p.max_restarts(); m_tracker.set_random_seed(p.random_seed()); - m_plateau_limit = p.plateau_limit(); + m_walksat = p.walksat(); + m_walksat_repick = p.walksat_repick(); + m_paws_sp = p.paws_sp(); + m_wp = p.wp(); + m_vns_mc = p.vns_mc(); + m_vns_repick = p.vns_repick(); + + m_restart_base = p.restart_base(); + m_restart_next = m_restart_base; + m_restart_init = p.restart_init(); } void sls_engine::checkpoint() { @@ -105,9 +108,7 @@ double sls_engine::top_score() { tout << " " << m_tracker.get_score(m_assertions[i]); tout << " AVG: " << top_sum / (double)sz << std::endl;); -#if _CACHE_TOP_SCORE_ m_tracker.set_top_sum(top_sum); -#endif return top_sum / (double)sz; } @@ -121,37 +122,21 @@ double sls_engine::rescore() { double sls_engine::serious_score(func_decl * fd, const mpz & new_value) { m_evaluator.serious_update(fd, new_value); m_stats.m_incr_evals++; -#if _CACHE_TOP_SCORE_ return (m_tracker.get_top_sum() / m_assertions.size()); -#else - return top_score(); -#endif } double sls_engine::incremental_score(func_decl * fd, const mpz & new_value) { m_evaluator.update(fd, new_value); m_stats.m_incr_evals++; -#if _CACHE_TOP_SCORE_ return (m_tracker.get_top_sum() / m_assertions.size()); -#else - return top_score(); -#endif } double sls_engine::incremental_score_prune(func_decl * fd, const mpz & new_value) { -#if _EARLY_PRUNE_ m_stats.m_incr_evals++; if (m_evaluator.update_prune(fd, new_value)) -#if _CACHE_TOP_SCORE_ return (m_tracker.get_top_sum() / m_assertions.size()); -#else - return top_score(); -#endif else return 0.0; -#else - NOT_IMPLEMENTED_YET(); -#endif } // checks whether the score outcome of a given move is better than the previous score @@ -261,7 +246,7 @@ void sls_engine::mk_random_move(ptr_vector & unsat_constants) // inversion doesn't make sense, let's do a flip instead. if (mt == MV_INV) mt = MV_FLIP; #else - mt = MV_FLIP; + move_type mt = MV_FLIP; #endif unsigned bit = 0; @@ -300,7 +285,7 @@ void sls_engine::mk_random_move(ptr_vector & unsat_constants) tout << "Locally randomized model: " << std::endl; m_tracker.show_model(tout);); } - m_evaluator.update(fd, new_value); + m_evaluator.serious_update(fd, new_value); m_mpz_manager.del(new_value); } @@ -385,7 +370,7 @@ double sls_engine::find_best_move_mc(ptr_vector & to_evaluate, double if (m_bv_util.is_bv_sort(srt) && bv_sz > 2) { for (unsigned j = 0; j < bv_sz; j++) { mk_flip(srt, old_value, j, temp); - for (unsigned l = 0; l < _VNS_MC_TRIES_ && l < bv_sz / 2; l++) + for (unsigned l = 0; l < m_vns_mc && l < bv_sz / 2; l++) { unsigned k = m_tracker.get_random_uint(16) % bv_sz; while (k == j) @@ -411,144 +396,85 @@ double sls_engine::find_best_move_mc(ptr_vector & to_evaluate, double lbool sls_engine::search() { lbool res = l_undef; double score = 0.0, old_score = 0.0; - unsigned new_const = (unsigned)-1, new_bit = 0; + unsigned new_const = (unsigned)-1, new_bit; mpz new_value; move_type move; - unsigned plateau_cnt = 0; score = rescore(); unsigned sz = m_assertions.size(); -#if _RESTARTS_ - while (check_restart(m_stats.m_moves) && m_stats.m_stopwatch.get_current_seconds() < _TIMELIMIT_) { -#else - while (m_stats.m_stopwatch.get_current_seconds() < _TIMELIMIT_) { -#endif - + while (check_restart(m_stats.m_moves)) { checkpoint(); m_stats.m_moves++; - -#if _UCT_FORGET_ - if (m_stats.m_moves % _UCT_FORGET_ == 0) - m_tracker.uct_forget(g); -#endif + if (m_stats.m_moves % m_restart_base == 0) + m_tracker.ucb_forget(m_assertions); #if _REAL_RS_ //m_tracker.debug_real(g, m_stats.m_moves); #endif - -#if _FOCUS_ - expr * e = m_tracker.get_unsat_assertion(m_assertions); - - if (!e) - { - res = l_true; - goto bailout; - } - ptr_vector & to_evaluate = m_tracker.get_unsat_constants_walksat(e); -#else - ptr_vector & to_evaluate = m_tracker.get_unsat_constants_gsat(m_assertions, sz); + + ptr_vector & to_evaluate = m_tracker.get_unsat_constants(m_assertions); if (!to_evaluate.size()) { res = l_true; goto bailout; } -#endif - if (m_tracker.get_random_uint(16) % 1000 < _PERM_RSTEP_) + if (m_wp && m_tracker.get_random_uint(10) < m_wp) { mk_random_move(to_evaluate); -#if _CACHE_TOP_SCORE_ score = m_tracker.get_top_sum() / sz; -#else - score = top_score(g); -#endif continue; } old_score = score; new_const = (unsigned)-1; - move = MV_FLIP; - new_bit = 0; score = find_best_move(to_evaluate, score, new_const, new_value, new_bit, move); -#if _VNS_MC_ > _VNS_REPICK_ -#if _VNS_MC_ - if (new_const == static_cast(-1)) - score = find_best_move_mc(g, to_evaluate, score, new_const, new_value); -#endif -#if _VNS_REPICK_ - if (new_const == static_cast(-1)) + if (m_vns_mc && (new_const == static_cast(-1))) + score = find_best_move_mc(to_evaluate, score, new_const, new_value); + + /*if (m_vns_repick && (new_const == static_cast(-1))) { - expr * q = m_tracker.get_new_unsat_assertion(g, e); + expr * q = m_tracker.get_new_unsat_assertion(m_assertions, e); if (q) { ptr_vector & to_evaluate2 = m_tracker.get_unsat_constants_walksat(e); - score = find_best_move(g, to_evaluate2, score, new_const, new_value, new_bit, move); + score = find_best_move(to_evaluate2, score, new_const, new_value, new_bit, move); } - } -#endif -#endif - -#if _VNS_MC_ < _VNS_REPICK_ -#if _VNS_REPICK_ - if (new_const == static_cast(-1)) - { - expr * q = m_tracker.get_new_unsat_assertion(g, e); - if (q) - { - ptr_vector & to_evaluate2 = m_tracker.get_unsat_constants_walksat(e); - score = find_best_move(g, to_evaluate2, score, new_const, new_value, new_bit, move); - } - } -#endif -#if _VNS_MC_ - if (new_const == static_cast(-1)) - score = find_best_move_mc(g, to_evaluate, score, new_const, new_value); -#endif -#endif + }*/ if (new_const == static_cast(-1)) { score = old_score; - plateau_cnt++; -#if _REPICK_ + if (m_walksat && m_walksat_repick) m_evaluator.randomize_local(m_assertions); -#else + else m_evaluator.randomize_local(to_evaluate); -#endif -#if _CACHE_TOP_SCORE_ score = m_tracker.get_top_sum() / m_assertions.size(); -#else - score = top_score(g); -#endif -#if _PAWS_ - for (unsigned i = 0; i < sz; i++) + if (m_paws_sp < 1024) { - expr * q = m_assertions[i]; - if (m_tracker.get_random_uint(16) % 100 < _PAWS_) + for (unsigned i = 0; i < sz; i++) { - if (m_mpz_manager.eq(m_tracker.get_value(q),m_one)) - m_tracker.decrease_weight(q); - } - else - { - if (m_mpz_manager.eq(m_tracker.get_value(q),m_zero)) - m_tracker.increase_weight(q); + expr * q = m_assertions[i]; + if (m_tracker.get_random_uint(10) < m_paws_sp) + { + if (m_mpz_manager.eq(m_tracker.get_value(q),m_one)) + m_tracker.decrease_weight(q); + } + else + { + if (m_mpz_manager.eq(m_tracker.get_value(q),m_zero)) + m_tracker.increase_weight(q); + } } } -#endif - } else { func_decl * fd = to_evaluate[new_const]; -#if _REAL_RS_ || _PAWS_ score = serious_score(fd, new_value); -#else - score = incremental_score(fd, new_value); -#endif } } @@ -569,30 +495,9 @@ void sls_engine::operator()(goal_ref const & g, model_converter_ref & mc) { for (unsigned i = 0; i < g->size(); i++) assert_expr(g->form(i)); - verbose_stream() << "_FOCUS_ " << _FOCUS_ << std::endl; - verbose_stream() << "_RESTARTS_ " << _RESTARTS_ << std::endl; - verbose_stream() << "_RESTART_LIMIT_ " << _RESTART_LIMIT_ << std::endl; - verbose_stream() << "_RESTART_INIT_ " << _RESTART_INIT_ << std::endl; - verbose_stream() << "_RESTART_SCHEME_ " << _RESTART_SCHEME_ << std::endl; - verbose_stream() << "_TIMELIMIT_ " << _TIMELIMIT_ << std::endl; - verbose_stream() << "_PAWS_ " << _PAWS_ << std::endl; - verbose_stream() << "_PAWS_INIT_ " << _PAWS_INIT_ << std::endl; - verbose_stream() << "_VNS_MC_ " << _VNS_MC_ << std::endl; - verbose_stream() << "_VNS_MC_TRIES_ " << _VNS_MC_TRIES_ << std::endl; - verbose_stream() << "_VNS_REPICK_ " << _VNS_REPICK_ << std::endl; - verbose_stream() << "_WEIGHT_DIST_ " << _WEIGHT_DIST_ << std::endl; - verbose_stream() << "_WEIGHT_DIST_FACTOR_ " << std::fixed << std::setprecision(2) << _WEIGHT_DIST_FACTOR_ << std::endl; - verbose_stream() << "_REPICK_ " << _REPICK_ << std::endl; - verbose_stream() << "_UCT_ " << _UCT_ << std::endl; - verbose_stream() << "_UCT_CONSTANT_ " << std::fixed << std::setprecision(2) << _UCT_CONSTANT_ << std::endl; - verbose_stream() << "_UCT_INIT_ " << _UCT_INIT_ << std::endl; - verbose_stream() << "_UCT_FORGET_ " << _UCT_FORGET_ << std::endl; - verbose_stream() << "_UCT_FORGET_FACTOR_ " << std::fixed << std::setprecision(2) << _UCT_FORGET_FACTOR_ << std::endl; verbose_stream() << "_USE_ADDSUB_ " << _USE_ADDSUB_ << std::endl; verbose_stream() << "_REAL_RS_ " << _REAL_RS_ << std::endl; - verbose_stream() << "_PERM_RSTEP_ " << _PERM_RSTEP_ << std::endl; verbose_stream() << "_EARLY_PRUNE_ " << _EARLY_PRUNE_ << std::endl; - verbose_stream() << "_CACHE_TOP_SCORE_ " << _CACHE_TOP_SCORE_ << std::endl; lbool res = operator()(); @@ -620,8 +525,6 @@ lbool sls_engine::operator()() { m_tracker.initialize(m_assertions); lbool res = l_undef; - m_restart_limit = _RESTART_LIMIT_; - do { checkpoint(); @@ -630,39 +533,53 @@ lbool sls_engine::operator()() { if (res == l_undef) { -#if _RESTART_INIT_ - m_tracker.randomize(); -#else - m_tracker.reset(m_assertions); -#endif + if (m_restart_init) + m_tracker.randomize(m_assertions); + else + m_tracker.reset(m_assertions); } - } while (m_stats.m_stopwatch.get_current_seconds() < _TIMELIMIT_ && res != l_true && m_stats.m_restarts++ < m_max_restarts); + } while (res != l_true && m_stats.m_restarts++ < m_max_restarts); verbose_stream() << "(restarts: " << m_stats.m_restarts << " flips: " << m_stats.m_moves << " time: " << std::fixed << std::setprecision(2) << m_stats.m_stopwatch.get_current_seconds() << " fps: " << (m_stats.m_moves / m_stats.m_stopwatch.get_current_seconds()) << ")" << std::endl; return res; } -unsigned sls_engine::check_restart(unsigned curr_value) +/* Andreas: Needed for Armin's restart scheme if we don't want to use loops. +inline double sls_engine::get_restart_armin(unsigned cnt_restarts) { - if (curr_value > m_restart_limit) + unsigned outer_id = (unsigned)(0.5 + sqrt(0.25 + 2 * cnt_restarts)); + unsigned inner_id = cnt_restarts - (outer_id - 1) * outer_id / 2; + return pow((double) _RESTART_CONST_ARMIN_, (int) inner_id + 1); +} +*/ + +inline unsigned sls_engine::check_restart(unsigned curr_value) +{ + if (curr_value > m_restart_next) { + /* Andreas: My own scheme (= 1) seems to work best. Other schemes are disabled so that we save 1 parameter. + I leave the other versions as comments in case you want to try it again somewhen. #if _RESTART_SCHEME_ == 5 - m_restart_limit += (unsigned)(_RESTART_LIMIT_ * pow(_RESTART_CONST_ARMIN_, m_stats.m_restarts)); + m_restart_next += (unsigned)(m_restart_base * pow(_RESTART_CONST_ARMIN_, m_stats.m_restarts)); #elif _RESTART_SCHEME_ == 4 - m_restart_limit += (m_stats.m_restarts & (m_stats.m_restarts + 1)) ? _RESTART_LIMIT_ : (_RESTART_LIMIT_ * m_stats.m_restarts + 1); + m_restart_next += (m_stats.m_restarts & (m_stats.m_restarts + 1)) ? m_restart_base : (m_restart_base * m_stats.m_restarts + 1); #elif _RESTART_SCHEME_ == 3 - m_restart_limit += (unsigned)get_restart_armin(m_stats.m_restarts + 1) * _RESTART_LIMIT_; + m_restart_next += (unsigned)get_restart_armin(m_stats.m_restarts + 1) * m_restart_base; #elif _RESTART_SCHEME_ == 2 - m_restart_limit += get_luby(m_stats.m_restarts + 1) * _RESTART_LIMIT_; + m_restart_next += get_luby(m_stats.m_restarts + 1) * m_restart_base; #elif _RESTART_SCHEME_ == 1 if (m_stats.m_restarts & 1) - m_restart_limit += _RESTART_LIMIT_; + m_restart_next += m_restart_base; else - m_restart_limit += (2 << (m_stats.m_restarts >> 1)) * _RESTART_LIMIT_; + m_restart_next += (2 << (m_stats.m_restarts >> 1)) * m_restart_base; #else - m_restart_limit += _RESTART_LIMIT_; -#endif + m_restart_limit += m_restart_base; +#endif */ + if (m_stats.m_restarts & 1) + m_restart_next += m_restart_base; + else + m_restart_next += (2 << (m_stats.m_restarts >> 1)) * m_restart_base; return 0; } return 1; diff --git a/src/tactic/sls/sls_engine.h b/src/tactic/sls/sls_engine.h index 4e5af8c93..ff0e55f24 100644 --- a/src/tactic/sls/sls_engine.h +++ b/src/tactic/sls/sls_engine.h @@ -70,9 +70,16 @@ protected: sls_evaluator m_evaluator; ptr_vector m_assertions; - unsigned m_restart_limit; unsigned m_max_restarts; - unsigned m_plateau_limit; + unsigned m_walksat; + unsigned m_walksat_repick; + unsigned m_wp; + unsigned m_vns_mc; + unsigned m_vns_repick; + unsigned m_paws_sp; + unsigned m_restart_base; + unsigned m_restart_next; + unsigned m_restart_init; ptr_vector m_old_values; @@ -110,7 +117,6 @@ public: protected: void checkpoint(); - double get_restart_armin(unsigned cnt_restarts); bool what_if(func_decl * fd, const unsigned & fd_inx, const mpz & temp, double & best_score, unsigned & best_const, mpz & best_value); @@ -129,6 +135,7 @@ protected: void mk_random_move(ptr_vector & unsat_constants); + //inline double get_restart_armin(unsigned cnt_restarts); inline unsigned check_restart(unsigned curr_value); }; diff --git a/src/tactic/sls/sls_evaluator.h b/src/tactic/sls/sls_evaluator.h index da2a4b29f..37bfa5a2d 100644 --- a/src/tactic/sls/sls_evaluator.h +++ b/src/tactic/sls/sls_evaluator.h @@ -81,11 +81,7 @@ public: case OP_AND: { m_mpz_manager.set(result, m_one); for (unsigned i = 0; i < n_args; i++) -#if _DIRTY_UP_ - if (m_mpz_manager.neq(m_tracker.get_value(args[i]), result) && !m_tracker.is_top_expr(args[i])) { -#else if (m_mpz_manager.neq(m_tracker.get_value(args[i]), result)) { -#endif m_mpz_manager.set(result, m_zero); break; } @@ -93,11 +89,7 @@ public: } case OP_OR: { for (unsigned i = 0; i < n_args; i++) -#if _DIRTY_UP_ - if (m_mpz_manager.neq(m_tracker.get_value(args[i]), result) || m_tracker.is_top_expr(args[i])) { -#else if (m_mpz_manager.neq(m_tracker.get_value(args[i]), result)) { -#endif m_mpz_manager.set(result, m_one); break; } @@ -105,16 +97,9 @@ public: } case OP_NOT: { SASSERT(n_args == 1); -#if _DIRTY_UP_ - if (m_tracker.is_top_expr(args[0])) - m_mpz_manager.set(result, m_zero); - else - m_mpz_manager.set(result, (m_mpz_manager.is_zero(m_tracker.get_value(args[0]))) ? m_one : m_zero); -#else const mpz & child = m_tracker.get_value(args[0]); SASSERT(m_mpz_manager.is_one(child) || m_mpz_manager.is_zero(child)); m_mpz_manager.set(result, (m_mpz_manager.is_zero(child)) ? m_one : m_zero); -#endif break; } case OP_EQ: { @@ -545,9 +530,7 @@ public: expr_fast_mark1 visited; mpz new_value; -#if _EARLY_PRUNE_ || _CACHE_TOP_SCORE_ double new_score; -#endif SASSERT(cur_depth < m_traversal_stack.size()); while (cur_depth != static_cast(-1)) { @@ -569,23 +552,12 @@ public: } #endif + new_score = m_tracker.score(cur); + if (m_tracker.is_top_expr(cur)) + m_tracker.adapt_top_sum(cur, new_score, m_tracker.get_score(cur)); + m_tracker.set_score(cur, new_score); #if _EARLY_PRUNE_ - new_score = m_tracker.score(cur); -#if _CACHE_TOP_SCORE_ - if (m_tracker.is_top_expr(cur)) - m_tracker.adapt_top_sum(cur, new_score, m_tracker.get_score(cur)); -#endif - m_tracker.set_score(cur, new_score); m_tracker.set_score_prune(cur, new_score); -#else -#if _CACHE_TOP_SCORE_ - new_score = m_tracker.score(cur); - if (m_tracker.is_top_expr(cur)) - m_tracker.adapt_top_sum(cur, new_score, m_tracker.get_score(cur)); - m_tracker.set_score(cur, new_score); -#else - m_tracker.set_score(cur, m_tracker.score(cur)); -#endif #endif if (m_tracker.has_uplinks(cur)) { @@ -614,9 +586,7 @@ public: expr_fast_mark1 visited; mpz new_value; -#if _EARLY_PRUNE_ || _CACHE_TOP_SCORE_ double new_score; -#endif SASSERT(cur_depth < m_traversal_stack.size()); while (cur_depth != static_cast(-1)) { @@ -627,23 +597,12 @@ public: (*this)(to_app(cur), new_value); m_tracker.set_value(cur, new_value); + new_score = m_tracker.score(cur); + if (m_tracker.is_top_expr(cur)) + m_tracker.adapt_top_sum(cur, new_score, m_tracker.get_score(cur)); + m_tracker.set_score(cur, new_score); #if _EARLY_PRUNE_ - new_score = m_tracker.score(cur); -#if _CACHE_TOP_SCORE_ - if (m_tracker.is_top_expr(cur)) - m_tracker.adapt_top_sum(cur, new_score, m_tracker.get_score(cur)); -#endif - m_tracker.set_score(cur, new_score); m_tracker.set_score_prune(cur, new_score); -#else -#if _CACHE_TOP_SCORE_ - new_score = m_tracker.score(cur); - if (m_tracker.is_top_expr(cur)) - m_tracker.adapt_top_sum(cur, new_score, m_tracker.get_score(cur)); - m_tracker.set_score(cur, new_score); -#else - m_tracker.set_score(cur, m_tracker.score(cur)); -#endif #endif if (m_tracker.has_uplinks(cur)) { ptr_vector & ups = m_tracker.get_uplinks(cur); @@ -679,11 +638,7 @@ public: m_traversal_stack[cur_depth].push_back(ep); if (cur_depth > max_depth) max_depth = cur_depth; } -#if _REAL_RS_ || _PAWS_ run_serious_update(max_depth); -#else - run_update(max_depth); -#endif } void update(func_decl * fd, const mpz & new_value) { @@ -708,7 +663,6 @@ public: run_serious_update(cur_depth); } -#if _EARLY_PRUNE_ unsigned run_update_bool_prune(unsigned cur_depth) { expr_fast_mark1 visited; @@ -722,10 +676,9 @@ public: expr * cur = cur_depth_exprs[i]; new_score = m_tracker.score(cur); -#if _CACHE_TOP_SCORE_ if (m_tracker.is_top_expr(cur)) m_tracker.adapt_top_sum(cur, new_score, m_tracker.get_score(cur)); -#endif + prune_score = m_tracker.get_score_prune(cur); m_tracker.set_score(cur, new_score); @@ -746,9 +699,6 @@ public: } } } - else - { - } } cur_depth_exprs.reset(); @@ -762,14 +712,11 @@ public: for (unsigned i = 0; i < cur_size; i++) { expr * cur = cur_depth_exprs[i]; -#if _CACHE_TOP_SCORE_ new_score = m_tracker.score(cur); if (m_tracker.is_top_expr(cur)) m_tracker.adapt_top_sum(cur, new_score, m_tracker.get_score(cur)); m_tracker.set_score(cur, new_score); -#else - m_tracker.set_score(cur, m_tracker.score(cur)); -#endif + if (m_tracker.has_uplinks(cur)) { ptr_vector & ups = m_tracker.get_uplinks(cur); for (unsigned j = 0; j < ups.size(); j++) { @@ -850,103 +797,6 @@ public: } return run_update_bool_prune(cur_depth); } -#endif - - unsigned run_update_bool_prune_new(unsigned cur_depth) { - expr_fast_mark1 visited; - - double prune_score, new_score; - unsigned pot_benefits = 0; - SASSERT(cur_depth < m_traversal_stack_bool.size()); - - ptr_vector & cur_depth_exprs = m_traversal_stack_bool[cur_depth]; - - for (unsigned i = 0; i < cur_depth_exprs.size(); i++) { - expr * cur = cur_depth_exprs[i]; - - new_score = m_tracker.score(cur); - if (m_tracker.is_top_expr(cur)) - m_tracker.adapt_top_sum(cur, new_score, m_tracker.get_score(cur)); - prune_score = m_tracker.get_score_prune(cur); - m_tracker.set_score(cur, new_score); - - if ((new_score >= prune_score) && (m_tracker.has_pos_occ(cur))) - pot_benefits = 1; - if ((new_score < prune_score) && (m_tracker.has_neg_occ(cur))) - pot_benefits = 1; - - if (m_tracker.has_uplinks(cur)) { - ptr_vector & ups = m_tracker.get_uplinks(cur); - for (unsigned j = 0; j < ups.size(); j++) { - expr * next = ups[j]; - unsigned next_d = m_tracker.get_distance(next); - SASSERT(next_d < cur_depth); - if (!visited.is_marked(next)) { - m_traversal_stack_bool[next_d].push_back(next); - visited.mark(next); - } - } - } - else - { - } - } - - cur_depth_exprs.reset(); - cur_depth--; - - while (cur_depth != static_cast(-1)) { - ptr_vector & cur_depth_exprs = m_traversal_stack_bool[cur_depth]; - if (pot_benefits) - { - unsigned cur_size = cur_depth_exprs.size(); - for (unsigned i = 0; i < cur_size; i++) { - expr * cur = cur_depth_exprs[i]; - - new_score = m_tracker.score(cur); - if (m_tracker.is_top_expr(cur)) - m_tracker.adapt_top_sum(cur, new_score, m_tracker.get_score(cur)); - m_tracker.set_score(cur, new_score); - if (m_tracker.has_uplinks(cur)) { - ptr_vector & ups = m_tracker.get_uplinks(cur); - for (unsigned j = 0; j < ups.size(); j++) { - expr * next = ups[j]; - unsigned next_d = m_tracker.get_distance(next); - SASSERT(next_d < cur_depth); - if (!visited.is_marked(next)) { - m_traversal_stack_bool[next_d].push_back(next); - visited.mark(next); - } - } - } - } - } - cur_depth_exprs.reset(); - cur_depth--; - } - - return pot_benefits; - } - - unsigned update_prune_new(func_decl * fd, const mpz & new_value) { - m_tracker.set_value(fd, new_value); - expr * ep = m_tracker.get_entry_point(fd); - unsigned cur_depth = m_tracker.get_distance(ep); - - if (m_traversal_stack_bool.size() <= cur_depth) - m_traversal_stack_bool.resize(cur_depth+1); - if (m_traversal_stack.size() <= cur_depth) - m_traversal_stack.resize(cur_depth+1); - - if (m_manager.is_bool(ep)) - m_traversal_stack_bool[cur_depth].push_back(ep); - else - { - m_traversal_stack[cur_depth].push_back(ep); - run_update_prune(cur_depth); - } - return run_update_bool_prune_new(cur_depth); - } void randomize_local(ptr_vector & unsat_constants) { // Randomize _one_ candidate: @@ -954,11 +804,8 @@ public: func_decl * fd = unsat_constants[r]; mpz temp = m_tracker.get_random(fd->get_range()); -#if _REAL_RS_ || _PAWS_ serious_update(fd, temp); -#else - update(fd, temp); -#endif + m_mpz_manager.del(temp); TRACE("sls", tout << "Randomization candidate: " << unsat_constants[r]->get_name() << std::endl; diff --git a/src/tactic/sls/sls_tactic.cpp b/src/tactic/sls/sls_tactic.cpp index 7a9252fe2..2a40e908d 100644 --- a/src/tactic/sls/sls_tactic.cpp +++ b/src/tactic/sls/sls_tactic.cpp @@ -159,16 +159,12 @@ tactic * mk_preamble(ast_manager & m, params_ref const & p) { using_params(mk_simplify_tactic(m), simp2_p)), using_params(mk_simplify_tactic(m), hoist_p), mk_max_bv_sharing_tactic(m), - // Andreas: It would be cool to get rid of shared top level assertions but which simplification is doing this? - //mk_ctx_simplify_tactic(m, ctx_p), - // Andreas: This one at least eliminates top level duplicates ... but has very bad effects on performance! - //mk_simplify_tactic(m), mk_nnf_tactic(m, p)); } tactic * mk_qfbv_sls_tactic(ast_manager & m, params_ref const & p) { tactic * t = and_then(mk_preamble(m, p), mk_sls_tactic(m)); -// tactic * t = and_then(mk_simplify_tactic(m), mk_nnf_tactic(m, p), mk_sls_tactic(m)); + //tactic * t = and_then(mk_simplify_tactic(m), mk_nnf_tactic(m, p), mk_sls_tactic(m)); t->updt_params(p); return t; } diff --git a/src/tactic/sls/sls_tracker.h b/src/tactic/sls/sls_tracker.h index 235ab9471..65011dc8d 100644 --- a/src/tactic/sls/sls_tracker.h +++ b/src/tactic/sls/sls_tracker.h @@ -39,11 +39,7 @@ class sls_tracker { mpz m_zero, m_one, m_two; struct value_score { -#if _EARLY_PRUNE_ value_score() : m(0), value(unsynch_mpz_manager::mk_z(0)), score(0.0), distance(0), touched(1), score_prune(0.0), has_pos_occ(0), has_neg_occ(0) { }; -#else - value_score() : m(0), value(unsynch_mpz_manager::mk_z(0)), score(0.0), distance(0), touched(1) { }; -#endif ~value_score() { if (m) m->del(value); } unsynch_mpz_manager * m; mpz value; @@ -80,20 +76,22 @@ private: ptr_vector m_constants; ptr_vector m_temp_constants; occ_type m_constants_occ; -#if _UCT_ + + unsigned m_walksat; + unsigned m_ucb; + double m_ucb_constant; + unsigned m_ucb_init; + double m_ucb_forget; unsigned m_touched; -#endif + double m_scale_unsat; + unsigned m_paws_init; #if _REAL_RS_ ptr_vector m_unsat_expr; obj_map m_where_false; expr** m_list_false; #endif -#if _PAWS_ obj_map m_weights; -#endif -#if _CACHE_TOP_SCORE_ double m_top_sum; -#endif unsigned m_equal_scores; public: @@ -114,6 +112,17 @@ public: m_mpz_manager.del(m_two); } + void updt_params(params_ref const & _p) { + sls_params p(_p); + m_walksat = p.walksat(); + m_ucb = p.walksat_ucb(); + m_ucb_constant = p.walksat_ucb_constant(); + m_ucb_init = p.walksat_ucb_init(); + m_ucb_forget = p.walksat_ucb_forget(); + m_scale_unsat = p.scale_unsat(); + m_paws_init = p.paws_init(); + } + unsigned get_formula_size() { return m_scores.size(); } @@ -147,13 +156,8 @@ public: return ++m_equal_scores; } -#if _CACHE_TOP_SCORE_ inline void adapt_top_sum(expr * e, double add, double sub) { -#if _PAWS_ m_top_sum += m_weights.find(e) * (add - sub); -#else - m_top_sum += add - sub; -#endif } inline void set_top_sum(double new_score) { @@ -163,7 +167,6 @@ public: inline double get_top_sum() { return m_top_sum; } -#endif inline void set_value(expr * n, const mpz & r) { SASSERT(m_scores.contains(n)); @@ -209,7 +212,6 @@ public: return get_score(ep); } -#if _EARLY_PRUNE_ inline void set_score_prune(expr * n, double score) { SASSERT(m_scores.contains(n)); m_scores.find(n).score_prune = score; @@ -229,7 +231,6 @@ public: SASSERT(m_scores.contains(n)); return m_scores.find(n).has_neg_occ; } -#endif inline unsigned get_distance(expr * n) { SASSERT(m_scores.contains(n)); @@ -310,17 +311,20 @@ public: } #endif - void uct_forget(ptr_vector & as) { - expr * e; - unsigned touched_old, touched_new; - - for (unsigned i = 0; i < as.size(); i++) + inline void ucb_forget(ptr_vector & as) { + if (m_ucb_forget < 1.0) { - e = as[i]; - touched_old = m_scores.find(e).touched; - touched_new = (unsigned)((touched_old - 1) * _UCT_FORGET_FACTOR_ + 1); - m_scores.find(e).touched = touched_new; - m_touched += touched_new - touched_old; + expr * e; + unsigned touched_old, touched_new; + + for (unsigned i = 0; i < as.size(); i++) + { + e = as[i]; + touched_old = m_scores.find(e).touched; + touched_new = (unsigned)((touched_old - 1) * m_ucb_forget + 1); + m_scores.find(e).touched = touched_new; + m_touched += touched_new - touched_old; + } } } @@ -490,26 +494,21 @@ public: //} #endif -#if _PAWS_ for (unsigned i = 0; i < sz; i++) { expr * e = as[i]; if (!m_weights.contains(e)) - m_weights.insert(e, _PAWS_INIT_); + m_weights.insert(e, m_paws_init); } -#endif #if _EARLY_PRUNE_ for (unsigned i = 0; i < sz; i++) setup_occs(as[i]); #endif -#if _UCT_ - m_touched = _UCT_INIT_ ? as.size() : 1; -#endif + m_touched = m_ucb_init ? as.size() : 1; } -#if _PAWS_ void increase_weight(expr * e) { m_weights.find(e)++; @@ -518,14 +517,13 @@ public: void decrease_weight(expr * e) { unsigned old_weight = m_weights.find(e); - m_weights.find(e) = old_weight > _PAWS_INIT_ ? old_weight - 1 : _PAWS_INIT_; + m_weights.find(e) = old_weight > m_paws_init ? old_weight - 1 : m_paws_init; } unsigned get_weight(expr * e) { return m_weights.find(e); } -#endif #if _REAL_RS_ void make_assertion(expr * e) @@ -684,7 +682,6 @@ public: } } -#if _EARLY_PRUNE_ void setup_occs(expr * n, bool negated = false) { if (m_manager.is_bool(n)) { @@ -717,7 +714,6 @@ public: else NOT_IMPLEMENTED_YET(); } -#endif double score_bool(expr * n, bool negated = false) { TRACE("sls_score", tout << ((negated)?"NEG ":"") << "BOOL: " << mk_ismt2_pp(n, m_manager) << std::endl; ); @@ -735,20 +731,17 @@ public: SASSERT(!negated); app * a = to_app(n); expr * const * args = a->get_args(); - // Andreas: Seems to have no effect. Probably it does not even occur. -#if _SCORE_AND_AVG_ + /* Andreas: Seems to have no effect. But maybe you want to try it again at some point. double sum = 0.0; for (unsigned i = 0; i < a->get_num_args(); i++) sum += get_score(args[i]); - res = sum / (double) a->get_num_args(); -#else + res = sum / (double) a->get_num_args(); */ double min = 1.0; for (unsigned i = 0; i < a->get_num_args(); i++) { double cur = get_score(args[i]); if (cur < min) min = cur; } res = min; -#endif } else if (m_manager.is_or(n)) { SASSERT(!negated); @@ -927,13 +920,11 @@ public: SASSERT(res >= 0.0 && res <= 1.0); -#if _WEIGHT_DIST_ app * a = to_app(n); family_id afid = a->get_family_id(); if (afid == m_bv_util.get_family_id()) - if (res < 1.0) res *= _WEIGHT_DIST_FACTOR_; -#endif + if (res < 1.0) res *= m_scale_unsat; TRACE("sls_score", tout << "SCORE = " << res << std::endl; ); return res; @@ -995,8 +986,8 @@ public: return m_temp_constants; } - ptr_vector & get_unsat_constants_gsat(ptr_vector const & as, unsigned sz) { - + ptr_vector & get_unsat_constants_gsat(ptr_vector const & as) { + unsigned sz = as.size(); if (sz == 1) { if (m_mpz_manager.neq(get_value(as[0]), m_one)) return get_constants(); @@ -1033,89 +1024,88 @@ public: } ptr_vector & get_unsat_constants(ptr_vector const & as) { -#if _FOCUS_ - expr * e = get_unsat_assertion(as); - - if (!e) + if (m_walksat) { - m_temp_constants.reset(); - return m_temp_constants; - } + expr * e = get_unsat_assertion(as); - return get_unsat_constants_walksat(e); -#else - return m_tracker.get_unsat_constants_gsat(as, sz); -#endif + if (!e) + { + m_temp_constants.reset(); + return m_temp_constants; + } + + return get_unsat_constants_walksat(e); + } + else + return get_unsat_constants_gsat(as); } expr * get_unsat_assertion(ptr_vector const & as) { unsigned sz = as.size(); - if (sz == 1) { if (m_mpz_manager.neq(get_value(as[0]), m_one)) return as[0]; else return 0; } - m_temp_constants.reset(); -#if _UCT_ + unsigned pos = -1; - value_score vscore; - double max = -1.0; + if (m_ucb) + { + value_score vscore; + double max = -1.0; for (unsigned i = 0; i < sz; i++) { expr * e = as[i]; // for (unsigned i = 0; i < m_where_false.size(); i++) { // expr * e = m_list_false[i]; vscore = m_scores.find(e); -#if _UCT_ == 1 - double q = vscore.score + _UCT_CONSTANT_ * sqrt(log((double)m_touched) / vscore.touched); -#elif _UCT_ == 3 + double q = vscore.score + m_ucb_constant * sqrt(log((double)m_touched) / vscore.touched); +#if _UCT_ == 3 double q = vscore.score + _UCT_CONSTANT_ * sqrt(log(m_touched)/vscore.touched) + (get_random_uint(16) * 0.1 / (2<<16)); #endif - if (q > max && m_mpz_manager.neq(get_value(e), m_one) ) { max = q; pos = i; } + if (q > max && m_mpz_manager.neq(get_value(e), m_one) ) { max = q; pos = i; } } - if (pos == static_cast(-1)) - return 0; + if (pos == static_cast(-1)) + return 0; -#if _UCT_ - m_scores.find(as[pos]).touched++; - m_touched++; -#endif + m_scores.find(as[pos]).touched++; + m_touched++; // return m_list_false[pos]; + } + else + { + unsigned cnt_unsat = 0; + for (unsigned i = 0; i < sz; i++) + if (m_mpz_manager.neq(get_value(as[i]), m_one) && (get_random_uint(16) % ++cnt_unsat == 0)) pos = i; + if (pos == static_cast(-1)) + return 0; + } + return as[pos]; -#elif _REAL_RS_ +#if _REAL_RS_ //unsigned pos = m_false_list[get_random_uint(16) % m_cnt_false]; //expr * e = m_unsat_expr[get_random_uint(16) % m_unsat_expr.size()]; sz = m_where_false.size(); if (sz == 0) return 0; return m_list_false[get_random_uint(16) % sz]; -#else - unsigned cnt_unsat = 0, pos = -1; - for (unsigned i = 0; i < sz; i++) - if (m_mpz_manager.neq(get_value(as[i]), m_one) && (get_random_uint(16) % ++cnt_unsat == 0)) pos = i; - if (pos == static_cast(-1)) - return 0; #endif - return as[pos]; } - expr * get_new_unsat_assertion(goal_ref const & g, expr * e) { - unsigned sz = g->size(); - + expr * get_new_unsat_assertion(ptr_vector const & as, expr * e) { + unsigned sz = as.size(); if (sz == 1) return 0; - m_temp_constants.reset(); - + unsigned cnt_unsat = 0, pos = -1; for (unsigned i = 0; i < sz; i++) - if (m_mpz_manager.neq(get_value(g->form(i)), m_one) && (get_random_uint(16) % ++cnt_unsat == 0) && (g->form(i) != e)) pos = i; + if (m_mpz_manager.neq(get_value(as[i]), m_one) && (get_random_uint(16) % ++cnt_unsat == 0) && (as[i] != e)) pos = i; if (pos == static_cast(-1)) return 0; - return g->form(pos); + return as[pos]; } }; From 8346aed39c927923365efa3c2dbabc5bace18cb7 Mon Sep 17 00:00:00 2001 From: Andreas Froehlich Date: Tue, 22 Apr 2014 01:07:30 +0100 Subject: [PATCH 3/7] Fixed bug with VNS repick. --- src/tactic/sls/sls_compilation_settings.h | 2 +- src/tactic/sls/sls_engine.cpp | 22 +++++++++++++++++----- src/tactic/sls/sls_tracker.h | 7 ++++--- 3 files changed, 22 insertions(+), 9 deletions(-) diff --git a/src/tactic/sls/sls_compilation_settings.h b/src/tactic/sls/sls_compilation_settings.h index 9add78daa..a649bc9ed 100644 --- a/src/tactic/sls/sls_compilation_settings.h +++ b/src/tactic/sls/sls_compilation_settings.h @@ -23,7 +23,7 @@ Notes: #define _SLS_COMPILATION_SETTINGS_H_ // shall we use addition/subtraction? -#define _USE_ADDSUB_ 0 +#define _USE_ADDSUB_ 1 // should we use unsat-structures as done in SLS 4 SAT instead for random or bfs selection? #define _REAL_RS_ 0 diff --git a/src/tactic/sls/sls_engine.cpp b/src/tactic/sls/sls_engine.cpp index c240a0c51..af8ae1df2 100644 --- a/src/tactic/sls/sls_engine.cpp +++ b/src/tactic/sls/sls_engine.cpp @@ -68,6 +68,12 @@ void sls_engine::updt_params(params_ref const & _p) { m_restart_base = p.restart_base(); m_restart_next = m_restart_base; m_restart_init = p.restart_init(); + + // Andreas: Would cause trouble because repick requires an assertion being picked before which is not the case in GSAT. + if (m_walksat_repick && !m_walksat) + NOT_IMPLEMENTED_YET(); + if (m_vns_repick && !m_walksat) + NOT_IMPLEMENTED_YET(); } void sls_engine::checkpoint() { @@ -435,19 +441,25 @@ lbool sls_engine::search() { 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))) + if (m_vns_repick && (new_const == static_cast(-1))) { - expr * q = m_tracker.get_new_unsat_assertion(m_assertions, e); + expr * q = m_tracker.get_new_unsat_assertion(m_assertions); if (q) { - ptr_vector & to_evaluate2 = m_tracker.get_unsat_constants_walksat(e); + ptr_vector & to_evaluate2 = m_tracker.get_unsat_constants_walksat(q); score = find_best_move(to_evaluate2, score, new_const, new_value, new_bit, move); + + if (new_const != static_cast(-1)) { + func_decl * fd = to_evaluate2[new_const]; + score = serious_score(fd, new_value); + continue; + } } - }*/ + } if (new_const == static_cast(-1)) { score = old_score; - if (m_walksat && m_walksat_repick) + if (m_walksat_repick) m_evaluator.randomize_local(m_assertions); else m_evaluator.randomize_local(to_evaluate); diff --git a/src/tactic/sls/sls_tracker.h b/src/tactic/sls/sls_tracker.h index 65011dc8d..7b48057d4 100644 --- a/src/tactic/sls/sls_tracker.h +++ b/src/tactic/sls/sls_tracker.h @@ -76,7 +76,7 @@ private: ptr_vector m_constants; ptr_vector m_temp_constants; occ_type m_constants_occ; - + unsigned m_last_pos; unsigned m_walksat; unsigned m_ucb; double m_ucb_constant; @@ -1082,6 +1082,7 @@ public: return 0; } + m_last_pos = pos; return as[pos]; #if _REAL_RS_ //unsigned pos = m_false_list[get_random_uint(16) % m_cnt_false]; @@ -1093,7 +1094,7 @@ public: #endif } - expr * get_new_unsat_assertion(ptr_vector const & as, expr * e) { + expr * get_new_unsat_assertion(ptr_vector const & as) { unsigned sz = as.size(); if (sz == 1) return 0; @@ -1101,7 +1102,7 @@ public: unsigned cnt_unsat = 0, pos = -1; for (unsigned i = 0; i < sz; i++) - if (m_mpz_manager.neq(get_value(as[i]), m_one) && (get_random_uint(16) % ++cnt_unsat == 0) && (as[i] != e)) pos = i; + if ((i != m_last_pos) && 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; From c441bb4388e6cd007c68e0974f4acf2c3a4e7d33 Mon Sep 17 00:00:00 2001 From: Andreas Froehlich Date: Tue, 22 Apr 2014 16:10:44 +0100 Subject: [PATCH 4/7] Backup before I touch early pruning ... --- src/tactic/sls/sls_compilation_settings.h | 3 --- src/tactic/sls/sls_engine.cpp | 30 +++++++++++++---------- src/tactic/sls/sls_engine.h | 1 + src/tactic/sls/sls_evaluator.h | 4 +-- src/tactic/sls/sls_tracker.h | 9 ------- 5 files changed, 19 insertions(+), 28 deletions(-) diff --git a/src/tactic/sls/sls_compilation_settings.h b/src/tactic/sls/sls_compilation_settings.h index a649bc9ed..5c837b4b2 100644 --- a/src/tactic/sls/sls_compilation_settings.h +++ b/src/tactic/sls/sls_compilation_settings.h @@ -22,9 +22,6 @@ Notes: #ifndef _SLS_COMPILATION_SETTINGS_H_ #define _SLS_COMPILATION_SETTINGS_H_ -// shall we use addition/subtraction? -#define _USE_ADDSUB_ 1 - // should we use unsat-structures as done in SLS 4 SAT instead for random or bfs selection? #define _REAL_RS_ 0 diff --git a/src/tactic/sls/sls_engine.cpp b/src/tactic/sls/sls_engine.cpp index af8ae1df2..5d4df237e 100644 --- a/src/tactic/sls/sls_engine.cpp +++ b/src/tactic/sls/sls_engine.cpp @@ -61,6 +61,7 @@ void sls_engine::updt_params(params_ref const & _p) { m_walksat = p.walksat(); m_walksat_repick = p.walksat_repick(); m_paws_sp = p.paws_sp(); + m_paws = m_paws_sp < 1024; m_wp = p.wp(); m_vns_mc = p.vns_mc(); m_vns_repick = p.vns_repick(); @@ -173,7 +174,6 @@ bool sls_engine::what_if( // 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; best_const = fd_inx; m_mpz_manager.set(best_value, temp); @@ -244,16 +244,12 @@ void sls_engine::mk_random_move(ptr_vector & unsat_constants) 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 - move_type mt = MV_FLIP; -#endif unsigned bit = 0; switch (mt) @@ -308,8 +304,9 @@ double sls_engine::find_best_move( unsigned bv_sz; double new_score = score; - m_tracker.reset_equal_scores(); - + //unsigned offset = m_tracker.get_random_uint(16) % to_evaluate.size(); + //for (unsigned j = 0; j < to_evaluate.size(); j++) { + //unsigned i = (j + offset) % to_evaluate.size(); for (unsigned i = 0; i < to_evaluate.size(); i++) { func_decl * fd = to_evaluate[i]; sort * srt = fd->get_range(); @@ -328,7 +325,6 @@ double sls_engine::find_best_move( } 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); @@ -341,7 +337,6 @@ double sls_engine::find_best_move( 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 (what_if(fd, i, temp, new_score, best_const, best_value)) @@ -418,7 +413,7 @@ lbool sls_engine::search() { #if _REAL_RS_ //m_tracker.debug_real(g, m_stats.m_moves); #endif - + // get candidate variables ptr_vector & to_evaluate = m_tracker.get_unsat_constants(m_assertions); if (!to_evaluate.size()) { @@ -426,6 +421,7 @@ lbool sls_engine::search() { goto bailout; } + // random walk with probability wp / 1024 if (m_wp && m_tracker.get_random_uint(10) < m_wp) { mk_random_move(to_evaluate); @@ -436,14 +432,18 @@ lbool sls_engine::search() { old_score = score; new_const = (unsigned)-1; + // find best increasing move score = find_best_move(to_evaluate, score, new_const, new_value, new_bit, move); + // use Monte Carlo 2-bit-flip sampling if no increasing move was found previously if (m_vns_mc && (new_const == static_cast(-1))) score = find_best_move_mc(to_evaluate, score, new_const, new_value); + // repick assertion if no increasing move was found previously if (m_vns_repick && (new_const == static_cast(-1))) { expr * q = m_tracker.get_new_unsat_assertion(m_assertions); + // only apply if another unsatisfied assertion actually exists if (q) { ptr_vector & to_evaluate2 = m_tracker.get_unsat_constants_walksat(q); @@ -457,6 +457,7 @@ lbool sls_engine::search() { } } + // randomize if no increasing move was found if (new_const == static_cast(-1)) { score = old_score; if (m_walksat_repick) @@ -466,16 +467,19 @@ lbool sls_engine::search() { score = m_tracker.get_top_sum() / m_assertions.size(); - if (m_paws_sp < 1024) + // update assertion weights if a weigthing is enabled (sp < 1024) + if (m_paws) { for (unsigned i = 0; i < sz; i++) { expr * q = m_assertions[i]; + // smooth weights with probability sp / 1024 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); } + // increase weights otherwise else { if (m_mpz_manager.eq(m_tracker.get_value(q),m_zero)) @@ -484,6 +488,7 @@ lbool sls_engine::search() { } } } + // otherwise, apply most increasing move else { func_decl * fd = to_evaluate[new_const]; score = serious_score(fd, new_value); @@ -507,7 +512,6 @@ void sls_engine::operator()(goal_ref const & g, model_converter_ref & mc) { for (unsigned i = 0; i < g->size(); i++) assert_expr(g->form(i)); - verbose_stream() << "_USE_ADDSUB_ " << _USE_ADDSUB_ << std::endl; verbose_stream() << "_REAL_RS_ " << _REAL_RS_ << std::endl; verbose_stream() << "_EARLY_PRUNE_ " << _EARLY_PRUNE_ << std::endl; @@ -570,7 +574,7 @@ 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. + /* Andreas: My own scheme (= 1) seems to work best. Other schemes are disabled so that we save one parameter. I leave the other versions as comments in case you want to try it again somewhen. #if _RESTART_SCHEME_ == 5 m_restart_next += (unsigned)(m_restart_base * pow(_RESTART_CONST_ARMIN_, m_stats.m_restarts)); diff --git a/src/tactic/sls/sls_engine.h b/src/tactic/sls/sls_engine.h index ff0e55f24..94f3fa626 100644 --- a/src/tactic/sls/sls_engine.h +++ b/src/tactic/sls/sls_engine.h @@ -76,6 +76,7 @@ protected: unsigned m_wp; unsigned m_vns_mc; unsigned m_vns_repick; + unsigned m_paws; unsigned m_paws_sp; unsigned m_restart_base; unsigned m_restart_next; diff --git a/src/tactic/sls/sls_evaluator.h b/src/tactic/sls/sls_evaluator.h index 37bfa5a2d..200a0e380 100644 --- a/src/tactic/sls/sls_evaluator.h +++ b/src/tactic/sls/sls_evaluator.h @@ -37,9 +37,7 @@ class sls_evaluator { powers & m_powers; expr_ref_buffer m_temp_exprs; vector > m_traversal_stack; -#if _EARLY_PRUNE_ vector > m_traversal_stack_bool; -#endif public: sls_evaluator(ast_manager & m, bv_util & bvu, sls_tracker & t, unsynch_mpz_manager & mm, powers & p) : @@ -753,7 +751,7 @@ public: (*this)(to_app(cur), new_value); m_tracker.set_value(cur, new_value); - // should always have uplinks ... + // Andreas: Should actually always have uplinks ... if (m_tracker.has_uplinks(cur)) { ptr_vector & ups = m_tracker.get_uplinks(cur); for (unsigned j = 0; j < ups.size(); j++) { diff --git a/src/tactic/sls/sls_tracker.h b/src/tactic/sls/sls_tracker.h index 7b48057d4..a815c9ad3 100644 --- a/src/tactic/sls/sls_tracker.h +++ b/src/tactic/sls/sls_tracker.h @@ -92,7 +92,6 @@ private: #endif obj_map m_weights; double m_top_sum; - unsigned m_equal_scores; public: sls_tracker(ast_manager & m, bv_util & bvu, unsynch_mpz_manager & mm, powers & p) : @@ -148,14 +147,6 @@ public: return sum / count; } - void reset_equal_scores() { - m_equal_scores = 1; - } - - unsigned inc_equal_scores() { - return ++m_equal_scores; - } - inline void adapt_top_sum(expr * e, double add, double sub) { m_top_sum += m_weights.find(e) * (add - sub); } From 9ebfb119dbd87babb52bed8eb55eee5c061cbcba Mon Sep 17 00:00:00 2001 From: Andreas Froehlich Date: Wed, 23 Apr 2014 14:52:18 +0100 Subject: [PATCH 5/7] Moved parameters to the right file. Almost clean. --- src/tactic/sls/sls_compilation_settings.h | 5 +-- src/tactic/sls/sls_engine.cpp | 38 +++++++++++------------ src/tactic/sls/sls_engine.h | 3 +- src/tactic/sls/sls_evaluator.h | 5 --- src/tactic/sls/sls_params.pyg | 20 ++++++++++-- src/tactic/sls/sls_tracker.h | 33 +++++++++----------- 6 files changed, 52 insertions(+), 52 deletions(-) diff --git a/src/tactic/sls/sls_compilation_settings.h b/src/tactic/sls/sls_compilation_settings.h index 5c837b4b2..707802cf4 100644 --- a/src/tactic/sls/sls_compilation_settings.h +++ b/src/tactic/sls/sls_compilation_settings.h @@ -22,10 +22,7 @@ Notes: #ifndef _SLS_COMPILATION_SETTINGS_H_ #define _SLS_COMPILATION_SETTINGS_H_ -// should we use unsat-structures as done in SLS 4 SAT instead for random or bfs selection? +// should we use unsat-structures as done in SLS 4 SAT? #define _REAL_RS_ 0 -// shall we use early pruning for incremental update? -#define _EARLY_PRUNE_ 1 - #endif \ No newline at end of file diff --git a/src/tactic/sls/sls_engine.cpp b/src/tactic/sls/sls_engine.cpp index 5d4df237e..a1c72609c 100644 --- a/src/tactic/sls/sls_engine.cpp +++ b/src/tactic/sls/sls_engine.cpp @@ -70,6 +70,8 @@ void sls_engine::updt_params(params_ref const & _p) { m_restart_next = m_restart_base; m_restart_init = p.restart_init(); + m_early_prune = p.early_prune(); + // Andreas: Would cause trouble because repick requires an assertion being picked before which is not the case in GSAT. if (m_walksat_repick && !m_walksat) NOT_IMPLEMENTED_YET(); @@ -117,7 +119,7 @@ double sls_engine::top_score() { m_tracker.set_top_sum(top_sum); - return top_sum / (double)sz; + return top_sum; } double sls_engine::rescore() { @@ -129,21 +131,21 @@ double sls_engine::rescore() { double sls_engine::serious_score(func_decl * fd, const mpz & new_value) { m_evaluator.serious_update(fd, new_value); m_stats.m_incr_evals++; - return (m_tracker.get_top_sum() / m_assertions.size()); + return m_tracker.get_top_sum(); } double sls_engine::incremental_score(func_decl * fd, const mpz & new_value) { m_evaluator.update(fd, new_value); m_stats.m_incr_evals++; - return (m_tracker.get_top_sum() / m_assertions.size()); + return m_tracker.get_top_sum(); } 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)) - return (m_tracker.get_top_sum() / m_assertions.size()); + return m_tracker.get_top_sum(); else - return 0.0; + return -DBL_MAX; } // checks whether the score outcome of a given move is better than the previous score @@ -160,11 +162,11 @@ bool sls_engine::what_if( m_mpz_manager.set(old_value, m_tracker.get_value(fd)); #endif -#if _EARLY_PRUNE_ - double r = incremental_score_prune(fd, temp); -#else - double r = incremental_score(fd, temp); -#endif + double r; + if (m_early_prune) + r = incremental_score_prune(fd, temp); + else + r = incremental_score(fd, temp); #ifdef Z3DEBUG TRACE("sls_whatif", tout << "WHAT IF " << fd->get_name() << " WERE " << m_mpz_manager.to_string(temp) << " --> " << r << std::endl;); @@ -342,11 +344,8 @@ double sls_engine::find_best_move( if (what_if(fd, i, temp, new_score, best_const, best_value)) move = MV_INV; } - // reset to what it was before - double check = incremental_score(fd, old_value); - // Andreas: does not hold anymore now that we use top level score caching - //SASSERT(check == score); + incremental_score(fd, old_value); } m_mpz_manager.del(old_value); @@ -381,9 +380,8 @@ double sls_engine::find_best_move_mc(ptr_vector & to_evaluate, double } } } - // reset to what it was before - double check = incremental_score(fd, old_value); + incremental_score(fd, old_value); } m_mpz_manager.del(old_value); @@ -408,7 +406,10 @@ lbool sls_engine::search() { checkpoint(); m_stats.m_moves++; if (m_stats.m_moves % m_restart_base == 0) + { m_tracker.ucb_forget(m_assertions); + //score = rescore(); + } #if _REAL_RS_ //m_tracker.debug_real(g, m_stats.m_moves); @@ -425,7 +426,7 @@ lbool sls_engine::search() { if (m_wp && m_tracker.get_random_uint(10) < m_wp) { mk_random_move(to_evaluate); - score = m_tracker.get_top_sum() / sz; + score = m_tracker.get_top_sum(); continue; } @@ -465,7 +466,7 @@ lbool sls_engine::search() { else m_evaluator.randomize_local(to_evaluate); - score = m_tracker.get_top_sum() / m_assertions.size(); + score = m_tracker.get_top_sum(); // update assertion weights if a weigthing is enabled (sp < 1024) if (m_paws) @@ -513,7 +514,6 @@ void sls_engine::operator()(goal_ref const & g, model_converter_ref & mc) { assert_expr(g->form(i)); verbose_stream() << "_REAL_RS_ " << _REAL_RS_ << std::endl; - verbose_stream() << "_EARLY_PRUNE_ " << _EARLY_PRUNE_ << std::endl; lbool res = operator()(); diff --git a/src/tactic/sls/sls_engine.h b/src/tactic/sls/sls_engine.h index 94f3fa626..ac8610871 100644 --- a/src/tactic/sls/sls_engine.h +++ b/src/tactic/sls/sls_engine.h @@ -81,8 +81,7 @@ protected: unsigned m_restart_base; unsigned m_restart_next; unsigned m_restart_init; - - ptr_vector m_old_values; + unsigned m_early_prune; typedef enum { MV_FLIP = 0, MV_INC, MV_DEC, MV_INV } move_type; diff --git a/src/tactic/sls/sls_evaluator.h b/src/tactic/sls/sls_evaluator.h index 200a0e380..e4cf3c466 100644 --- a/src/tactic/sls/sls_evaluator.h +++ b/src/tactic/sls/sls_evaluator.h @@ -554,9 +554,7 @@ public: 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_ m_tracker.set_score_prune(cur, new_score); -#endif if (m_tracker.has_uplinks(cur)) { ptr_vector & ups = m_tracker.get_uplinks(cur); @@ -599,9 +597,6 @@ public: 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_ - m_tracker.set_score_prune(cur, new_score); -#endif if (m_tracker.has_uplinks(cur)) { ptr_vector & ups = m_tracker.get_uplinks(cur); for (unsigned j = 0; j < ups.size(); j++) { diff --git a/src/tactic/sls/sls_params.pyg b/src/tactic/sls/sls_params.pyg index cc3e05966..98875b20d 100644 --- a/src/tactic/sls/sls_params.pyg +++ b/src/tactic/sls/sls_params.pyg @@ -2,7 +2,21 @@ def_module_params('sls', export=True, description='Experimental Stochastic Local Search Solver (for QFBV only).', params=(max_memory_param(), - ('restarts', UINT, UINT_MAX, '(max) number of restarts'), - ('plateau_limit', UINT, 10, 'pleateau limit'), - ('random_seed', UINT, 0, 'random seed') + ('max_restarts', UINT, UINT_MAX, 'maximum number of restarts'), + ('walksat', BOOL, 1, 'use walksat assertion selection (instead of gsat)'), + ('walksat_ucb', BOOL, 1, 'use bandit heuristic for walksat assertion selection (instead of random)'), + ('walksat_ucb_constant', DOUBLE, 20.0, 'the ucb constant c in the term score + c * f(touched)'), + ('walksat_ucb_init', BOOL, 0, 'initialize total ucb touched to formula size'), + ('walksat_ucb_forget', DOUBLE, 1.0, 'scale touched by this factor every base restart interval'), + ('walksat_repick', BOOL, 1, 'repick assertion if randomizing in local minima'), + ('scale_unsat', DOUBLE, 0.5, 'scale score of unsat expressions by this factor'), + ('paws_init', UINT, 40, 'initial/minimum assertion weights'), + ('paws_sp', UINT, 52, 'smooth assertion weights with probability paws_sp / 1024'), + ('wp', UINT, 0, 'random walk with probability wp / 1024'), + ('vns_mc', UINT, 0, 'in local minima, try Monte Carlo sampling vns_mc many 2-bit-flips per bit'), + ('vns_repick', BOOL, 0, 'in local minima, try picking a different assertion (only for walksat)'), + ('restart_base', UINT, 100, 'base restart interval given by moves per run'), + ('restart_init', BOOL, 0, 'initialize to 0 or random value (= 1) after restart'), + ('early_prune', BOOL, 1, 'use early pruning for score prediction'), + ('random_seed', UINT, 0, 'random seed') )) diff --git a/src/tactic/sls/sls_tracker.h b/src/tactic/sls/sls_tracker.h index a815c9ad3..507596273 100644 --- a/src/tactic/sls/sls_tracker.h +++ b/src/tactic/sls/sls_tracker.h @@ -44,11 +44,9 @@ class sls_tracker { unsynch_mpz_manager * m; mpz value; double score; -#if _EARLY_PRUNE_ double score_prune; unsigned has_pos_occ; unsigned has_neg_occ; -#endif unsigned distance; // max distance from any root unsigned touched; value_score & operator=(const value_score & other) { @@ -122,6 +120,7 @@ public: m_paws_init = p.paws_init(); } + /* Andreas: Tried to give some measure for the formula size by the following two methods but both are not used currently. unsigned get_formula_size() { return m_scores.size(); } @@ -145,7 +144,7 @@ public: } return sum / count; - } + }*/ inline void adapt_top_sum(expr * e, double add, double sub) { m_top_sum += m_weights.find(e) * (add - sub); @@ -417,6 +416,8 @@ public: } } + /* Andreas: Used this at some point to have values for the non-top-level expressions. + However, it did not give better performance but even cause some additional m/o - is not used currently. void initialize_recursive(init_proc proc, expr_mark visited, expr * e) { if (m_manager.is_and(e) || m_manager.is_or(e)) { app * a = to_app(e); @@ -445,7 +446,7 @@ public: find_func_decls_proc ffd_proc(m_manager, m_constants_occ.find(e)); expr_fast_mark1 visited; quick_for_each_expr(ffd_proc, visited, e); - } + }*/ void initialize(ptr_vector const & as) { init_proc proc(m_manager, *this); @@ -455,8 +456,6 @@ public: expr * e = as[i]; if (!m_top_expr.contains(e)) m_top_expr.insert(e); - else - printf("this is already in ...\n"); for_each_expr(proc, visited, e); } @@ -464,7 +463,6 @@ public: for (unsigned i = 0; i < sz; i++) { expr * e = as[i]; - // Andreas: Maybe not fully correct. 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)); @@ -488,15 +486,16 @@ public: for (unsigned i = 0; i < sz; i++) { expr * e = as[i]; - if (!m_weights.contains(e)) + + // initialize weights + if (!m_weights.contains(e)) m_weights.insert(e, m_paws_init); + + // positive/negative occurences used for early pruning + setup_occs(as[i]); } -#if _EARLY_PRUNE_ - for (unsigned i = 0; i < sz; i++) - setup_occs(as[i]); -#endif - + // initialize ucb total touched value (individual ones are always initialized to 1) m_touched = m_ucb_init ? as.size() : 1; } @@ -738,7 +737,6 @@ public: 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. double max = 0.0; for (unsigned i = 0; i < a->get_num_args(); i++) { double cur = get_score(args[i]); @@ -764,7 +762,6 @@ public: const mpz & v1 = get_value(arg1); if (negated) { - //res = (m_mpz_manager.eq(v0, v1)) ? 0.5 * (m_bv_util.get_bv_size(arg0) - 1.0) / m_bv_util.get_bv_size(arg0) : 1.0; res = (m_mpz_manager.eq(v0, v1)) ? 0.0 : 1.0; TRACE("sls_score", tout << "V0 = " << m_mpz_manager.to_string(v0) << " ; V1 = " << m_mpz_manager.to_string(v1) << std::endl; ); @@ -1051,10 +1048,8 @@ public: // for (unsigned i = 0; i < m_where_false.size(); i++) { // expr * e = m_list_false[i]; vscore = m_scores.find(e); - double q = vscore.score + m_ucb_constant * sqrt(log((double)m_touched) / vscore.touched); -#if _UCT_ == 3 - double q = vscore.score + _UCT_CONSTANT_ * sqrt(log(m_touched)/vscore.touched) + (get_random_uint(16) * 0.1 / (2<<16)); -#endif + //double q = vscore.score + m_ucb_constant * sqrt(log((double)m_touched) / vscore.touched); + double q = vscore.score + m_ucb_constant * sqrt(log((double)m_touched) / vscore.touched) + (get_random_uint(8) * 0.0000002); if (q > max && m_mpz_manager.neq(get_value(e), m_one) ) { max = q; pos = i; } } if (pos == static_cast(-1)) From 3df2967be92549427ad1410c41f37c80df8e3726 Mon Sep 17 00:00:00 2001 From: Andreas Froehlich Date: Fri, 25 Apr 2014 13:56:15 +0100 Subject: [PATCH 6/7] Cleaned up final SLS version. Enjoy! --- src/tactic/sls/sls_compilation_settings.h | 28 ---- src/tactic/sls/sls_engine.cpp | 43 ++++-- src/tactic/sls/sls_engine.h | 2 + src/tactic/sls/sls_evaluator.h | 8 +- src/tactic/sls/sls_params.pyg | 6 +- src/tactic/sls/sls_tracker.h | 153 ++++++++-------------- 6 files changed, 94 insertions(+), 146 deletions(-) diff --git a/src/tactic/sls/sls_compilation_settings.h b/src/tactic/sls/sls_compilation_settings.h index 707802cf4..e69de29bb 100644 --- a/src/tactic/sls/sls_compilation_settings.h +++ b/src/tactic/sls/sls_compilation_settings.h @@ -1,28 +0,0 @@ -/*++ -Copyright (c) 2014 Microsoft Corporation - -Module Name: - - sls_compilation_constants.h - -Abstract: - - Stochastic Local Search (SLS) compilation constants - -Author: - - Christoph (cwinter) 2014-03-19 - -Notes: - - This file should go away completely once we have evaluated all options. - ---*/ - -#ifndef _SLS_COMPILATION_SETTINGS_H_ -#define _SLS_COMPILATION_SETTINGS_H_ - -// should we use unsat-structures as done in SLS 4 SAT? -#define _REAL_RS_ 0 - -#endif \ No newline at end of file diff --git a/src/tactic/sls/sls_engine.cpp b/src/tactic/sls/sls_engine.cpp index a1c72609c..269790902 100644 --- a/src/tactic/sls/sls_engine.cpp +++ b/src/tactic/sls/sls_engine.cpp @@ -71,6 +71,8 @@ void sls_engine::updt_params(params_ref const & _p) { m_restart_init = p.restart_init(); m_early_prune = p.early_prune(); + m_random_offset = p.random_offset(); + m_rescore = p.rescore(); // Andreas: Would cause trouble because repick requires an assertion being picked before which is not the case in GSAT. if (m_walksat_repick && !m_walksat) @@ -174,6 +176,9 @@ bool sls_engine::what_if( m_mpz_manager.del(old_value); #endif + // Andreas: Had this idea on my last day. Maybe we could add a noise here similar to the one that worked so well for ucb assertion selection. + // r += 0.0001 * m_tracker.get_random_uint(8); + // Andreas: For some reason it is important to use > here instead of >=. Probably related to prefering the LSB. if (r > best_score) { best_score = r; @@ -248,9 +253,15 @@ void sls_engine::mk_random_move(ptr_vector & unsat_constants) { if (m_mpz_manager.is_one(m_tracker.get_random_bool())) rnd_mv = 2; if (m_mpz_manager.is_one(m_tracker.get_random_bool())) rnd_mv++; + + // Andreas: The other option would be to scale the probability for flips according to the bit-width. + /* unsigned bv_sz2 = m_bv_util.get_bv_size(srt); + rnd_mv = m_tracker.get_random_uint(16) % (bv_sz2 + 3); + if (rnd_mv > 3) rnd_mv = 0; */ + move_type mt = (move_type)rnd_mv; - // inversion doesn't make sense, let's do a flip instead. + // Andreas: Christoph claimed inversion doesn't make sense, let's do a flip instead. Is this really true? if (mt == MV_INV) mt = MV_FLIP; unsigned bit = 0; @@ -306,10 +317,13 @@ double sls_engine::find_best_move( unsigned bv_sz; double new_score = score; - //unsigned offset = m_tracker.get_random_uint(16) % to_evaluate.size(); - //for (unsigned j = 0; j < to_evaluate.size(); j++) { - //unsigned i = (j + offset) % to_evaluate.size(); - for (unsigned i = 0; i < to_evaluate.size(); i++) { + // Andreas: Introducting a bit of randomization by using a random offset and a random direction to go through the candidate list. + unsigned sz = to_evaluate.size(); + unsigned offset = (m_random_offset) ? m_tracker.get_random_uint(16) % sz : 0; + for (unsigned j = 0; j < sz; j++) { + unsigned i = j + offset; + if (i >= sz) i -= sz; + //for (unsigned i = 0; i < to_evaluate.size(); i++) { func_decl * fd = to_evaluate[i]; sort * srt = fd->get_range(); bv_sz = (m_manager.is_bool(srt)) ? 1 : m_bv_util.get_bv_size(srt); @@ -361,7 +375,13 @@ double sls_engine::find_best_move_mc(ptr_vector & to_evaluate, double unsigned bv_sz; double new_score = score; - for (unsigned i = 0; i < to_evaluate.size(); i++) { + // Andreas: Introducting a bit of randomization by using a random offset and a random direction to go through the candidate list. + unsigned sz = to_evaluate.size(); + unsigned offset = (m_random_offset) ? m_tracker.get_random_uint(16) % sz : 0; + for (unsigned j = 0; j < sz; j++) { + unsigned i = j + offset; + if (i >= sz) i -= sz; + //for (unsigned i = 0; i < to_evaluate.size(); i++) { func_decl * fd = to_evaluate[i]; sort * srt = fd->get_range(); bv_sz = (m_manager.is_bool(srt)) ? 1 : m_bv_util.get_bv_size(srt); @@ -405,15 +425,16 @@ lbool sls_engine::search() { while (check_restart(m_stats.m_moves)) { checkpoint(); m_stats.m_moves++; + + // Andreas: Every base restart interval ... if (m_stats.m_moves % m_restart_base == 0) { + // ... potentially smooth the touched counters ... m_tracker.ucb_forget(m_assertions); - //score = rescore(); + // ... or normalize the top-level score. + if (m_rescore) score = rescore(); } -#if _REAL_RS_ - //m_tracker.debug_real(g, m_stats.m_moves); -#endif // get candidate variables ptr_vector & to_evaluate = m_tracker.get_unsat_constants(m_assertions); if (!to_evaluate.size()) @@ -513,8 +534,6 @@ void sls_engine::operator()(goal_ref const & g, model_converter_ref & mc) { for (unsigned i = 0; i < g->size(); i++) assert_expr(g->form(i)); - verbose_stream() << "_REAL_RS_ " << _REAL_RS_ << std::endl; - lbool res = operator()(); if (res == l_true) { diff --git a/src/tactic/sls/sls_engine.h b/src/tactic/sls/sls_engine.h index ac8610871..8158808fa 100644 --- a/src/tactic/sls/sls_engine.h +++ b/src/tactic/sls/sls_engine.h @@ -82,6 +82,8 @@ protected: unsigned m_restart_next; unsigned m_restart_init; unsigned m_early_prune; + unsigned m_random_offset; + unsigned m_rescore; typedef enum { MV_FLIP = 0, MV_INC, MV_DEC, MV_INV } move_type; diff --git a/src/tactic/sls/sls_evaluator.h b/src/tactic/sls/sls_evaluator.h index e4cf3c466..61afb7457 100644 --- a/src/tactic/sls/sls_evaluator.h +++ b/src/tactic/sls/sls_evaluator.h @@ -22,7 +22,6 @@ Notes: #include"model_evaluator.h" -#include"sls_compilation_settings.h" #include"sls_powers.h" #include"sls_tracker.h" @@ -540,19 +539,16 @@ public: (*this)(to_app(cur), new_value); m_tracker.set_value(cur, new_value); -#if _REAL_RS_ + new_score = m_tracker.score(cur); if (m_tracker.is_top_expr(cur)) { + m_tracker.adapt_top_sum(cur, new_score, m_tracker.get_score(cur)); if (m_mpz_manager.eq(new_value,m_one)) m_tracker.make_assertion(cur); else m_tracker.break_assertion(cur); } -#endif - new_score = m_tracker.score(cur); - if (m_tracker.is_top_expr(cur)) - m_tracker.adapt_top_sum(cur, new_score, m_tracker.get_score(cur)); m_tracker.set_score(cur, new_score); m_tracker.set_score_prune(cur, new_score); diff --git a/src/tactic/sls/sls_params.pyg b/src/tactic/sls/sls_params.pyg index 98875b20d..ad7a22675 100644 --- a/src/tactic/sls/sls_params.pyg +++ b/src/tactic/sls/sls_params.pyg @@ -8,15 +8,19 @@ def_module_params('sls', ('walksat_ucb_constant', DOUBLE, 20.0, 'the ucb constant c in the term score + c * f(touched)'), ('walksat_ucb_init', BOOL, 0, 'initialize total ucb touched to formula size'), ('walksat_ucb_forget', DOUBLE, 1.0, 'scale touched by this factor every base restart interval'), + ('walksat_ucb_noise', DOUBLE, 0.0002, 'add noise 0 <= 256 * ucb_noise to ucb score for assertion selection'), ('walksat_repick', BOOL, 1, 'repick assertion if randomizing in local minima'), ('scale_unsat', DOUBLE, 0.5, 'scale score of unsat expressions by this factor'), ('paws_init', UINT, 40, 'initial/minimum assertion weights'), ('paws_sp', UINT, 52, 'smooth assertion weights with probability paws_sp / 1024'), - ('wp', UINT, 0, 'random walk with probability wp / 1024'), + ('wp', UINT, 100, 'random walk with probability wp / 1024'), ('vns_mc', UINT, 0, 'in local minima, try Monte Carlo sampling vns_mc many 2-bit-flips per bit'), ('vns_repick', BOOL, 0, 'in local minima, try picking a different assertion (only for walksat)'), ('restart_base', UINT, 100, 'base restart interval given by moves per run'), ('restart_init', BOOL, 0, 'initialize to 0 or random value (= 1) after restart'), ('early_prune', BOOL, 1, 'use early pruning for score prediction'), + ('random_offset', BOOL, 1, 'use random offset vor candidate evaluation'), + ('rescore', BOOL, 1, 'rescore/normalize top-level score every base restart interval'), + ('track_unsat', BOOL, 0, 'keep a list of unsat assertions as done in SAT - currently disabled internally'), ('random_seed', UINT, 0, 'random seed') )) diff --git a/src/tactic/sls/sls_tracker.h b/src/tactic/sls/sls_tracker.h index 507596273..4356bcc9b 100644 --- a/src/tactic/sls/sls_tracker.h +++ b/src/tactic/sls/sls_tracker.h @@ -80,14 +80,13 @@ private: double m_ucb_constant; unsigned m_ucb_init; double m_ucb_forget; + double m_ucb_noise; unsigned m_touched; double m_scale_unsat; unsigned m_paws_init; -#if _REAL_RS_ - ptr_vector m_unsat_expr; obj_map m_where_false; expr** m_list_false; -#endif + unsigned m_track_unsat; obj_map m_weights; double m_top_sum; @@ -116,8 +115,12 @@ public: m_ucb_constant = p.walksat_ucb_constant(); m_ucb_init = p.walksat_ucb_init(); m_ucb_forget = p.walksat_ucb_forget(); + m_ucb_noise = p.walksat_ucb_noise(); m_scale_unsat = p.scale_unsat(); m_paws_init = p.paws_init(); + // Andreas: track_unsat is currently disabled because I cannot guarantee that it is not buggy. + // If you want to use it, you will also need to change comments in the assertion selection. + m_track_unsat = 0;//p.track_unsat(); } /* Andreas: Tried to give some measure for the formula size by the following two methods but both are not used currently. @@ -254,53 +257,6 @@ public: return m_uplinks.find(n); } -#if _REAL_RS_ - void debug_real(goal_ref const & g, unsigned flip) - { - unsigned count = 0; - for (unsigned i = 0; i < g->size(); i++) - { - expr * e = g->form(i); - if (m_mpz_manager.eq(get_value(e),m_one) && m_where_false.contains(e)) - { - printf("iteration %d: ", flip); - printf("form %d is sat but in unsat list at position %d of %d\n", i, m_where_false.find(e), m_where_false.size()); - exit(4); - } - - if (m_mpz_manager.eq(get_value(e),m_zero) && !m_where_false.contains(e)) - { - printf("iteration %d: ", flip); - printf("form %d is unsat but not in unsat list\n", i); - exit(4); - } - - if (m_mpz_manager.eq(get_value(e),m_zero) && m_where_false.contains(e)) - { - unsigned pos = m_where_false.find(e); - expr * q = m_list_false[pos]; - if (q != e) - { - printf("iteration %d: ", flip); - printf("form %d is supposed to be at pos %d in unsat list but something else was there\n", i, pos); - exit(4); - } - } - - if (m_mpz_manager.eq(get_value(e),m_zero)) - count++; - } - - // should be true now that duplicate assertions are removed - if (count != m_where_false.size()) - { - printf("iteration %d: ", flip); - printf("%d are unsat but list is of size %d\n", count, m_where_false.size()); - exit(4); - } - } -#endif - inline void ucb_forget(ptr_vector & as) { if (m_ucb_forget < 1.0) { @@ -474,14 +430,15 @@ public: TRACE("sls", tout << "Initial model:" << std::endl; show_model(tout); ); -#if _REAL_RS_ - m_list_false = new expr*[sz]; - //for (unsigned i = 0; i < sz; i++) - //{ - // if (m_mpz_manager.eq(get_value(g->form(i)),m_zero)) - // break_assertion(g->form(i)); - //} -#endif + if (m_track_unsat) + { + m_list_false = new expr*[sz]; + for (unsigned i = 0; i < sz; i++) + { + if (m_mpz_manager.eq(get_value(as[i]), m_zero)) + break_assertion(as[i]); + } + } for (unsigned i = 0; i < sz; i++) { @@ -515,44 +472,36 @@ public: return m_weights.find(e); } -#if _REAL_RS_ void make_assertion(expr * e) { - if (m_where_false.contains(e)) + if (m_track_unsat) { - unsigned pos = m_where_false.find(e); - m_where_false.erase(e); - if (pos != m_where_false.size()) + if (m_where_false.contains(e)) { - expr * q = m_list_false[m_where_false.size()]; - m_list_false[pos] = q; - m_where_false.find(q) = pos; - //printf("Moving %d from %d to %d\n", q, m_where_false.size(), pos); + unsigned pos = m_where_false.find(e); + m_where_false.erase(e); + if (pos != m_where_false.size()) + { + expr * q = m_list_false[m_where_false.size()]; + m_list_false[pos] = q; + m_where_false.find(q) = pos; + } } - //else - //printf("Erasing %d from %d to %d\n", e, pos); -// m_list_false[m_where_false.size()] = 0; -// printf("Going in %d\n", m_where_false.size()); } - //if (m_unsat_expr.contains(e)) - //m_unsat_expr.erase(e); } void break_assertion(expr * e) { - //printf("I'm broken... that's still fine.\n"); - if (!m_where_false.contains(e)) + if (m_track_unsat) { - //printf("This however is not so cool...\n"); - unsigned pos = m_where_false.size(); - m_list_false[pos] = e; - m_where_false.insert(e, pos); - // printf("Going in %d\n", m_where_false.size()); + if (!m_where_false.contains(e)) + { + unsigned pos = m_where_false.size(); + m_list_false[pos] = e; + m_where_false.insert(e, pos); + } } - //if (!m_unsat_expr.contains(e)) - //m_unsat_expr.push_back(e); } -#endif void show_model(std::ostream & out) { unsigned sz = get_num_constants(); @@ -1043,24 +992,38 @@ public: { value_score vscore; double max = -1.0; + // Andreas: Commented things here might be used for track_unsat data structures as done in SLS for SAT. But seems to have no benefit. + /* for (unsigned i = 0; i < m_where_false.size(); i++) { + expr * e = m_list_false[i]; */ for (unsigned i = 0; i < sz; i++) { expr * e = as[i]; -// for (unsigned i = 0; i < m_where_false.size(); i++) { -// expr * e = m_list_false[i]; - vscore = m_scores.find(e); - //double q = vscore.score + m_ucb_constant * sqrt(log((double)m_touched) / vscore.touched); - double q = vscore.score + m_ucb_constant * sqrt(log((double)m_touched) / vscore.touched) + (get_random_uint(8) * 0.0000002); - if (q > max && m_mpz_manager.neq(get_value(e), m_one) ) { max = q; pos = i; } + if (m_mpz_manager.neq(get_value(e), m_one)) + { + vscore = m_scores.find(e); + // Andreas: Select the assertion with the greatest ucb score. Potentially add some noise. + // double q = vscore.score + m_ucb_constant * sqrt(log((double)m_touched) / vscore.touched); + double q = vscore.score + m_ucb_constant * sqrt(log((double)m_touched) / vscore.touched) + m_ucb_noise * get_random_uint(8); + if (q > max) { max = q; pos = i; } + } } if (pos == static_cast(-1)) return 0; - m_scores.find(as[pos]).touched++; m_touched++; -// return m_list_false[pos]; + m_scores.find(as[pos]).touched++; + // Andreas: Also part of track_unsat data structures. Additionally disable the previous line! + /* m_last_pos = pos; + m_scores.find(m_list_false[pos]).touched++; + return m_list_false[pos]; */ } else { + // Andreas: The track_unsat data structures for random assertion selection. + /* sz = m_where_false.size(); + if (sz == 0) + return 0; + return m_list_false[get_random_uint(16) % sz]; */ + unsigned cnt_unsat = 0; for (unsigned i = 0; i < sz; i++) if (m_mpz_manager.neq(get_value(as[i]), m_one) && (get_random_uint(16) % ++cnt_unsat == 0)) pos = i; @@ -1070,14 +1033,6 @@ public: m_last_pos = pos; return as[pos]; -#if _REAL_RS_ - //unsigned pos = m_false_list[get_random_uint(16) % m_cnt_false]; - //expr * e = m_unsat_expr[get_random_uint(16) % m_unsat_expr.size()]; - sz = m_where_false.size(); - if (sz == 0) - return 0; - return m_list_false[get_random_uint(16) % sz]; -#endif } expr * get_new_unsat_assertion(ptr_vector const & as) { From a3f20774a8538eeec48191ae474ae2416750527c Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Fri, 25 Apr 2014 17:17:47 +0100 Subject: [PATCH 7/7] BVSLS comments Signed-off-by: Christoph M. Wintersteiger --- src/tactic/sls/sls_params.pyg | 2 +- src/tactic/sls/sls_tracker.h | 4 +++- 2 files changed, 4 insertions(+), 2 deletions(-) diff --git a/src/tactic/sls/sls_params.pyg b/src/tactic/sls/sls_params.pyg index ad7a22675..bf5bd181a 100644 --- a/src/tactic/sls/sls_params.pyg +++ b/src/tactic/sls/sls_params.pyg @@ -19,7 +19,7 @@ def_module_params('sls', ('restart_base', UINT, 100, 'base restart interval given by moves per run'), ('restart_init', BOOL, 0, 'initialize to 0 or random value (= 1) after restart'), ('early_prune', BOOL, 1, 'use early pruning for score prediction'), - ('random_offset', BOOL, 1, 'use random offset vor candidate evaluation'), + ('random_offset', BOOL, 1, 'use random offset for candidate evaluation'), ('rescore', BOOL, 1, 'rescore/normalize top-level score every base restart interval'), ('track_unsat', BOOL, 0, 'keep a list of unsat assertions as done in SAT - currently disabled internally'), ('random_seed', UINT, 0, 'random seed') diff --git a/src/tactic/sls/sls_tracker.h b/src/tactic/sls/sls_tracker.h index 4356bcc9b..d58f94af2 100644 --- a/src/tactic/sls/sls_tracker.h +++ b/src/tactic/sls/sls_tracker.h @@ -831,7 +831,9 @@ public: app * a = to_app(n); SASSERT(a->get_num_args() == 1); expr * child = a->get_arg(0); - if (m_manager.is_and(child) || m_manager.is_or(child)) // Precondition: Assertion set is in NNF. + // Precondition: Assertion set is in NNF. + // Also: careful about the unsat assertion scaling further down. + if (m_manager.is_and(child) || m_manager.is_or(child)) NOT_IMPLEMENTED_YET(); res = score_bool(child, true); }