diff --git a/src/tactic/sls/sls_evaluator.h b/src/tactic/sls/sls_evaluator.h index cdb08038f..696d7664a 100644 --- a/src/tactic/sls/sls_evaluator.h +++ b/src/tactic/sls/sls_evaluator.h @@ -78,7 +78,11 @@ 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; } @@ -86,7 +90,11 @@ 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; } @@ -94,9 +102,16 @@ 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); + m_mpz_manager.set(result, (m_mpz_manager.is_zero(child)) ? m_one : m_zero); +#endif break; } case OP_EQ: { @@ -542,7 +557,8 @@ public: m_tracker.set_value(cur, new_value); #if _REAL_RS_ || _REAL_PBFS_ - if (!m_tracker.has_uplinks(cur)) + //if (!m_tracker.has_uplinks(cur)) + if (m_tracker.is_top_expr(cur)) { if (m_mpz_manager.eq(new_value,m_one)) m_tracker.make_assertion(cur); @@ -554,7 +570,8 @@ public: #if _EARLY_PRUNE_ new_score = m_tracker.score(cur); #if _CACHE_TOP_SCORE_ - if (!m_tracker.has_uplinks(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)); #endif m_tracker.set_score(cur, new_score); @@ -562,13 +579,14 @@ public: #else #if _CACHE_TOP_SCORE_ new_score = m_tracker.score(cur); - if (!m_tracker.has_uplinks(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.set_score(cur, new_score); #else m_tracker.set_score(cur, m_tracker.score(cur)); #endif -#endif +#endif if (m_tracker.has_uplinks(cur)) { ptr_vector & ups = m_tracker.get_uplinks(cur); for (unsigned j = 0; j < ups.size(); j++) { @@ -611,7 +629,8 @@ public: #if _EARLY_PRUNE_ new_score = m_tracker.score(cur); #if _CACHE_TOP_SCORE_ - if (!m_tracker.has_uplinks(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)); #endif m_tracker.set_score(cur, new_score); @@ -619,13 +638,14 @@ public: #else #if _CACHE_TOP_SCORE_ new_score = m_tracker.score(cur); - if (!m_tracker.has_uplinks(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.set_score(cur, new_score); #else m_tracker.set_score(cur, m_tracker.score(cur)); #endif -#endif +#endif if (m_tracker.has_uplinks(cur)) { ptr_vector & ups = m_tracker.get_uplinks(cur); for (unsigned j = 0; j < ups.size(); j++) { @@ -695,7 +715,7 @@ public: double prune_score, new_score; unsigned pot_benefits = 0; - SASSERT(cur_depth < m_traversal_stack_bool.size()); + SASSERT(cur_depth < m_traversal_stack_bool.size()); ptr_vector & cur_depth_exprs = m_traversal_stack_bool[cur_depth]; @@ -704,7 +724,8 @@ public: new_score = m_tracker.score(cur); #if _CACHE_TOP_SCORE_ - if (!m_tracker.has_uplinks(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)); #endif prune_score = m_tracker.get_score_prune(cur); @@ -745,7 +766,8 @@ public: #if _CACHE_TOP_SCORE_ new_score = m_tracker.score(cur); - if (!m_tracker.has_uplinks(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.set_score(cur, new_score); #else @@ -833,44 +855,7 @@ public: } #endif - void randomize_local(expr * e, unsigned int flip) { - ptr_vector & unsat_constants = m_tracker.get_constants(e); - - // Randomize _one_ candidate: - unsigned r = m_tracker.get_random_uint(16) % unsat_constants.size(); - func_decl * fd = unsat_constants[r]; -#if _PERC_CHANGE_ - sort * srt = fd->get_range(); - mpz temp; - - if (m_manager.is_bool(srt)) - m_mpz_manager.set(temp, (m_mpz_manager.is_zero(m_tracker.get_value(fd))) ? m_one : m_zero); - else - { - mpz temp2, mask; - unsigned bv_sz = m_bv_util.get_bv_size(srt); - m_mpz_manager.set(temp, m_tracker.get_value(fd)); - - for (unsigned bit = 0; bit < bv_sz; bit++) - if (m_tracker.get_random_uint(16) % 100 < _PERC_CHANGE_) - { - m_mpz_manager.set(mask, m_powers(bit)); - m_mpz_manager.bitwise_xor(temp, mask, temp2); - m_mpz_manager.set(temp, temp2); - } - m_mpz_manager.del(mask); - m_mpz_manager.del(temp2); - } -#else - mpz temp = m_tracker.get_random(fd->get_range()); -#endif - update(fd, temp); - m_mpz_manager.del(temp); - } - - void randomize_local(goal_ref const & g, unsigned int flip) { - ptr_vector & unsat_constants = m_tracker.get_unsat_constants(g, flip); - + void randomize_local(ptr_vector & unsat_constants) { // Randomize _all_ candidates: //// bool did_something = false; @@ -927,6 +912,15 @@ public: tout << "Randomization candidate: " << unsat_constants[r]->get_name() << std::endl; tout << "Locally randomized model: " << std::endl; m_tracker.show_model(tout); ); + + } + + void randomize_local(expr * e) { + randomize_local(m_tracker.get_constants(e)); + } + + void randomize_local(goal_ref const & g, unsigned int flip) { + randomize_local(m_tracker.get_unsat_constants(g, flip)); } }; diff --git a/src/tactic/sls/sls_tactic.cpp b/src/tactic/sls/sls_tactic.cpp index 553acc35a..ada0ec359 100644 --- a/src/tactic/sls/sls_tactic.cpp +++ b/src/tactic/sls/sls_tactic.cpp @@ -34,6 +34,8 @@ Notes: #include"propagate_values_tactic.h" #include"sls_tactic.h" #include"nnf_tactic.h" +#include"luby.h" +#include "ctx_simplify_tactic.h" // which unsatisfied assertion is selected? only works with _FOCUS_ > 0 // 0 = random, 1 = #moves, 2 = assertion with min score, 3 = assertion with max score @@ -43,9 +45,23 @@ Notes: // 0 = all terms (GSAT), 1 = only one top level assertion (WSAT), 2 = only one bottom level atom #define _FOCUS_ 1 +// probability of choosing the same assertion again in the next step +#define _PERC_STICKY_ 0 + +// do we use dirty unit propagation to get rid of nested top level assertions? +#define _DIRTY_UP_ 0 + // do we use restarts? -// 0 = no, otherwise the value defines the maximum number of moves -#define _RESTARTS_ 0 +// 0 = no, 1 = use #moves, 2 = use #plateaus, 3 = use time +#define _RESTARTS_ 3 +// limit of moves/plateaus/seconds until first restart occurs +#define _RESTART_LIMIT_ 10 +// 0 = initialize with all zero, 1 initialize with random value +#define _RESTART_INIT_ 0 +// 0 = even intervals, 1 = pseudo luby, 2 = real luby, 3 = armin, 4 = rapid +#define _RESTART_SCHEME_ 1 +// base value c for armin restart scheme using c^inner - only applies for _RESTART_SCHEME_ 3 +#define _RESTART_CONST_ARMIN_ 3.0 // timelimit #define _TIMELIMIT_ 3600 @@ -66,38 +82,58 @@ Notes: // 2 = yes, by squaring it // 3 = yes, by setting it to zero // 4 = by progessively increasing weight (_TIMELIMIT_ needs to be set appropriately!) -#define _WEIGHT_DIST_ 0 +#define _WEIGHT_DIST_ 1 // the factor used for _WEIGHT_DIST_ = 1 #define _WEIGHT_DIST_FACTOR_ 0.25 +// shall we toggle the weight after each restart? +#define _WEIGHT_TOGGLE_ 0 + // do we use intensification steps in local minima? if so, how many? #define _INTENSIFICATION_ 0 #define _INTENSIFICATION_TRIES_ 0 +// what is the percentage of random moves in plateaus (instead of full randomization)? +#define _PERC_PLATEAU_MOVES_ 0 + +// shall we repick clause when randomizing in a plateau or use the current one? +#define _REPICK_ 1 + // do we use some UCT-like scheme for assertion-selection? overrides _BFS_ -#define _UCT_ 0 +#define _UCT_ 1 // how much diversification is used in the UCT-scheme? -#define _UCT_CONSTANT_ 0.01 +#define _UCT_CONSTANT_ 10.0 // is uct clause selection probabilistic similar to variable selection in sparrow? +// 0 = no, 1 = yes, use uct-value, 2 = yes, use score-value (_UCT_CONSTANT_ = 0.0) with squared score #define _PROBABILISTIC_UCT_ 0 +// additive constants for probabilistic uct > 0 +#define _UCT_EPS_ 0.0001 + +// shall we reset _UCT_ touched values after restart? +#define _UCT_RESET_ 0 + +// how shall we initialize the _UCT_ total touched counter? +// 0 = initialize with one, 1 = initialize with number of assertions +#define _UCT_INIT_ 1 + // shall we use addition/subtraction? #define _USE_ADDSUB_ 1 // shall we try multilication and division by 2? -#define _USE_MUL2DIV2_ 1 +#define _USE_MUL2DIV2_ 0 // shall we try multiplication by 3? -#define _USE_MUL3_ 1 +#define _USE_MUL3_ 0 // shall we try unary minus (= inverting and incrementing) -#define _USE_UNARY_MINUS_ 1 +#define _USE_UNARY_MINUS_ 0 // is random selection for assertions uniform? only works with _BFS_ = _UCT_ = 0 -#define _UNIFORM_RANDOM_ 1 +#define _UNIFORM_RANDOM_ 0 // should we use unsat-structures as done in SLS 4 SAT instead for random or bfs selection? #define _REAL_RS_ 0 @@ -124,13 +160,21 @@ Notes: #define _CACHE_TOP_SCORE_ 1 -#if ((_UCT_ > 0) + _UNIFORM_RANDOM_ + _REAL_RS_ + _REAL_PBFS_ > 1) || _BFS_ && (_UCT_ ||_UNIFORM_RANDOM_ ||_REAL_RS_ ||_REAL_PBFS_) +#if ((_BFS_ > 0) + (_UCT_ > 0) + _UNIFORM_RANDOM_ + _REAL_RS_ + _REAL_PBFS_ > 1) InvalidConfiguration; #endif #if (_PROBABILISTIC_UCT_ && !_UCT_) InvalidConfiguration; #endif - +#if (_PERM_RSTEP_ && !_TYPE_RSTEP_) + InvalidConfiguration; +#endif +#if (_PERC_CHANGE_ == 50) + InvalidConfiguration; +#endif +#if (_PERC_STICKY_ && !_FOCUS_) + InvalidConfiguration; +#endif #include"sls_params.hpp" #include"sls_evaluator.h" @@ -180,6 +224,7 @@ class sls_tactic : public tactic { sls_tracker m_tracker; sls_evaluator m_evaluator; + unsigned m_restart_limit; unsigned m_max_restarts; unsigned m_plateau_limit; @@ -208,6 +253,41 @@ class sls_tactic : public tactic { m_mpz_manager.del(m_two); } + double get_restart_armin(unsigned cnt_restarts) + { + unsigned outer_id = (unsigned)(0.5 + sqrt(0.25 + 2 * cnt_restarts)); + unsigned inner_id = cnt_restarts - (outer_id - 1) * outer_id / 2; + //printf("armin: %f\n", pow(1.1, inner_id + 1)); + return pow(_RESTART_CONST_ARMIN_, inner_id + 1); + } + + inline unsigned check_restart(unsigned curr_value) + { + if (curr_value > m_restart_limit) + { +#if _RESTART_SCHEME_ == 4 + m_restart_limit += (m_stats.m_restarts & (m_stats.m_restarts + 1)) ? _RESTART_LIMIT_ : (_RESTART_LIMIT_ * m_stats.m_restarts + 1); +#elif _RESTART_SCHEME_ == 3 + m_restart_limit += (unsigned)get_restart_armin(m_stats.m_restarts + 1) * _RESTART_LIMIT_; +#elif _RESTART_SCHEME_ == 2 + m_restart_limit += get_luby(m_stats.m_restarts + 1) * _RESTART_LIMIT_; +#elif _RESTART_SCHEME_ == 1 + if (m_stats.m_restarts & 1) + m_restart_limit += _RESTART_LIMIT_; + else + m_restart_limit += (2 << (m_stats.m_restarts >> 1)) * _RESTART_LIMIT_; +#else + m_restart_limit += _RESTART_LIMIT_; +#endif +#if _WEIGHT_TOGGLE_ + printf("Setting weight: %f\n", _WEIGHT_DIST_FACTOR_ * (((m_stats.m_restarts & 2) == 0) + 1)); + m_tracker.set_weight_dist_factor(_WEIGHT_DIST_FACTOR_ * (((m_stats.m_restarts & 2) == 0) + 1)); +#endif + return 0; + } + return 1; + } + ast_manager & m() const { return m_manager; } void set_cancel(bool f) { m_cancel = f; } @@ -435,12 +515,10 @@ class sls_tactic : public tactic { NOT_IMPLEMENTED_YET(); } - void mk_random_move(goal_ref const & g) { + void mk_random_move(ptr_vector & unsat_constants) + { unsigned rnd_mv = 0; - if (m_stats.m_moves > 10000) - rnd_mv = 0; - ptr_vector & unsat_constants = m_tracker.get_unsat_constants(g, m_stats.m_moves); unsigned ucc = unsat_constants.size(); unsigned rc = (m_tracker.get_random_uint((ucc < 16) ? 4 : (ucc < 256) ? 8 : (ucc < 4096) ? 12 : (ucc < 65536) ? 16 : 32)) % ucc; func_decl * fd = unsat_constants[rc]; @@ -503,6 +581,10 @@ class sls_tactic : public tactic { m_mpz_manager.del(new_value); } + void mk_random_move(goal_ref const & g) { + mk_random_move(m_tracker.get_unsat_constants(g, m_stats.m_moves)); + } + // will use VNS to ignore some possible moves and increase the flips per second double find_best_move_vns(goal_ref const & g, ptr_vector & to_evaluate, double score, unsigned & best_const, mpz & best_value, unsigned & new_bit, move_type & move) { @@ -857,7 +939,7 @@ class sls_tactic : public tactic { m_stats.m_flips++; global_score = incremental_score(g, fd, new_value); - local_score = m_tracker.get_score(q); + local_score = m_tracker.get_score(q); SASSERT(new_score == i * local_score / _INTENSIFICATION_TRIES_ + (_INTENSIFICATION_TRIES_ - i) * global_score / _INTENSIFICATION_TRIES_); @@ -875,6 +957,130 @@ class sls_tactic : public tactic { unsigned new_const = (unsigned)-1, new_bit = 0; mpz new_value; move_type move; + unsigned plateau_cnt = 0; + + score = rescore(g); + unsigned sz = g->size(); +#if _PERC_STICKY_ + expr * e = m_tracker.get_unsat_assertion(g, m_stats.m_moves); +#endif + +#if _RESTARTS_ == 1 + while (check_restart(m_stats.m_moves) && m_stats.m_stopwatch.get_current_seconds() < _TIMELIMIT_) { +#elif _RESTARTS_ == 2 + while (check_restart(plateau_cnt) && m_stats.m_stopwatch.get_current_seconds() < _TIMELIMIT_) { +#elif _RESTARTS_ == 3 + while (check_restart((unsigned)m_stats.m_stopwatch.get_current_seconds()) && m_stats.m_stopwatch.get_current_seconds() < _TIMELIMIT_) { +#else + while (m_stats.m_stopwatch.get_current_seconds() < _TIMELIMIT_) { +#endif + checkpoint(); + m_stats.m_moves++; + +#if _REAL_RS_ || _REAL_PBFS_ + //m_tracker.debug_real(g, m_stats.m_moves); +#endif + +#if _FOCUS_ +#if _PERC_STICKY_ + if (m_tracker.get_random_uint(16) % 100 >= _PERC_STICKY_ || m_mpz_manager.eq(m_tracker.get_value(e), m_one)) + e = m_tracker.get_unsat_assertion(g, m_stats.m_moves); +#else + expr * e = m_tracker.get_unsat_assertion(g, m_stats.m_moves); +#endif + if (!e) + { + res = l_true; + goto bailout; + } + ptr_vector & to_evaluate = m_tracker.get_unsat_constants_walksat(e); +#else + ptr_vector & to_evaluate = m_tracker.get_unsat_constants_gsat(g, sz); + if (!to_evaluate.size()) + { + res = l_true; + goto bailout; + } +#endif + +#if _TYPE_RSTEP_ + if (m_tracker.get_random_uint(16) % 1000 < _PERM_RSTEP_) + { +#if _TYPE_RSTEP_ == 1 + m_evaluator.randomize_local(to_evaluate); +#elif _TYPE_RSTEP_ == 2 + mk_random_move(to_evaluate); +#endif +#if _CACHE_TOP_SCORE_ + score = m_tracker.get_top_sum() / g->size(); +#else + score = top_score(g); +#endif + } + continue; +#endif + +#if _WEIGHT_DIST_ == 4 + m_tracker.set_weight_dist_factor(m_stats.m_stopwatch.get_current_seconds() / _TIMELIMIT_); +#endif + old_score = score; + new_const = (unsigned)-1; + +#if _VNS_ + score = find_best_move_vns(g, to_evaluate, score, new_const, new_value, new_bit, move); +#else + score = find_best_move(g, to_evaluate, score, new_const, new_value, new_bit, move); +#endif + + if (new_const == static_cast(-1)) { + score = old_score; + plateau_cnt++; +#if _INTENSIFICATION_ + handle_plateau(g, score); + //handle_plateau(g); + //e = m_tracker.get_unsat_assertion(g, m_stats.m_moves); + //to_evaluate = m_tracker.get_unsat_constants_walksat(e); +#else +#if _PERC_PLATEAU_MOVES_ + if (m_tracker.get_random_uint(8) % 100 < _PERC_PLATEAU_MOVES_) + mk_random_move(to_evaluate); + else +#endif +#if _REPICK_ + m_evaluator.randomize_local(g, m_stats.m_moves); +#else + m_evaluator.randomize_local(to_evaluate); +#endif +#endif + +#if _CACHE_TOP_SCORE_ + score = m_tracker.get_top_sum() / g->size(); +#else + score = top_score(g); +#endif + } else { + func_decl * fd = to_evaluate[new_const]; +#if _REAL_RS_ || _REAL_PBFS_ + score = serious_score(g, fd, new_value); +#else + score = incremental_score(g, fd, new_value); +#endif + } + } + + bailout: + m_mpz_manager.del(new_value); + + return res; + } + + // main search loop + lbool search_old(goal_ref const & g) { + lbool res = l_undef; + double score = 0.0, old_score = 0.0; + unsigned new_const = (unsigned)-1, new_bit = 0; + mpz new_value; + move_type move; score = rescore(g); TRACE("sls", tout << "Starting search, initial score = " << std::setprecision(32) << score << std::endl; @@ -887,12 +1093,12 @@ class sls_tactic : public tactic { // Andreas: Why do we only allow so few plateaus? #if _RESTARTS_ - while (plateau_cnt < m_plateau_limit && m_stats.m_stopwatch.get_current_seconds() < _TIMELIMIT_) { + while (m_stats.m_stopwatch.get_current_seconds() < 200 * (m_stats.m_restarts + 1) * 0.2) { + //while (plateau_cnt < m_plateau_limit && m_stats.m_stopwatch.get_current_seconds() < _TIMELIMIT_) { #else while (m_stats.m_stopwatch.get_current_seconds() < _TIMELIMIT_ && (_RESTARTS_ == 0 || m_stats.m_moves < _RESTARTS_)) { #endif do { - if (m_stats.m_moves == 5590) checkpoint(); #if _WEIGHT_DIST_ == 4 @@ -1072,7 +1278,11 @@ class sls_tactic : public tactic { verbose_stream() << "_BFS_ " << _BFS_ << std::endl; verbose_stream() << "_FOCUS_ " << _FOCUS_ << std::endl; + verbose_stream() << "_PERC_STICKY_ " << _PERC_STICKY_ << std::endl; verbose_stream() << "_RESTARTS_ " << _RESTARTS_ << std::endl; + verbose_stream() << "_RESTART_LIMIT_ " << _RESTART_LIMIT_ << std::endl; + verbose_stream() << "_RESTART_INIT_ " << _RESTART_INIT_ << std::endl; + verbose_stream() << "_RESTART_SCHEME_ " << _RESTART_SCHEME_ << std::endl; verbose_stream() << "_TIMELIMIT_ " << _TIMELIMIT_ << std::endl; verbose_stream() << "_SCORE_AND_AVG_ " << _SCORE_AND_AVG_ << std::endl; verbose_stream() << "_SCORE_OR_MUL_ " << _SCORE_OR_MUL_ << std::endl; @@ -1081,9 +1291,14 @@ class sls_tactic : public tactic { verbose_stream() << "_WEIGHT_DIST_FACTOR_ " << std::fixed << std::setprecision(2) << _WEIGHT_DIST_FACTOR_ << std::endl; verbose_stream() << "_INTENSIFICATION_ " << _INTENSIFICATION_ << std::endl; verbose_stream() << "_INTENSIFICATION_TRIES_ " << _INTENSIFICATION_TRIES_ << std::endl; + verbose_stream() << "_PERC_PLATEAU_MOVES_ " << _PERC_PLATEAU_MOVES_ << std::endl; + verbose_stream() << "_REPICK_ " << _REPICK_ << std::endl; verbose_stream() << "_UCT_ " << _UCT_ << std::endl; verbose_stream() << "_UCT_CONSTANT_ " << std::fixed << std::setprecision(2) << _UCT_CONSTANT_ << std::endl; + verbose_stream() << "_UCT_RESET_ " << _UCT_RESET_ << std::endl; + verbose_stream() << "_UCT_INIT_ " << _UCT_INIT_ << std::endl; verbose_stream() << "_PROBABILISTIC_UCT_ " << _PROBABILISTIC_UCT_ << std::endl; + verbose_stream() << "_UCT_EPS_ " << std::fixed << std::setprecision(4) << _UCT_EPS_ << std::endl; verbose_stream() << "_USE_ADDSUB_ " << _USE_ADDSUB_ << std::endl; verbose_stream() << "_USE_MUL2DIV2_ " << _USE_MUL2DIV2_ << std::endl; verbose_stream() << "_USE_MUL3_ " << _USE_MUL3_ << std::endl; @@ -1099,21 +1314,30 @@ class sls_tactic : public tactic { verbose_stream() << "_CACHE_TOP_SCORE_ " << _CACHE_TOP_SCORE_ << std::endl; #if _WEIGHT_DIST_ == 4 - m_tracker.set_weight_dist_factor(m_stats.m_stopwatch.get_current_seconds() / _TIMELIMIT_); + m_tracker.set_weight_dist_factor(m_stats.m_stopwatch.get_current_seconds() / _TIMELIMIT_); +#endif +#if _WEIGHT_TOGGLE_ + m_tracker.set_weight_dist_factor(_WEIGHT_DIST_FACTOR_); #endif m_tracker.initialize(g); lbool res = l_undef; + m_restart_limit = _RESTART_LIMIT_; + do { checkpoint(); - // Andreas: I think restarts are too impotant to ignore 99% of them are happening... - //if ((m_stats.m_restarts % 100) == 0) - report_tactic_progress("Searching... restarts left:", m_max_restarts - m_stats.m_restarts); - + + report_tactic_progress("Searching... restarts left:", m_max_restarts - m_stats.m_restarts); res = search(g); if (res == l_undef) - m_tracker.randomize(); + { +#if _RESTART_INIT_ + m_tracker.randomize(g); +#else + m_tracker.reset(g); +#endif + } } while (m_stats.m_stopwatch.get_current_seconds() < _TIMELIMIT_ && res != l_true && m_stats.m_restarts++ < m_max_restarts); @@ -1121,6 +1345,13 @@ class sls_tactic : public tactic { if (res == l_true) { report_tactic_progress("Number of flips:", m_stats.m_moves); + for (unsigned i = 0; i < g->size(); i++) + if (!m_mpz_manager.is_one(m_tracker.get_value(g->form(i)))) + { + verbose_stream() << "Terminated before all assertions were SAT!" << std::endl; + NOT_IMPLEMENTED_YET(); + } + if (m_produce_models) { model_ref mdl = m_tracker.get_model(); mc = model2model_converter(mdl.get()); @@ -1183,12 +1414,17 @@ public: } virtual void cleanup() { - imp * d = alloc(imp, m, m_params, m_stats); + imp * d = m_imp; #pragma omp critical (tactic_cancel) { - std::swap(d, m_imp); + d = m_imp; } dealloc(d); + d = alloc(imp, m, m_params, m_stats); + #pragma omp critical (tactic_cancel) + { + m_imp = d; + } } virtual void collect_statistics(statistics & st) const { @@ -1246,6 +1482,9 @@ tactic * mk_preamble(ast_manager & m, params_ref const & p) { // conservative gaussian elimination. gaussian_p.set_uint("gaussian_max_occs", 2); + params_ref ctx_p; + ctx_p.set_uint("max_depth", 32); + ctx_p.set_uint("max_steps", 5000000); return and_then(and_then(mk_simplify_tactic(m), mk_propagate_values_tactic(m), using_params(mk_solve_eqs_tactic(m), gaussian_p), @@ -1254,6 +1493,10 @@ 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 ... + mk_simplify_tactic(m), // Andreas: How does a NNF actually look like? Can it contain ITE operators? mk_nnf_tactic(m, p)); } diff --git a/src/tactic/sls/sls_tracker.h b/src/tactic/sls/sls_tracker.h index 006bbb888..0aca1f59c 100644 --- a/src/tactic/sls/sls_tracker.h +++ b/src/tactic/sls/sls_tracker.h @@ -65,6 +65,7 @@ private: typedef obj_map scores_type; typedef obj_map > uplinks_type; typedef obj_map > occ_type; + obj_hashtable m_top_expr; scores_type m_scores; uplinks_type m_uplinks; entry_point_type m_entry_points; @@ -75,15 +76,15 @@ private: unsigned m_touched; #endif #if _REAL_RS_ || _REAL_PBFS_ - ptr_vector m_unsat_expr; - obj_map m_where_false; - expr** m_list_false; + ptr_vector m_unsat_expr; + obj_map m_where_false; + expr** m_list_false; #endif #if _CACHE_TOP_SCORE_ - double m_top_sum; + double m_top_sum; #endif -#if _WEIGHT_DIST_ == 4 - double m_weight_dist_factor; +#if _WEIGHT_DIST_ == 4 || _WEIGHT_TOGGLE_ + double m_weight_dist_factor; #endif public: @@ -104,7 +105,7 @@ public: m_mpz_manager.del(m_two); } -#if _WEIGHT_DIST_ == 4 +#if _WEIGHT_DIST_ == 4 || _WEIGHT_TOGGLE_ inline void set_weight_dist_factor(double val) { m_weight_dist_factor = val; } @@ -182,12 +183,12 @@ public: inline unsigned has_pos_occ(expr * n) { SASSERT(m_scores.contains(n)); return m_scores.find(n).has_pos_occ; - } + } inline unsigned has_neg_occ(expr * n) { SASSERT(m_scores.contains(n)); return m_scores.find(n).has_neg_occ; - } + } #endif inline unsigned get_distance(expr * n) { @@ -213,11 +214,62 @@ public: return m_uplinks.contains(n); } + inline bool is_top_expr(expr * n) { + return m_top_expr.contains(n); + } + inline ptr_vector & get_uplinks(expr * n) { SASSERT(m_uplinks.contains(n)); return m_uplinks.find(n); } +#if _REAL_RS_ || _REAL_PBFS_ + 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 + void initialize(app * n) { // Build score table if (!m_scores.contains(n)) { @@ -327,7 +379,7 @@ public: } } for_each_expr(proc, visited, e); - } + } void initialize_recursive(expr * e) { if (m_manager.is_and(e) || m_manager.is_or(e)) { @@ -344,7 +396,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(goal_ref const & g) { init_proc proc(m_manager, *this); @@ -352,6 +404,10 @@ public: unsigned sz = g->size(); for (unsigned i = 0; i < sz; i++) { expr * e = g->form(i); + if (!m_top_expr.contains(e)) + m_top_expr.insert(e); + else + printf("this is already in ...\n"); // Andreas: Maybe not fully correct. #if _FOCUS_ == 2 initialize_recursive(proc, visited, e); @@ -380,18 +436,20 @@ public: #if _REAL_RS_ || _REAL_PBFS_ 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)); + //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 _EARLY_PRUNE_ for (unsigned i = 0; i < sz; i++) - setup_occs(g->form(i)); + setup_occs(g->form(i)); #endif #if _UCT_ - m_touched = 1; + m_touched = _UCT_INIT_ ? g->size() : 1; #endif } @@ -407,8 +465,12 @@ public: 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); } -// printf("Going in %d\n", m_where_false.size()); + //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); @@ -416,12 +478,14 @@ public: void break_assertion(expr * e) { + //printf("I'm broken... that's still fine.\n"); if (!m_where_false.contains(e)) { + //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()); + // printf("Going in %d\n", m_where_false.size()); } //if (!m_unsat_expr.contains(e)) //m_unsat_expr.push_back(e); @@ -522,7 +586,7 @@ public: NOT_IMPLEMENTED_YET(); // This only works for bit-vectors for now. } - void randomize() { + void randomize(goal_ref const & g) { TRACE("sls", tout << "Abandoned model:" << std::endl; show_model(tout); ); for (entry_point_type::iterator it = m_entry_points.begin(); it != m_entry_points.end(); it++) { @@ -534,6 +598,28 @@ public: } TRACE("sls", tout << "Randomized model:" << std::endl; show_model(tout); ); + +#if _UCT_RESET_ + m_touched = _UCT_INIT_ ? g->size() : 1; + for (unsigned i = 0; i < g->size(); i++) + m_scores.find(g->form(i)).touched = 1; +#endif + } + + void reset(goal_ref const & g) { + TRACE("sls", tout << "Abandoned model:" << std::endl; show_model(tout); ); + + for (entry_point_type::iterator it = m_entry_points.begin(); it != m_entry_points.end(); it++) { + mpz temp = m_zero; + set_value(it->m_value, temp); + m_mpz_manager.del(temp); + } + +#if _UCT_RESET_ + m_touched = _UCT_INIT_ ? g->size() : 1; + for (unsigned i = 0; i < g->size(); i++) + m_scores.find(g->form(i)).touched = 1; +#endif } #if _EARLY_PRUNE_ @@ -591,12 +677,20 @@ public: #if _SCORE_AND_AVG_ double sum = 0.0; for (unsigned i = 0; i < a->get_num_args(); i++) +#if _DIRTY_UP_ + sum += is_top_expr(args[i]) ? 1.0 : get_score(args[i]); +#else sum += get_score(args[i]); +#endif res = sum / (double) a->get_num_args(); #else double min = 1.0; for (unsigned i = 0; i < a->get_num_args(); i++) { +#if _DIRTY_UP_ + double cur = is_top_expr(args[i]) ? 1.0 : get_score(args[i]); +#else double cur = get_score(args[i]); +#endif if (cur < min) min = cur; } res = min; @@ -610,14 +704,22 @@ public: #if _SCORE_OR_MUL_ double inv = 1.0; for (unsigned i = 0; i < a->get_num_args(); i++) { +#if _DIRTY_UP_ + double cur = is_top_expr(args[i]) ? 1.0 : get_score(args[i]); +#else double cur = get_score(args[i]); +#endif inv *= (1.0 - get_score(args[i])); } res = 1.0 - inv; #else double max = 0.0; for (unsigned i = 0; i < a->get_num_args(); i++) { +#if _DIRTY_UP_ + double cur = is_top_expr(args[i]) ? 1.0 : get_score(args[i]); +#else double cur = get_score(args[i]); +#endif if (cur > max) max = cur; } res = max; @@ -772,7 +874,11 @@ public: expr * child = a->get_arg(0); if (m_manager.is_and(child) || m_manager.is_or(child)) // Precondition: Assertion set is in NNF. NOT_IMPLEMENTED_YET(); +#if _DIRTY_UP_ + res = is_top_expr(child) ? 0.0 : score_bool(child, true); +#else res = score_bool(child, true); +#endif } else if (m_manager.is_distinct(n)) { app * a = to_app(n); @@ -803,7 +909,11 @@ public: if (afid == m_bv_util.get_family_id()) #endif #if _WEIGHT_DIST_ == 1 +#if _WEIGHT_TOGGLE_ + if (res < 1.0) res *= m_weight_dist_factor; +#else if (res < 1.0) res *= _WEIGHT_DIST_FACTOR_; +#endif #elif _WEIGHT_DIST_ == 2 res *= res; #elif _WEIGHT_DIST_ == 3 @@ -900,6 +1010,10 @@ public: } ptr_vector & get_unsat_constants_gsat(goal_ref const & g, unsigned sz) { + if (sz == 1) + return get_constants(); + m_temp_constants.reset(); + for (unsigned i = 0; i < sz; i++) { expr * q = g->form(i); if (m_mpz_manager.eq(get_value(q), m_one)) @@ -945,7 +1059,7 @@ public: } ptr_vector & get_unsat_constants_walksat(expr * e) { - if (!e) + if (!e || m_temp_constants.size()) return m_temp_constants; ptr_vector const & this_decls = m_constants_occ.find(e); unsigned sz = this_decls.size(); @@ -1033,32 +1147,43 @@ public: #if _PROBABILISTIC_UCT_ double sum_score = 0.0; unsigned start_index = get_random_uint(16) % sz; + for (unsigned i = start_index; i < sz; i++) { expr * e = g->form(i); vscore = m_scores.find(e); - double q = vscore.score + _UCT_CONSTANT_ * sqrt(log(m_touched)/vscore.touched); +#if _PROBABILISTIC_UCT_ == 2 + double q = vscore.score * vscore.score; +#else + double q = vscore.score + _UCT_CONSTANT_ * sqrt(log(m_touched)/vscore.touched) + _UCT_EPS_; +#endif if (m_mpz_manager.neq(get_value(g->form(i)), m_one)) { sum_score += q; if (rand() <= (q * RAND_MAX / sum_score) + 1) pos = i; - } + } } for (unsigned i = 0; i < start_index; i++) { expr * e = g->form(i); vscore = m_scores.find(e); - double q = vscore.score + _UCT_CONSTANT_ * sqrt(log(m_touched)/vscore.touched); +#if _PROBABILISTIC_UCT_ == 2 + double q = vscore.score * vscore.score; +#else + double q = vscore.score + _UCT_CONSTANT_ * sqrt(log(m_touched)/vscore.touched) + _UCT_EPS_; +#endif if (m_mpz_manager.neq(get_value(g->form(i)), m_one)) { sum_score += q; if (rand() <= (q * RAND_MAX / sum_score) + 1) pos = i; - } + } } #else double max = -1.0; for (unsigned i = 0; i < sz; i++) { expr * e = g->form(i); +// for (unsigned i = 0; i < m_where_false.size(); i++) { +// expr * e = m_list_false[i]; vscore = m_scores.find(e); #if _UCT_ == 1 double q = vscore.score + _UCT_CONSTANT_ * sqrt(log(m_touched)/vscore.touched); @@ -1078,6 +1203,7 @@ public: m_scores.find(g->form(pos)).touched = flip; #endif expr * e = g->form(pos); +// expr * e = m_list_false[pos]; #elif _BFS_ == 3 unsigned int pos = -1; @@ -1109,7 +1235,7 @@ public: #elif _UNIFORM_RANDOM_ unsigned cnt_unsat = 0, pos = -1; for (unsigned i = 0; i < sz; i++) - if (m_mpz_manager.neq(get_value(g->form(i)), m_one) && (get_random_uint(16) % ++cnt_unsat == 0)) pos = i; + if (m_mpz_manager.neq(get_value(g->form(i)), m_one) && (get_random_uint(16) % ++cnt_unsat == 0)) pos = i; if (pos == static_cast(-1)) return m_temp_constants; expr * e = g->form(pos); @@ -1120,8 +1246,7 @@ public: sz = m_where_false.size(); if (sz == 0) return m_temp_constants; - else - expr * e = m_list_false[get_random_uint(16) % sz]; + expr * e = m_list_false[get_random_uint(16) % sz]; #elif _REAL_PBFS_ //unsigned pos = m_false_list[flip % m_cnt_false]; //expr * e = get_unsat_assertion(g, sz, pos); @@ -1154,6 +1279,142 @@ public: #endif } } + + + expr * get_unsat_assertion(goal_ref const & g, unsigned int flip) { + unsigned sz = g->size(); + + if (sz == 1) + return g->form(0); + + m_temp_constants.reset(); +#if _FOCUS_ == 1 +#if _UCT_ + unsigned pos = -1; + value_score vscore; +#if _PROBABILISTIC_UCT_ + double sum_score = 0.0; + unsigned start_index = get_random_uint(16) % sz; + + for (unsigned i = start_index; i < sz; i++) + { + expr * e = g->form(i); + vscore = m_scores.find(e); +#if _PROBABILISTIC_UCT_ == 2 + double q = vscore.score * vscore.score + _UCT_EPS_; +#else + double q = vscore.score + _UCT_CONSTANT_ * sqrt(log(m_touched)/vscore.touched) + _UCT_EPS_; +#endif + if (m_mpz_manager.neq(get_value(g->form(i)), m_one)) { + sum_score += q; + if (rand() <= (q * RAND_MAX / sum_score) + 1) + pos = i; + } + } + for (unsigned i = 0; i < start_index; i++) + { + expr * e = g->form(i); + vscore = m_scores.find(e); +#if _PROBABILISTIC_UCT_ == 2 + double q = vscore.score * vscore.score + _UCT_EPS_; +#else + double q = vscore.score + _UCT_CONSTANT_ * sqrt(log(m_touched)/vscore.touched) + _UCT_EPS_; +#endif + if (m_mpz_manager.neq(get_value(g->form(i)), m_one)) { + sum_score += q; + if (rand() <= (q * RAND_MAX / sum_score) + 1) + pos = i; + } + } +#else + double max = -1.0; + for (unsigned i = 0; i < sz; i++) { + expr * e = g->form(i); +// for (unsigned i = 0; i < m_where_false.size(); i++) { +// expr * e = m_list_false[i]; + vscore = m_scores.find(e); +#if _UCT_ == 1 + double q = vscore.score + _UCT_CONSTANT_ * sqrt(log(m_touched)/vscore.touched); +#elif _UCT_ == 2 + double q = vscore.score + (_UCT_CONSTANT_ * (flip - vscore.touched)) / sz; +#endif + if (q > max && m_mpz_manager.neq(get_value(e), m_one) ) { max = q; pos = i; } + } +#endif + if (pos == static_cast(-1)) + return 0; + +#if _UCT_ == 1 + m_scores.find(g->form(pos)).touched++; + m_touched++; +#elif _UCT_ == 2 + m_scores.find(g->form(pos)).touched = flip; +#endif +// return m_list_false[pos]; + return g->form(pos); + +#elif _BFS_ == 3 + unsigned int pos = -1; + double max = -1.0; + for (unsigned i = 0; i < sz; i++) { + expr * e = g->form(i); + double q = get_score(e); + if (q > max && m_mpz_manager.neq(get_value(e), m_one) ) { max = q; pos = i; } + if (pos == static_cast(-1)) + return 0; + return g->form(pos); +#elif _BFS_ == 2 + unsigned int pos = -1; + double min = 2.0; + for (unsigned i = 0; i < sz; i++) { + expr * e = g->form(i); + double q = get_score(e); + if (q < min && m_mpz_manager.neq(get_value(e), m_one) ) { min = q; pos = i; } + } + if (pos == static_cast(-1)) + return 0; + return g->form(pos); +#elif _BFS_ == 1 + unsigned int pos = flip % sz; + return get_unsat_assertion(g, sz, pos); +#elif _UNIFORM_RANDOM_ + unsigned cnt_unsat = 0, pos = -1; + for (unsigned i = 0; i < sz; i++) + if (m_mpz_manager.neq(get_value(g->form(i)), m_one) && (get_random_uint(16) % ++cnt_unsat == 0)) pos = i; + if (pos == static_cast(-1)) + return 0; + return g->form(pos); +#elif _REAL_RS_ + //unsigned pos = m_false_list[get_random_uint(16) % m_cnt_false]; + //expr * e = get_unsat_assertion(g, sz, pos); + //expr * e = m_unsat_expr[get_random_uint(16) % m_unsat_expr.size()]; + sz = m_where_false.size(); + if (sz == 0) + return 0; + return m_list_false[get_random_uint(16) % sz]; +#elif _REAL_PBFS_ + //unsigned pos = m_false_list[flip % m_cnt_false]; + //expr * e = get_unsat_assertion(g, sz, pos); + //expr * e = m_unsat_expr[flip % m_unsat_expr.size()]; + sz = m_where_false.size(); + if (sz == 0) + return0; + else + return m_list_false[flip % sz]; +#else + unsigned int pos = get_random_uint(16) % sz; + return get_unsat_assertion(g, sz, pos); +#endif + return g->form(pos); +#elif _FOCUS_ == 2 +#if _BFS_ + unsigned int pos = flip % sz; +#else + unsigned int pos = get_random_uint(16) % sz; +#endif + return get_unsat_constants_crsat(g, sz, pos); +#endif + } }; #endif \ No newline at end of file