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